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  653  pm2.65  661  annimim  688  condcOLD  856  pm2.26dc  909  ax10o  1739  issref  5070  fundif  5323  acexmidlem2  5948  findcard2  6993  findcard2s  6994  xpfi  7036  exmidontriim  7344  pcmptcl  12709  txlm  14795  bj-inf2vnlem1  15980  bj-findis  15989