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  1800  cbvexv1  1801  cbvalh  1802  cbvexh  1804  equvini  1807  stdpc7  1819  sbequ12r  1821  sbequ12a  1822  sbequ  1889  sb6rf  1902  cbvalvw  1969  cbvexvw  1970  sb9v  2032  sb6a  2042  mo2n  2108  elequ1  2207  elequ2  2208  cleqh  2332  cbvab  2358  sbralie  2796  reu8  3013  sbcco2  3065  reu8nf  3124  snnex  4569  tfisi  4709  opeliunxp  4805  elrnmpt1  5008  rnxpid  5197  iotaval  5324  elabrex  5930  elabrexg  5931  opabex3d  6314  opabex3  6315  enq0ref  7748  fproddivapf  12317  setindis  16737  bdsetindis  16739