Theorem equcoms 1684

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 1680	. 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 1425  ax-ie2 1470  ax-8 1482  ax-17 1506  ax-i9 1510

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  equtr  1685  equtr2  1687  equequ2  1689  elequ1  1690  elequ2  1691  ax10o  1693  cbvalh  1726  cbvexh  1728  equvini  1731  stdpc7  1743  sbequ12r  1745  sbequ12a  1746  sbequ  1812  sb6rf  1825  sb9v  1953  sb6a  1963  mo2n  2027  cleqh  2239  cbvab  2263  sbralie  2670  reu8  2880  sbcco2  2931  snnex  4369  tfisi  4501  opeliunxp  4594  elrnmpt1  4790  rnxpid  4973  iotaval  5099  elabrex  5659  opabex3d  6019  opabex3  6020  enq0ref  7241  setindis  13165  bdsetindis  13167