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 577  biimt 735  meredith 928  ax10o 1143  r19.27av 1761  vtoclegft 1863  tfindsg 3178  xrub 6112  caun0 7971  bcthlem2 8026  dmdbr5 10260  ref3w 10505  efilcp 10603  efilcp2 10608

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

Copyright terms: Public domain