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 ⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  pm2.43  53  com23  78  biimt  241  pm3.35  347  pm3.2im  646  jcn  661  pm2.65  669  annimim  697  condcOLD  866  pm2.26dc  919  ax10o  1767  issref  5173  fundif  5428  acexmidlem2  6085  findcard2  7198  findcard2s  7199  xpfi  7244  exmidontriim  7588  pcmptcl  13151  txlm  15517  bj-inf2vnlem1  17213  bj-findis  17222