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  1879  ax10lem6  1883  ax10o  1892  ax10-16  2129  ax10o-o  2142  tfinds  4650  tfindsg  4651  issref  5056  smogt  6384  findcard2  7098  findcard3  7100  fisupg  7105  xpfi  7128  dffi2  7176  cantnfle  7372  ac5num  7663  pwsdompw  7830  cfsmolem  7896  axcc4  8065  axdc3lem2  8077  fpwwe2lem8  8259  pwfseqlem3  8282  tskord  8402  grudomon  8439  grur1a  8441  xrub  10630  pcmptcl  12939  restntr  16912  cmpsublem  17126  cmpsub  17127  txlm  17342  ptcmplem3  17748  c1lip1  19344  wilthlem3  20308  dmdbr5  22888  waj-ax  24853  lukshef-ax2  24854  osneisi  25531  bwt2  25592  pgapspf2  26053  bsstr  26128  nbssntr  26129  sgplpte21d1  26139  sgplpte21d2  26140  filbcmb  26432  ax4567to6  27604  ax4567to7  27605  a9e2nd  28324  elex22VD  28615  exbiriVD  28630  ssralv2VD  28642  truniALTVD  28654  trintALTVD  28656  onfrALTVD  28667  hbimpgVD  28680  a9e2eqVD  28683  a9e2ndVD  28684  ax10lem17ALT  29123  ax9lem17  29156
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator