Theorem equcoms 1732

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 1728	. 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 1473  ax-ie2 1518  ax-8 1528  ax-17 1550  ax-i9 1554

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equtr  1733  equtr2  1735  equequ2  1737  ax10o  1739  cbvalv1  1775  cbvexv1  1776  cbvalh  1777  cbvexh  1779  equvini  1782  stdpc7  1794  sbequ12r  1796  sbequ12a  1797  sbequ  1864  sb6rf  1877  cbvalvw  1944  cbvexvw  1945  sb9v  2007  sb6a  2017  mo2n  2083  elequ1  2181  elequ2  2182  cleqh  2306  cbvab  2330  sbralie  2757  reu8  2970  sbcco2  3022  snnex  4499  tfisi  4639  opeliunxp  4734  elrnmpt1  4934  rnxpid  5122  iotaval  5248  elabrex  5833  elabrexg  5834  opabex3d  6213  opabex3  6214  enq0ref  7553  fproddivapf  11986  setindis  15977  bdsetindis  15979