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 1498  ax-ie2 1543  ax-8 1553  ax-17 1575  ax-i9 1579

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  2356  sbralie  2786  reu8  3003  sbcco2  3055  reu8nf  3114  snnex  4551  tfisi  4691  opeliunxp  4787  elrnmpt1  4989  rnxpid  5178  iotaval  5305  elabrex  5908  elabrexg  5909  opabex3d  6292  opabex3  6293  enq0ref  7696  fproddivapf  12255  setindis  16666  bdsetindis  16668