Or Elimination
   
 

This rule is used to eliminate an OR formula from your proof by proving a goal which can be achieved if either the left sub formula or the right sub formula of the OR formula is true (arguing by cases). It is used backwards only (on your current goal) to split the proof into these two cases.
To use it backwards:

  1. select the goal line you wish to derive and click on Or Elimination.
  2. then select the OR formula line (in the scope of the goal line) you wish to use to derive the goal.
  3. a double box will then be added to your proof with the left and right hand boxes assuming the left and right hand sub formulas of your OR formula, respectively, and having the goal line you selected as their conclusions.