Theorem equcoms 1732

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 1728	. 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 1473  ax-ie2 1518  ax-8 1528  ax-17 1550  ax-i9 1554

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equtr  1733  equtr2  1735  equequ2  1737  ax10o  1739  cbvalv1  1775  cbvexv1  1776  cbvalh  1777  cbvexh  1779  equvini  1782  stdpc7  1794  sbequ12r  1796  sbequ12a  1797  sbequ  1864  sb6rf  1877  cbvalvw  1944  cbvexvw  1945  sb9v  2007  sb6a  2017  mo2n  2083  elequ1  2181  elequ2  2182  cleqh  2306  cbvab  2330  sbralie  2757  reu8  2973  sbcco2  3025  snnex  4508  tfisi  4648  opeliunxp  4743  elrnmpt1  4943  rnxpid  5131  iotaval  5257  elabrex  5844  elabrexg  5845  opabex3d  6224  opabex3  6225  enq0ref  7576  fproddivapf  12027  setindis  16072  bdsetindis  16074