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

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

1. select the goal IF AND ONLY IF line you wish to introduce and click on Derived If and only if Introduction.
2. the A ^ B | ~A ^ ~B equivalent of the goal line will then be added as a new goal to you proof.