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

Theorem equcoms 1696
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 1694 . 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  1697  equtr2  1703  ax12b  1704  ax12bOLD  1705  spfw  1706  spwOLD  1710  cbvalw  1717  cbvalvwOLD  1719  alcomiw  1721  elequ1  1731  elequ2  1733  19.8a  1765  stdpc7  1946  sbequ12r  1949  sbequ12a  1950  a9e  1956  cbval  1986  ax12OLD  2024  ax10oOLD  2043  equvini  2087  equviniOLD  2088  sbequi  2115  sbequ  2116  sb6rf  2174  sb6a  2200  ax12from12o  2240  ax10o-o  2287  mo  2310  cleqh  2540  cbvab  2561  reu8  3139  sbcco2  3193  snnex  4748  tfisi  4873  tfinds2  4878  opeliunxp  4964  elrnmpt1  5154  iotaval  5464  elabrex  6021  opabex3d  6025  opabex3  6026  boxriin  7140  ixpiunwdom  7595  elirrv  7601  imasvscafn  13800  ptbasfi  17651  elmptrab  17897  pcoass  19087  iundisj2  19481  dchrisumlema  21220  dchrisumlem2  21222  cusgrafilem2  21527  iundisj2f  24065  iundisj2fi  24188  voliune  24620  volfiniune  24621  cvmsss2  24996  ax13dfeq  25461  mblfinlem2  26284  sdclem2  26488  rexzrexnn0  26976  frgrancvvdeqlem9  28602  bnj1014  29505  ax10oNEW7  29650  cbvalwwAUX7  29693  equviniNEW7  29701  sbequNEW7  29754  sb6rfNEW7  29766  sb6aNEW7  29785  cbvalOLD7  29899
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690
This theorem depends on definitions:  df-bi 179  df-ex 1552
  Copyright terms: Public domain W3C validator