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  345  pm3.2im  632  jcn  646  pm2.65  654  annimim  681  condcOLD  849  pm2.26dc  902  ax10o  1708  issref  4993  acexmidlem2  5850  findcard2  6867  findcard2s  6868  xpfi  6907  exmidontriim  7202  pcmptcl  12294  txlm  13073  bj-inf2vnlem1  14005  bj-findis  14014
  Copyright terms: Public domain W3C validator