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

Theorem pm2.27 35
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 19 . 2  |-  ( (
ph  ->  ps )  -> 
( ph  ->  ps )
)
21com12 27 1  |-  ( ph  ->  ( ( ph  ->  ps )  ->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  pm2.43  47  com23  72  pm3.2im  137  mth8  138  biimt  325  pm3.35  570  pm2.26  853  dvelimv  1892  ax10lem6  1896  ax10o  1905  ax10-16  2142  ax10o-o  2155  tfinds  4666  tfindsg  4667  issref  5072  smogt  6400  findcard2  7114  findcard3  7116  fisupg  7121  xpfi  7144  dffi2  7192  cantnfle  7388  ac5num  7679  pwsdompw  7846  cfsmolem  7912  axcc4  8081  axdc3lem2  8093  fpwwe2lem8  8275  pwfseqlem3  8298  tskord  8418  grudomon  8455  grur1a  8457  xrub  10646  pcmptcl  12955  restntr  16928  cmpsublem  17142  cmpsub  17143  txlm  17358  ptcmplem3  17764  c1lip1  19360  wilthlem3  20324  dmdbr5  22904  waj-ax  24925  lukshef-ax2  24926  osneisi  25634  bwt2  25695  pgapspf2  26156  bsstr  26231  nbssntr  26232  sgplpte21d1  26242  sgplpte21d2  26243  filbcmb  26535  ax4567to6  27707  ax4567to7  27708  a9e2nd  28623  elex22VD  28931  exbiriVD  28946  ssralv2VD  28958  truniALTVD  28970  trintALTVD  28972  onfrALTVD  28983  hbimpgVD  28996  a9e2eqVD  28999  a9e2ndVD  29000  dvelimvNEW7  29439  ax10oNEW7  29453  ax10lem17ALT  29745  ax9lem17  29778
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator