Theorem equcoms 1591

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	⊢ (x = y → φ)

Assertion

Ref	Expression
equcoms	⊢ (y = x → φ)

Proof of Theorem equcoms

Step	Hyp	Ref	Expression
1		equcomi 1589	. 2 ⊢ (y = x → x = y)
2		equcoms.1	. 2 ⊢ (x = y → φ)
3	1, 2	syl 14	1 ⊢ (y = x → φ)

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-gen 1335  ax-ie2 1380  ax-8 1392  ax-17 1416  ax-i9 1420

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  equtr  1592  equtr2  1594  equequ2  1596  elequ1  1597  elequ2  1598  ax10o  1600  cbvalh  1633  cbvexh  1635  equvini  1638  stdpc7  1650  sbequ12r  1652  sbequ12a  1653  sbequ  1718  sb6rf  1730  sb9v  1851  sb6a  1861  mo2n  1925  cleqh  2134  cbvab  2157  reu8  2731  sbcco2  2780  snnex  4147  tfisi  4253  opeliunxp  4338  elrnmpt1  4528  rnxpid  4698  iotaval  4821  elabrex  5340  opabex3d  5690  opabex3  5691  enq0ref  6415  setindis  9397  bdsetindis  9399