ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm2.27 Unicode version

Theorem pm2.27 40
Description: This theorem, called "Assertion," can be thought of as closed form of modus ponens ax-mp 5. 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 30 1  |-  ( ph  ->  ( ( ph  ->  ps )  ->  ps )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  pm2.43  53  com23  78  biimt  240  pm3.35  342  pm3.2im  609  mth8  622  pm2.65  631  annimim  658  condcOLD  822  pm2.26dc  875  ax10o  1676  issref  4889  acexmidlem2  5737  findcard2  6749  findcard2s  6750  xpfi  6784  txlm  12343  bj-inf2vnlem1  12970  bj-findis  12979
  Copyright terms: Public domain W3C validator