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

Theorem pm2.27 37
Description: This theorem, called "Assertion," can be thought of as closed form of modus ponens ax-mp 8. 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 20 . 2  |-  ( (
ph  ->  ps )  -> 
( ph  ->  ps )
)
21com12 29 1  |-  ( ph  ->  ( ( ph  ->  ps )  ->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  pm2.43  49  com23  74  pm3.2im  139  mth8  140  biimt  326  pm3.35  571  pm2.26  854  ax10o2  2024  dvelimvOLD  2028  ax10oOLD  2039  ax10-16  2267  ax10o-o  2280  tfinds  4839  tfindsg  4840  issref  5247  smogt  6629  findcard2  7348  findcard3  7350  fisupg  7355  xpfi  7378  dffi2  7428  cantnfle  7626  ac5num  7917  pwsdompw  8084  cfsmolem  8150  axcc4  8319  axdc3lem2  8331  fpwwe2lem8  8512  pwfseqlem3  8535  tskord  8655  grudomon  8692  grur1a  8694  xrub  10890  pcmptcl  13260  restntr  17246  cmpsublem  17462  cmpsub  17463  bwth  17473  txlm  17680  ptcmplem3  18085  c1lip1  19881  wilthlem3  20853  dmdbr5  23811  wzel  25575  waj-ax  26164  lukshef-ax2  26165  mbfresfi  26253  filbcmb  26442  ax4567to6  27581  ax4567to7  27582  a9e2nd  28645  elex22VD  28951  exbiriVD  28966  ssralv2VD  28978  truniALTVD  28990  trintALTVD  28992  onfrALTVD  29003  hbimpgVD  29016  a9e2eqVD  29019  a9e2ndVD  29020  dvelimvNEW7  29462  ax10oNEW7  29476
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator