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  241  pm3.35  347  pm3.2im  637  jcn  651  pm2.65  659  annimim  686  condcOLD  854  pm2.26dc  907  ax10o  1715  issref  5013  acexmidlem2  5874  findcard2  6891  findcard2s  6892  xpfi  6931  exmidontriim  7226  pcmptcl  12342  txlm  13818  bj-inf2vnlem1  14761  bj-findis  14770
  Copyright terms: Public domain W3C validator