Theorem equcoms 1719

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 1715	. 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 1460  ax-ie2 1505  ax-8 1515  ax-17 1537  ax-i9 1541

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equtr  1720  equtr2  1722  equequ2  1724  ax10o  1726  cbvalv1  1762  cbvexv1  1763  cbvalh  1764  cbvexh  1766  equvini  1769  stdpc7  1781  sbequ12r  1783  sbequ12a  1784  sbequ  1851  sb6rf  1864  cbvalvw  1931  cbvexvw  1932  sb9v  1994  sb6a  2004  mo2n  2070  elequ1  2168  elequ2  2169  cleqh  2293  cbvab  2317  sbralie  2744  reu8  2956  sbcco2  3008  snnex  4479  tfisi  4619  opeliunxp  4714  elrnmpt1  4913  rnxpid  5100  iotaval  5226  elabrex  5800  elabrexg  5801  opabex3d  6173  opabex3  6174  enq0ref  7493  fproddivapf  11774  setindis  15459  bdsetindis  15461