Theorem equcoms 1760

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 1756	. 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 1502  ax-ie2 1547  ax-8 1557  ax-17 1579  ax-i9 1583

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equtr  1761  equtr2  1763  equequ2  1765  ax10o  1767  cbvalv1  1804  cbvexv1  1805  cbvalh  1806  cbvexh  1808  equvini  1811  stdpc7  1823  sbequ12r  1825  sbequ12a  1826  sbequ  1893  sb6rf  1906  cbvalvw  1975  cbvexvw  1976  sb9v  2038  sb6a  2048  mo2n  2114  elequ1  2213  elequ2  2214  cleqh  2338  cbvab  2364  sbralie  2804  reu8  3022  sbcco2  3074  reu8nf  3133  snnex  4592  tfisi  4732  opeliunxp  4828  elrnmpt1  5031  rnxpid  5220  iotaval  5347  elabrex  5957  elabrexg  5958  opabex3d  6344  opabex3  6345  enq0ref  7794  fproddivapf  12381  setindis  16976  bdsetindis  16978