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  1951  sb6a  1961  mo2n  2025  cleqh  2237  cbvab  2261  sbralie  2665  reu8  2875  sbcco2  2926  snnex  4364  tfisi  4496  opeliunxp  4589  elrnmpt1  4785  rnxpid  4968  iotaval  5094  elabrex  5652  opabex3d  6012  opabex3  6013  enq0ref  7234  setindis  13154  bdsetindis  13156