Theorem equcoms 1667

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 1663	. 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)
2		equcoms.1	. 2 ⊢ (𝑥 = 𝑦 → 𝜑)
3	1, 2	syl 14	1 ⊢ (𝑦 = 𝑥 → 𝜑)

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-gen 1408  ax-ie2 1453  ax-8 1465  ax-17 1489  ax-i9 1493

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  equtr  1668  equtr2  1670  equequ2  1672  elequ1  1673  elequ2  1674  ax10o  1676  cbvalh  1709  cbvexh  1711  equvini  1714  stdpc7  1726  sbequ12r  1728  sbequ12a  1729  sbequ  1794  sb6rf  1807  sb9v  1929  sb6a  1939  mo2n  2003  cleqh  2214  cbvab  2237  sbralie  2641  reu8  2849  sbcco2  2900  snnex  4329  tfisi  4461  opeliunxp  4554  elrnmpt1  4750  rnxpid  4931  iotaval  5057  elabrex  5613  opabex3d  5973  opabex3  5974  enq0ref  7186  setindis  12849  bdsetindis  12851