Theorem equcoms 1641

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 1637	. 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 1383  ax-ie2 1428  ax-8 1440  ax-17 1464  ax-i9 1468

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  equtr  1642  equtr2  1644  equequ2  1646  elequ1  1647  elequ2  1648  ax10o  1650  cbvalh  1683  cbvexh  1685  equvini  1688  stdpc7  1700  sbequ12r  1702  sbequ12a  1703  sbequ  1768  sb6rf  1781  sb9v  1902  sb6a  1912  mo2n  1976  cleqh  2187  cbvab  2210  reu8  2811  sbcco2  2862  snnex  4271  tfisi  4402  opeliunxp  4493  elrnmpt1  4686  rnxpid  4865  iotaval  4991  elabrex  5537  opabex3d  5892  opabex3  5893  enq0ref  6992  setindis  11862  bdsetindis  11864