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

Theorem equcoms 1688
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 1686 . 2  |-  ( y  =  x  ->  x  =  y )
2 equcoms.1 . 2  |-  ( x  =  y  ->  ph )
31, 2syl 16 1  |-  ( y  =  x  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  equtr  1689  equtr2  1695  ax12b  1696  ax12bOLD  1697  spfw  1698  spw  1701  cbvalw  1708  cbvalvw  1709  alcomiw  1711  elequ1  1720  elequ2  1722  19.8a  1754  stdpc7  1931  sbequ12r  1934  sbequ12a  1935  a9e  1941  ax12OLD  1974  ax10o  1991  cbval  2019  equvini  2022  sbequ  2093  sb6rf  2124  sb6a  2150  ax12from12o  2190  ax10o-o  2237  mo  2260  cleqh  2484  cbvab  2505  reu8  3073  sbcco2  3127  snnex  4653  tfisi  4778  tfinds2  4783  opeliunxp  4869  elrnmpt1  5059  iotaval  5369  elabrex  5924  opabex3d  5928  opabex3  5929  boxriin  7040  ixpiunwdom  7492  elirrv  7498  imasvscafn  13689  ptbasfi  17534  elmptrab  17780  pcoass  18920  iundisj2  19310  dchrisumlema  21049  dchrisumlem2  21051  cusgrafilem2  21355  iundisj2f  23873  iundisj2fi  23991  voliune  24379  volfiniune  24380  cvmsss2  24740  ax13dfeq  25179  sdclem2  26137  rexzrexnn0  26555  frgrancvvdeqlem9  27793  bnj1014  28669  ax10oNEW7  28814  cbvalwwAUX7  28855  equviniNEW7  28863  sbequNEW7  28915  sb6rfNEW7  28925  sb6aNEW7  28944  cbvalOLD7  29041
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682
This theorem depends on definitions:  df-bi 178  df-ex 1548
  Copyright terms: Public domain W3C validator