Theorem equcoms 1754

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 1750	. 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 1495  ax-ie2 1540  ax-8 1550  ax-17 1572  ax-i9 1576

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equtr  1755  equtr2  1757  equequ2  1759  ax10o  1761  cbvalv1  1797  cbvexv1  1798  cbvalh  1799  cbvexh  1801  equvini  1804  stdpc7  1816  sbequ12r  1818  sbequ12a  1819  sbequ  1886  sb6rf  1899  cbvalvw  1966  cbvexvw  1967  sb9v  2029  sb6a  2039  mo2n  2105  elequ1  2204  elequ2  2205  cleqh  2329  cbvab  2353  sbralie  2783  reu8  2999  sbcco2  3051  reu8nf  3110  snnex  4539  tfisi  4679  opeliunxp  4774  elrnmpt1  4975  rnxpid  5163  iotaval  5290  elabrex  5887  elabrexg  5888  opabex3d  6272  opabex3  6273  enq0ref  7628  fproddivapf  12150  setindis  16354  bdsetindis  16356