ADVICE on choosing a rule appropriate to the operator '=' (IDENTITY)
| suggestions: | ||
| If = | is the Main Operator in a PREMISE, | ID.1 ID.2 ID.3 |
| the MO in the GOAL or CONCLUSION, | ID.1 ID.2 ID.3 | |
| to be LEFT AS IS while others change, | any equivalence that fits the other operators. | |
| to be REPLACED with another operator, | DN TAUT EG UG |
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.
You can even use ID.3 to replace one of the individual constants in an identity with another individual constant!
Note: These rules are only defined for individual constants. To apply them to a variable, first instantiate to a constant. To prove a universal truth about identities, use IP.