ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm2.27 GIF 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 (𝜑 → ((𝜑𝜓) → 𝜓))

Proof of Theorem pm2.27
StepHypRef Expression
1 id 19 . 2 ((𝜑𝜓) → (𝜑𝜓))
21com12 30 1 (𝜑 → ((𝜑𝜓) → 𝜓))
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  344  pm3.2im  611  mth8  624  pm2.65  633  annimim  660  condcOLD  824  pm2.26dc  877  ax10o  1678  issref  4891  acexmidlem2  5739  findcard2  6751  findcard2s  6752  xpfi  6786  txlm  12375  bj-inf2vnlem1  13095  bj-findis  13104
  Copyright terms: Public domain W3C validator