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  1971  cbvexvw  1972  sb9v  2034  sb6a  2044  mo2n  2110  elequ1  2209  elequ2  2210  cleqh  2334  cbvab  2360  sbralie  2798  reu8  3016  sbcco2  3068  reu8nf  3127  snnex  4574  tfisi  4714  opeliunxp  4810  elrnmpt1  5013  rnxpid  5202  iotaval  5329  elabrex  5936  elabrexg  5937  opabex3d  6323  opabex3  6324  enq0ref  7764  fproddivapf  12342  setindis  16863  bdsetindis  16865