Theorem equcoms 1685

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 1681	. 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 105  ax-gen 1426  ax-ie2 1471  ax-8 1483  ax-17 1507  ax-i9 1511

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  equtr  1686  equtr2  1688  equequ2  1690  elequ1  1691  elequ2  1692  ax10o  1694  cbvalh  1727  cbvexh  1729  equvini  1732  stdpc7  1744  sbequ12r  1746  sbequ12a  1747  sbequ  1813  sb6rf  1826  sb9v  1954  sb6a  1964  mo2n  2028  cleqh  2240  cbvab  2264  sbralie  2673  reu8  2884  sbcco2  2935  snnex  4377  tfisi  4509  opeliunxp  4602  elrnmpt1  4798  rnxpid  4981  iotaval  5107  elabrex  5667  opabex3d  6027  opabex3  6028  enq0ref  7265  setindis  13336  bdsetindis  13338