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  2999  sbcco2  3051  reu8nf  3110  snnex  4538  tfisi  4678  opeliunxp  4773  elrnmpt1  4974  rnxpid  5162  iotaval  5289  elabrex  5880  elabrexg  5881  opabex3d  6264  opabex3  6265  enq0ref  7616  fproddivapf  12137  setindis  16288  bdsetindis  16290