Theorem pm2.27 62

Description: This theorem, called "Assertion," can be thought of as closed form of modus ponens. Theorem *2.27 of [WhiteheadRussell] p. 104.

Assertion

Ref	Expression
pm2.27	⊢ (φ → ((φ → ψ) → ψ))

Proof of Theorem pm2.27

Step	Hyp	Ref	Expression
1		id 59	. 2 ⊢ ((φ → ψ) → (φ → ψ))
2	1	com12 11	1 ⊢ (φ → ((φ → ψ) → ψ))

Syntax hints:   → wi 3

This theorem is referenced by:  pm2.43 63  pm3.2im 122  mth8 123  a1bi 197  pm3.35 359  pm2.75 573  biimt 730  meredith 923  ax10o 1138  r19.27av 1752  vtoclegft 1853  tfindsg 3158  xrub 6037  caun0 7907  bcthlem2 7962  dmdbr5 10191  efilcp 10504  efilcp2 10509

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain