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  572  pm2.26  855  dvelimv  1880  ax10lem6  1884  ax10o  1893  ax10-16  2131  ax10o-o  2143  tfinds  4649  tfindsg  4650  issref  5055  smogt  6379  findcard2  7093  findcard3  7095  fisupg  7100  xpfi  7123  dffi2  7171  cantnfle  7367  ac5num  7658  pwsdompw  7825  cfsmolem  7891  axcc4  8060  axdc3lem2  8072  fpwwe2lem8  8254  pwfseqlem3  8277  tskord  8397  grudomon  8434  grur1a  8436  xrub  10624  pcmptcl  12933  restntr  16906  cmpsublem  17120  cmpsub  17121  txlm  17336  ptcmplem3  17742  c1lip1  19338  wilthlem3  20302  dmdbr5  22880  waj-ax  24260  lukshef-ax2  24261  osneisi  24930  bwt2  24991  pgapspf2  25452  bsstr  25527  nbssntr  25528  sgplpte21d1  25538  sgplpte21d2  25539  filbcmb  25831  ax4567to6  27003  ax4567to7  27004  a9e2nd  27595  elex22VD  27883  exbiriVD  27898  ssralv2VD  27910  truniALTVD  27922  trintALTVD  27924  onfrALTVD  27935  hbimpgVD  27948  a9e2eqVD  27951  a9e2ndVD  27952  ax10lem17ALT  28390  ax9lem17  28423
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-mp 10
  Copyright terms: Public domain W3C validator