MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  equcoms Unicode version

Theorem equcoms 1651
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
StepHypRef Expression
1 equcomi 1646 . 2  |-  ( y  =  x  ->  x  =  y )
2 equcoms.1 . 2  |-  ( x  =  y  ->  ph )
31, 2syl 15 1  |-  ( y  =  x  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  equtr  1652  equtr2  1654  ax12b  1655  ax12bOLD  1656  spfw  1657  spw  1660  cbvalw  1675  cbvalvw  1676  alcomiw  1678  elequ1  1687  elequ2  1689  stdpc7  1858  sbequ12r  1861  sbequ12a  1862  ax12olem1  1868  ax10o  1892  cbval  1924  equvini  1927  sbequ  2000  sb6rf  2031  sb6a  2055  ax12  2095  ax10o-o  2142  mo  2165  cleqh  2380  cbvab  2401  reu8  2961  tfinds2  4654  boxriin  6858  elirrv  7311  elmptrab  17522  pcoass  18522  cvmsss2  23805  ax13dfeq  24155  dominc  25280  rninc  25281  pdiveql  26168  sdclem2  26452  rexzrexnn0  26885  bnj1014  28992
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643
  Copyright terms: Public domain W3C validator