Theorem equcoms 1634

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 1632	. 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 104  ax-gen 1378  ax-ie2 1423  ax-8 1435  ax-17 1459  ax-i9 1463

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  equtr  1635  equtr2  1637  equequ2  1639  elequ1  1640  elequ2  1641  ax10o  1643  cbvalh  1676  cbvexh  1678  equvini  1681  stdpc7  1693  sbequ12r  1695  sbequ12a  1696  sbequ  1761  sb6rf  1774  sb9v  1895  sb6a  1905  mo2n  1969  cleqh  2178  cbvab  2201  reu8  2788  sbcco2  2837  snnex  4199  tfisi  4328  opeliunxp  4413  elrnmpt1  4603  rnxpid  4775  iotaval  4898  elabrex  5418  opabex3d  5768  opabex3  5769  enq0ref  6623  setindis  10762  bdsetindis  10764