>>11691429It's a way of exploiting the rules of conjunction called augmentation. Lines 2-6 is just standard assumption-conditional procedure. Lines 7-11 I assume , and isolate . I can't just do here since our dependency numbers for these lines is the assumption, and that isn't allowed. So what I did was augmentation, where I conjuncted with one of our established premises, , and then isolated again so that now has a dependency number based on a premise. Now I can make a conditional out of our assumption and get the last conditional to prove our biconditional. It's a cheese strategy but it works for exams.