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  3015  sbcco2  3067  reu8nf  3126  snnex  4571  tfisi  4711  opeliunxp  4807  elrnmpt1  5010  rnxpid  5199  iotaval  5326  elabrex  5932  elabrexg  5933  opabex3d  6316  opabex3  6317  enq0ref  7753  fproddivapf  12325  setindis  16786  bdsetindis  16788