Theorem equcoms 1696

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 1692	. 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 105  ax-gen 1437  ax-ie2 1482  ax-8 1492  ax-17 1514  ax-i9 1518

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  equtr  1697  equtr2  1699  equequ2  1701  ax10o  1703  cbvalv1  1739  cbvexv1  1740  cbvalh  1741  cbvexh  1743  equvini  1746  stdpc7  1758  sbequ12r  1760  sbequ12a  1761  sbequ  1828  sb6rf  1841  cbvalvw  1907  cbvexvw  1908  sb9v  1966  sb6a  1976  mo2n  2042  elequ1  2140  elequ2  2141  cleqh  2266  cbvab  2290  sbralie  2710  reu8  2922  sbcco2  2973  snnex  4426  tfisi  4564  opeliunxp  4659  elrnmpt1  4855  rnxpid  5038  iotaval  5164  elabrex  5726  opabex3d  6089  opabex3  6090  enq0ref  7374  fproddivapf  11572  setindis  13849  bdsetindis  13851