This rule can be used forwards to derive either the left or right hand sub formula from an IF AND ONLY IF formula using the other sub formula, or backwards to derive one of the sub formulas as a new goal line using the other sub formula.
To use it forwards:

1. select and empty line and click on If and Only If Elimination.
2. then select the IF AND ONLY IF formula you wish to eliminate (the formula must be in the scope of the empty line).
3. then select a formula which matches either the left or right sub formula of the the IF AND ONLY IF formula, which must be also in the scope of the empty line.
4. the sub formula on the other side of the IF AND ONLY IF formula from the formula you selected will then be added, as a new line, into your proof.

1. select the goal line which matches a sub formula of the IF AND ONLY IF formula you wish to eliminate and click on If and Only If Elimination.
2. then select the IF AND ONLY IF formula you wish to use in the elimination, which must be in the scope of the goal line.
3. the sub formula on the other side of the IF AND ONLY IF formula from the goal formula will then be added as a new goal to your proof.