Theorem equcoms 1636

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 1633	. 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 1379  ax-ie2 1424  ax-8 1436  ax-17 1460  ax-i9 1464

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  equtr  1637  equtr2  1639  equequ2  1641  elequ1  1642  elequ2  1643  ax10o  1645  cbvalh  1678  cbvexh  1680  equvini  1683  stdpc7  1695  sbequ12r  1697  sbequ12a  1698  sbequ  1763  sb6rf  1776  sb9v  1897  sb6a  1907  mo2n  1971  cleqh  2182  cbvab  2205  reu8  2797  sbcco2  2846  snnex  4227  tfisi  4356  opeliunxp  4441  elrnmpt1  4633  rnxpid  4805  iotaval  4928  elabrex  5449  opabex3d  5799  opabex3  5800  enq0ref  6737  setindis  11029  bdsetindis  11031