Theorem equcoms 1719

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 1715	. 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-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1460  ax-ie2 1505  ax-8 1515  ax-17 1537  ax-i9 1541

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equtr  1720  equtr2  1722  equequ2  1724  ax10o  1726  cbvalv1  1762  cbvexv1  1763  cbvalh  1764  cbvexh  1766  equvini  1769  stdpc7  1781  sbequ12r  1783  sbequ12a  1784  sbequ  1851  sb6rf  1864  cbvalvw  1931  cbvexvw  1932  sb9v  1990  sb6a  2000  mo2n  2066  elequ1  2164  elequ2  2165  cleqh  2289  cbvab  2313  sbralie  2736  reu8  2948  sbcco2  3000  snnex  4466  tfisi  4604  opeliunxp  4699  elrnmpt1  4896  rnxpid  5081  iotaval  5207  elabrex  5778  elabrexg  5779  opabex3d  6145  opabex3  6146  enq0ref  7461  fproddivapf  11670  setindis  15172  bdsetindis  15174