**Description:** Inference applying commutative law for class equality to an antecedent.
(Contributed by NM, 24-Jun-1993)

Ref | Expression | ||
---|---|---|---|

Hypothesis | eqcoms.1 | $${\u22a2}{A}={B}\to {\phi}$$ | |

Assertion | eqcoms | $${\u22a2}{B}={A}\to {\phi}$$ |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | eqcoms.1 | $${\u22a2}{A}={B}\to {\phi}$$ | |

2 | eqcom | $${\u22a2}{B}={A}\leftrightarrow {A}={B}$$ | |

3 | 2 1 | sylbi | $${\u22a2}{B}={A}\to {\phi}$$ |