Theorem equcoms 1756

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 1752	. 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 1498  ax-ie2 1543  ax-8 1553  ax-17 1575  ax-i9 1579

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equtr  1757  equtr2  1759  equequ2  1761  ax10o  1763  cbvalv1  1800  cbvexv1  1801  cbvalh  1802  cbvexh  1804  equvini  1807  stdpc7  1819  sbequ12r  1821  sbequ12a  1822  sbequ  1889  sb6rf  1902  cbvalvw  1971  cbvexvw  1972  sb9v  2034  sb6a  2044  mo2n  2110  elequ1  2209  elequ2  2210  cleqh  2334  cbvab  2360  sbralie  2798  reu8  3016  sbcco2  3068  reu8nf  3127  snnex  4575  tfisi  4715  opeliunxp  4811  elrnmpt1  5014  rnxpid  5203  iotaval  5330  elabrex  5937  elabrexg  5938  opabex3d  6324  opabex3  6325  enq0ref  7765  fproddivapf  12347  setindis  16878  bdsetindis  16880