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

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜓))
2	1	com12 30	1 ⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓))

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  633  jcn  647  pm2.65  655  annimim  682  condcOLD  850  pm2.26dc  903  ax10o  1709  issref  4995  acexmidlem2  5854  findcard2  6871  findcard2s  6872  xpfi  6911  exmidontriim  7206  pcmptcl  12298  txlm  13158  bj-inf2vnlem1  14090  bj-findis  14099