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  1994  sb6a  2004  mo2n  2070  elequ1  2168  elequ2  2169  cleqh  2293  cbvab  2317  sbralie  2744  reu8  2957  sbcco2  3009  snnex  4480  tfisi  4620  opeliunxp  4715  elrnmpt1  4914  rnxpid  5101  iotaval  5227  elabrex  5801  elabrexg  5802  opabex3d  6175  opabex3  6176  enq0ref  7495  fproddivapf  11777  setindis  15529  bdsetindis  15531