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  1834  tfinds  4541  tfindsg  4542  issref  4963  smogt  6270  findcard2  6983  findcard3  6985  fisupg  6990  xpfi  7013  dffi2  7060  cantnfle  7256  ac5num  7547  pwsdompw  7714  cfsmolem  7780  axcc4  7949  axdc3lem2  7961  fpwwe2lem8  8139  pwfseqlem3  8162  tskord  8282  grudomon  8319  grur1a  8321  xrub  10508  pcmptcl  12813  restntr  16744  cmpsublem  16958  cmpsub  16959  txlm  17174  ptcmplem3  17580  c1lip1  19176  wilthlem3  20140  dmdbr5  22718  waj-ax  24027  lukshef-ax2  24028  osneisi  24697  bwt2  24758  pgapspf2  25219  bsstr  25294  nbssntr  25295  sgplpte21d1  25305  sgplpte21d2  25306  filbcmb  25598  ax4567to6  26770  ax4567to7  26771  ax10-16  26773  a9e2nd  27114  elex22VD  27402  exbiriVD  27417  ssralv2VD  27429  truniALTVD  27441  trintALTVD  27443  onfrALTVD  27454  hbimpgVD  27467  a9e2eqVD  27470  a9e2ndVD  27471  ax10lem23X  27996  ax10lem24X  27997  ax10lem17ALT  28027  ax9lem17  28060
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-mp 10
  Copyright terms: Public domain W3C validator