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  241  pm3.35  347  pm3.2im  638  jcn  652  pm2.65  660  annimim  687  condcOLD  855  pm2.26dc  908  ax10o  1729  issref  5052  acexmidlem2  5919  findcard2  6950  findcard2s  6951  xpfi  6993  exmidontriim  7292  pcmptcl  12511  txlm  14515  bj-inf2vnlem1  15616  bj-findis  15625