Theorem equcoms 1576

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 1574	. 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 1318  ax-ie2 1364  ax-8 1376  ax-17 1400  ax-i9 1404

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  equtr  1577  equtr2  1579  equequ2  1581  elequ1  1582  elequ2  1583  ax10o  1585  cbvalh  1618  cbvexh  1620  equvini  1623  stdpc7  1635  sbequ12r  1637  sbequ12a  1638  sbequ  1703  sb6rf  1715  sb9v  1836  sb6a  1846  mo2n  1910  cleqh  2119  cbvab  2142  reu8  2714  sbcco2  2763  snnex  4131  tfisi  4237  opeliunxp  4322  elrnmpt1  4512  rnxpid  4682  iotaval  4805  elabrex  5322  opabex3d  5671  opabex3  5672  enq0ref  6288  setindis  7332  bdsetindis  7334