Theorem equcoms 1731

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 1727	. 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 1472  ax-ie2 1517  ax-8 1527  ax-17 1549  ax-i9 1553

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equtr  1732  equtr2  1734  equequ2  1736  ax10o  1738  cbvalv1  1774  cbvexv1  1775  cbvalh  1776  cbvexh  1778  equvini  1781  stdpc7  1793  sbequ12r  1795  sbequ12a  1796  sbequ  1863  sb6rf  1876  cbvalvw  1943  cbvexvw  1944  sb9v  2006  sb6a  2016  mo2n  2082  elequ1  2180  elequ2  2181  cleqh  2305  cbvab  2329  sbralie  2756  reu8  2969  sbcco2  3021  snnex  4495  tfisi  4635  opeliunxp  4730  elrnmpt1  4929  rnxpid  5117  iotaval  5243  elabrex  5826  elabrexg  5827  opabex3d  6206  opabex3  6207  enq0ref  7546  fproddivapf  11942  setindis  15903  bdsetindis  15905