This rule can be used forwards to derive A ^ B | ~A ^ ~B from A # B or backwards to derive A # B as a new goal from A ^ B | ~A ^ ~B.
To use this rule forwards:

1. select an empty line and click on If and only if Elimination (derived).
2. then select the IF AND ONLY IF formula line to eliminate (this line must be in the scope of the empty line).
3. the A ^ B | ~A ^ ~B equivalent of the line you selected will then be added as a new line to the proof.

1. select the goal A ^ B | ~A ^ ~B line you wish to eliminate and click on If and only if Elimination (derived).
2. the IF AND ONLY IF equivalent of the goal line will then be added as a new goal to your proof.