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  642  jcn  657  pm2.65  665  annimim  692  condcOLD  861  pm2.26dc  914  ax10o  1763  issref  5119  fundif  5374  acexmidlem2  6015  findcard2  7078  findcard2s  7079  xpfi  7124  exmidontriim  7440  pcmptcl  12920  txlm  15009  bj-inf2vnlem1  16591  bj-findis  16600