ADVICE on choosing a rule appropriate to a line WITHOUT an operator or one which is compound but REPEATED in the same order within another line.
| suggestions: | ||
| If it is | repeated in a PREMISE, | MP CONJ ADD |
| repeated in a GOAL or CONCLUSION, | SIMP MP DS | |
| to be LEFT AS IS while others change, | cannot be done | |
| to be REPLACED with another operator, | DN 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. If just part of an • line is found in another premise, use SIMP.