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

Theorem equcoms 1653
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 1648 . 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  1654  equtr2  1656  ax12b  1657  ax12bOLD  1658  spfw  1659  spw  1662  cbvalw  1677  cbvalvw  1678  alcomiw  1680  elequ1  1689  elequ2  1691  stdpc7  1860  sbequ12r  1863  sbequ12a  1864  ax12olem1  1870  ax10o  1894  cbval  1926  equvini  1929  sbequ  2002  sb6rf  2033  sb6a  2057  ax12  2097  ax10o-o  2144  mo  2167  cleqh  2382  cbvab  2403  reu8  2963  tfinds2  4656  boxriin  6860  elirrv  7313  elmptrab  17524  pcoass  18524  cvmsss2  23807  ax13dfeq  24157  dominc  25291  rninc  25292  pdiveql  26179  sdclem2  26463  rexzrexnn0  26896  bnj1014  29065
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645
  Copyright terms: Public domain W3C validator