ADVICE on choosing a rule appropriate to the operator '∨' (OR)
| suggestions: | ||
| If ∨ | is the Main Operator in a PREMISE, | DS CD |
| the MO in the GOAL or CONCLUSION, | CD ADD | |
| to be LEFT AS IS while others change, | COM ASSOC | |
| to be REPLACED with another operator, | DM DN DIST IMPL EQUIV TAUT |
Note: if the conclusion or goal proposition is IDENTICAL to a portion of a premise, then chose the rule according to that PREMISE'S main operator.
ADD can be tricky. The v winds up in the result not in its premise.