Theorem equcoms 1754

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 1750	. 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 1495  ax-ie2 1540  ax-8 1550  ax-17 1572  ax-i9 1576

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equtr  1755  equtr2  1757  equequ2  1759  ax10o  1761  cbvalv1  1797  cbvexv1  1798  cbvalh  1799  cbvexh  1801  equvini  1804  stdpc7  1816  sbequ12r  1818  sbequ12a  1819  sbequ  1886  sb6rf  1899  cbvalvw  1966  cbvexvw  1967  sb9v  2029  sb6a  2039  mo2n  2105  elequ1  2204  elequ2  2205  cleqh  2329  cbvab  2353  sbralie  2783  reu8  3000  sbcco2  3052  reu8nf  3111  snnex  4543  tfisi  4683  opeliunxp  4779  elrnmpt1  4981  rnxpid  5169  iotaval  5296  elabrex  5893  elabrexg  5894  opabex3d  6278  opabex3  6279  enq0ref  7643  fproddivapf  12182  setindis  16498  bdsetindis  16500