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  627  jcn  641  pm2.65  649  annimim  676  condcOLD  844  pm2.26dc  897  ax10o  1703  issref  4986  acexmidlem2  5839  findcard2  6855  findcard2s  6856  xpfi  6895  exmidontriim  7181  pcmptcl  12272  txlm  12919  bj-inf2vnlem1  13852  bj-findis  13861