TRIPLE BAR Strategy

Next Related Topic on Ring

ADVICE on choosing a rule appropriate to the operator '' (EQUIV)

suggestions:
If ≡ is the Main Operator in a PREMISE, EQUIV
the MO in the GOAL or CONCLUSION, EQUIV
to be LEFT AS IS while others change, cannot be done
to be REPLACED with another operator, EQUIV 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.