IFF Introduction
   
 

This rule is used to introduce an if and only if formula from two opposite implies formulas (a > b and b > a can be used to get a # b), or backwards to
split an if and only if formula up into two boxes to prove left ARROW right and right ARROW left.
To use it forwards:

  1. select an empty line and click on IFF Introduction.
  2. select two opposite implies lines (for example a > b and b > a), which are in the empty lines scope. The left and right hand sides of the IF AND ONLY IF formula will be the same as the left and right sides of the first ARROW formula selected here.
  3. this will add the IF AND ONLY IF formula line to the proof.
To use it backwards:
  1. select the IF AND ONLY IF goal line you wish to seperate out and click on IFF Introduction.
  2. This will add two new boxes to the proof which are used to prove the left side IMPLIES right side of the IFF formula and the right side IMPLIES the left side.