Theorem equcoms 1755

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 1751	. 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 1497  ax-ie2 1542  ax-8 1552  ax-17 1574  ax-i9 1578

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equtr  1756  equtr2  1758  equequ2  1760  ax10o  1762  cbvalv1  1798  cbvexv1  1799  cbvalh  1800  cbvexh  1802  equvini  1805  stdpc7  1817  sbequ12r  1819  sbequ12a  1820  sbequ  1887  sb6rf  1900  cbvalvw  1967  cbvexvw  1968  sb9v  2030  sb6a  2040  mo2n  2106  elequ1  2205  elequ2  2206  cleqh  2330  cbvab  2354  sbralie  2784  reu8  3001  sbcco2  3053  reu8nf  3112  snnex  4547  tfisi  4687  opeliunxp  4783  elrnmpt1  4985  rnxpid  5173  iotaval  5300  elabrex  5903  elabrexg  5904  opabex3d  6288  opabex3  6289  enq0ref  7658  fproddivapf  12215  setindis  16622  bdsetindis  16624