Theorem equcoms 1594

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

Hypothesis

Ref	Expression
equcoms.1	⊢ (𝑥 = 𝑦 → 𝜑)

Assertion

Ref	Expression
equcoms	⊢ (𝑦 = 𝑥 → 𝜑)

Proof of Theorem equcoms

Step	Hyp	Ref	Expression
1		equcomi 1592	. 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)
2		equcoms.1	. 2 ⊢ (𝑥 = 𝑦 → 𝜑)
3	1, 2	syl 14	1 ⊢ (𝑦 = 𝑥 → 𝜑)

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-gen 1338  ax-ie2 1383  ax-8 1395  ax-17 1419  ax-i9 1423

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  equtr  1595  equtr2  1597  equequ2  1599  elequ1  1600  elequ2  1601  ax10o  1603  cbvalh  1636  cbvexh  1638  equvini  1641  stdpc7  1653  sbequ12r  1655  sbequ12a  1656  sbequ  1721  sb6rf  1733  sb9v  1854  sb6a  1864  mo2n  1928  cleqh  2137  cbvab  2160  reu8  2737  sbcco2  2786  snnex  4181  tfisi  4310  opeliunxp  4395  elrnmpt1  4585  rnxpid  4755  iotaval  4878  elabrex  5397  opabex3d  5748  opabex3  5749  enq0ref  6531  setindis  10092  bdsetindis  10094