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

Theorem pm2.27 37
Description: This theorem, called "Assertion," can be thought of as closed form of modus ponens ax-mp 10. Theorem *2.27 of [WhiteheadRussell] p. 104. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
pm2.27  |-  ( ph  ->  ( ( ph  ->  ps )  ->  ps )
)

Proof of Theorem pm2.27
StepHypRef Expression
1 id 21 . 2  |-  ( (
ph  ->  ps )  -> 
( ph  ->  ps )
)
21com12 29 1  |-  ( ph  ->  ( ( ph  ->  ps )  ->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6
This theorem is referenced by:  pm2.43  49  com23  74  pm3.2im  139  mth8  140  biimt  327  pm3.35  573  pm2.26  858  ax10lem23  1672  ax10lem24  1673  ax10o  1835  tfinds  4622  tfindsg  4623  issref  5044  smogt  6352  findcard2  7066  findcard3  7068  fisupg  7073  xpfi  7096  dffi2  7144  cantnfle  7340  ac5num  7631  pwsdompw  7798  cfsmolem  7864  axcc4  8033  axdc3lem2  8045  fpwwe2lem8  8227  pwfseqlem3  8250  tskord  8370  grudomon  8407  grur1a  8409  xrub  10596  pcmptcl  12901  restntr  16874  cmpsublem  17088  cmpsub  17089  txlm  17304  ptcmplem3  17710  c1lip1  19306  wilthlem3  20270  dmdbr5  22848  waj-ax  24228  lukshef-ax2  24229  osneisi  24898  bwt2  24959  pgapspf2  25420  bsstr  25495  nbssntr  25496  sgplpte21d1  25506  sgplpte21d2  25507  filbcmb  25799  ax4567to6  26971  ax4567to7  26972  ax10-16  26974  a9e2nd  27377  elex22VD  27665  exbiriVD  27680  ssralv2VD  27692  truniALTVD  27704  trintALTVD  27706  onfrALTVD  27717  hbimpgVD  27730  a9e2eqVD  27733  a9e2ndVD  27734  ax10lem23X  28259  ax10lem24X  28260  ax10lem17ALT  28290  ax9lem17  28323
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-mp 10
  Copyright terms: Public domain W3C validator