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

Theorem equcoms 1652
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 1647 . 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  1653  equtr2  1655  ax12b  1656  ax12bOLD  1657  spfw  1658  spw  1661  cbvalw  1676  cbvalvw  1677  alcomiw  1679  elequ1  1688  elequ2  1690  stdpc7  1860  sbequ12r  1863  sbequ12a  1864  ax12olem1  1870  ax10o  1894  cbval  1927  equvini  1930  sbequ  1999  sb6rf  2030  sb6a  2058  ax12  2097  ax10o-o  2143  mo  2166  cleqh  2381  cbvab  2402  reu8  2962  tfinds2  4653  boxriin  6854  elirrv  7307  elmptrab  17518  pcoass  18518  cvmsss2  23212  ax13dfeq  23559  dominc  24691  rninc  24692  pdiveql  25579  sdclem2  25863  rexzrexnn0  26296  bnj1014  28271
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 1636  ax-8 1644
  Copyright terms: Public domain W3C validator