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

Theorem equcoms 1689
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 1687 . 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  1690  equtr2  1696  ax12b  1697  ax12bOLD  1698  spfw  1699  spwOLD  1703  cbvalw  1710  cbvalvwOLD  1712  alcomiw  1714  elequ1  1724  elequ2  1726  19.8a  1758  stdpc7  1938  sbequ12r  1941  sbequ12a  1942  a9e  1948  ax12OLD  1986  ax10o  2001  cbval  2037  equvini  2040  equviniOLD  2041  sbequ  2109  sb6rf  2140  sb6a  2166  ax12from12o  2206  ax10o-o  2253  mo  2276  cleqh  2501  cbvab  2522  reu8  3090  sbcco2  3144  snnex  4672  tfisi  4797  tfinds2  4802  opeliunxp  4888  elrnmpt1  5078  iotaval  5388  elabrex  5944  opabex3d  5948  opabex3  5949  boxriin  7063  ixpiunwdom  7515  elirrv  7521  imasvscafn  13717  ptbasfi  17566  elmptrab  17812  pcoass  19002  iundisj2  19396  dchrisumlema  21135  dchrisumlem2  21137  cusgrafilem2  21442  iundisj2f  23983  iundisj2fi  24106  voliune  24538  volfiniune  24539  cvmsss2  24914  ax13dfeq  25369  mblfinlem  26143  sdclem2  26336  rexzrexnn0  26754  frgrancvvdeqlem9  28144  bnj1014  29037  ax10oNEW7  29182  cbvalwwAUX7  29223  equviniNEW7  29231  sbequNEW7  29283  sb6rfNEW7  29293  sb6aNEW7  29312  cbvalOLD7  29409
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 1662  ax-8 1683
This theorem depends on definitions:  df-bi 178  df-ex 1548
  Copyright terms: Public domain W3C validator