**Description:** An inference commuting equality in antecedent. Used to eliminate the
need for a syllogism. (Contributed by NM, 10-Jan-1993)

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

Hypothesis | equcoms.1 | $${\u22a2}{x}={y}\to {\phi}$$ | |

Assertion | equcoms | $${\u22a2}{y}={x}\to {\phi}$$ |

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

1 | equcoms.1 | $${\u22a2}{x}={y}\to {\phi}$$ | |

2 | equcomi | $${\u22a2}{y}={x}\to {x}={y}$$ | |

3 | 2 1 | syl | $${\u22a2}{y}={x}\to {\phi}$$ |