Theorem equcoms 1730

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 1726	. 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 1471  ax-ie2 1516  ax-8 1526  ax-17 1548  ax-i9 1552

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equtr  1731  equtr2  1733  equequ2  1735  ax10o  1737  cbvalv1  1773  cbvexv1  1774  cbvalh  1775  cbvexh  1777  equvini  1780  stdpc7  1792  sbequ12r  1794  sbequ12a  1795  sbequ  1862  sb6rf  1875  cbvalvw  1942  cbvexvw  1943  sb9v  2005  sb6a  2015  mo2n  2081  elequ1  2179  elequ2  2180  cleqh  2304  cbvab  2328  sbralie  2755  reu8  2968  sbcco2  3020  snnex  4494  tfisi  4634  opeliunxp  4729  elrnmpt1  4928  rnxpid  5116  iotaval  5242  elabrex  5825  elabrexg  5826  opabex3d  6205  opabex3  6206  enq0ref  7545  fproddivapf  11884  setindis  15836  bdsetindis  15838