Theorem equcoms 1722

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 1718	. 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)
2		equcoms.1	. 2 ⊢ (𝑥 = 𝑦 → 𝜑)
3	1, 2	syl 14	1 ⊢ (𝑦 = 𝑥 → 𝜑)

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1463  ax-ie2 1508  ax-8 1518  ax-17 1540  ax-i9 1544

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equtr  1723  equtr2  1725  equequ2  1727  ax10o  1729  cbvalv1  1765  cbvexv1  1766  cbvalh  1767  cbvexh  1769  equvini  1772  stdpc7  1784  sbequ12r  1786  sbequ12a  1787  sbequ  1854  sb6rf  1867  cbvalvw  1934  cbvexvw  1935  sb9v  1997  sb6a  2007  mo2n  2073  elequ1  2171  elequ2  2172  cleqh  2296  cbvab  2320  sbralie  2747  reu8  2960  sbcco2  3012  snnex  4483  tfisi  4623  opeliunxp  4718  elrnmpt1  4917  rnxpid  5104  iotaval  5230  elabrex  5804  elabrexg  5805  opabex3d  6178  opabex3  6179  enq0ref  7500  fproddivapf  11796  setindis  15613  bdsetindis  15615