Theorem equcoms 1635

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 -> ph )

Assertion

Ref	Expression
equcoms	|- ( y = x -> ph )

Proof of Theorem equcoms

Step	Hyp	Ref	Expression
1		equcomi 1633	. 2 |- ( y = x -> x = y )
2		equcoms.1	. 2 |- ( x = y -> ph )
3	1, 2	syl 14	1 |- ( y = x -> ph )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-gen 1379  ax-ie2 1424  ax-8 1436  ax-17 1460  ax-i9 1464

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  equtr  1636  equtr2  1638  equequ2  1640  elequ1  1641  elequ2  1642  ax10o  1644  cbvalh  1677  cbvexh  1679  equvini  1682  stdpc7  1694  sbequ12r  1696  sbequ12a  1697  sbequ  1762  sb6rf  1775  sb9v  1896  sb6a  1906  mo2n  1970  cleqh  2179  cbvab  2202  reu8  2789  sbcco2  2838  snnex  4207  tfisi  4336  opeliunxp  4421  elrnmpt1  4613  rnxpid  4785  iotaval  4908  elabrex  5429  opabex3d  5779  opabex3  5780  enq0ref  6685  setindis  10920  bdsetindis  10922