Theorem equcoms 1570

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 1568	. 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 1314  ax-ie2 1359  ax-8 1371  ax-17 1395  ax-i9 1399

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  equtr  1571  equtr2  1573  equequ2  1575  elequ1  1576  elequ2  1577  ax10o  1579  cbvalh  1612  cbvexh  1614  equvini  1617  stdpc7  1629  sbequ12r  1631  sbequ12a  1632  sbequ  1697  sb6rf  1709  sb9v  1830  sb6a  1840  mo2n  1904  cleqh  2113  cbvab  2136  reu8  2708  sbcco2  2757  snnex  4122  tfisi  4228  opeliunxp  4313  elrnmpt1  4503  rnxpid  4673  iotaval  4796  elabrex  5313  opabex3d  5662  opabex3  5663  enq0ref  6277  setindis  8603  bdsetindis  8605