Theorem equcoms 1756

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 1752	. 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 1497  ax-ie2 1542  ax-8 1552  ax-17 1574  ax-i9 1578

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equtr  1757  equtr2  1759  equequ2  1761  ax10o  1763  cbvalv1  1799  cbvexv1  1800  cbvalh  1801  cbvexh  1803  equvini  1806  stdpc7  1818  sbequ12r  1820  sbequ12a  1821  sbequ  1888  sb6rf  1901  cbvalvw  1968  cbvexvw  1969  sb9v  2031  sb6a  2041  mo2n  2107  elequ1  2206  elequ2  2207  cleqh  2331  cbvab  2355  sbralie  2785  reu8  3002  sbcco2  3054  reu8nf  3113  snnex  4545  tfisi  4685  opeliunxp  4781  elrnmpt1  4983  rnxpid  5171  iotaval  5298  elabrex  5897  elabrexg  5898  opabex3d  6282  opabex3  6283  enq0ref  7652  fproddivapf  12191  setindis  16562  bdsetindis  16564