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	|- ((-. ph -> ph) -> ph)

Proof of Theorem pm2.18

Step	Hyp	Ref	Expression
1		pm2.21 71	. . . 4 |- (-. ph -> (ph -> -. (-. ph -> ph)))
2	1	a2i 8	. . 3 |- ((-. ph -> ph) -> (-. ph -> -. (-. ph -> ph)))
3	2	a3d 70	. 2 |- ((-. ph -> ph) -> ((-. ph -> ph) -> ph))
4	3	pm2.43i 58	1 |- ((-. ph -> ph) -> ph)

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