Theorem equcoms 1722

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 1718	. 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 1463  ax-ie2 1508  ax-8 1518  ax-17 1540  ax-i9 1544

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equtr  1723  equtr2  1725  equequ2  1727  ax10o  1729  cbvalv1  1765  cbvexv1  1766  cbvalh  1767  cbvexh  1769  equvini  1772  stdpc7  1784  sbequ12r  1786  sbequ12a  1787  sbequ  1854  sb6rf  1867  cbvalvw  1934  cbvexvw  1935  sb9v  1997  sb6a  2007  mo2n  2073  elequ1  2171  elequ2  2172  cleqh  2296  cbvab  2320  sbralie  2747  reu8  2960  sbcco2  3012  snnex  4484  tfisi  4624  opeliunxp  4719  elrnmpt1  4918  rnxpid  5105  iotaval  5231  elabrex  5807  elabrexg  5808  opabex3d  6187  opabex3  6188  enq0ref  7517  fproddivapf  11813  setindis  15697  bdsetindis  15699