Theorem pm2.18 75

Description: Proof by contradiction. Theorem *2.18 of [WhiteheadRussell] p. 103. Also called the Law of Clavius.

Assertion

Ref	Expression
pm2.18	⊢ ((¬ φ → φ) → φ)

Proof of Theorem pm2.18

Step	Hyp	Ref	Expression
1		pm2.21 71	. . . 4 ⊢ (¬ φ → (φ → ¬ (¬ φ → φ)))
2	1	a2i 8	. . 3 ⊢ ((¬ φ → φ) → (¬ φ → ¬ (¬ φ → φ)))
3	2	a3d 70	. 2 ⊢ ((¬ φ → φ) → ((¬ φ → φ) → φ))
4	3	pm2.43i 58	1 ⊢ ((¬ φ → φ) → φ)

Syntax hints:  ¬ wn 1   → wi 2

This theorem is referenced by:  peirce 76  nega 78  pm2.01 80  pm2.61 109  oridm 208  oplem1 578  sumdmd 5787

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

metamath.org