Theorem pm2.18 81

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 76	. . . 4 |- (-. ph -> (ph -> -. (-. ph -> ph)))
2	1	a2i 9	. . 3 |- ((-. ph -> ph) -> (-. ph -> -. (-. ph -> ph)))
3	2	a3d 75	. 2 |- ((-. ph -> ph) -> ((-. ph -> ph) -> ph))
4	3	pm2.43i 64	1 |- ((-. ph -> ph) -> ph)

Syntax hints:  -. wn 2   -> wi 3

This theorem is referenced by:  peirce 82  nega 84  pm2.01 88  pm2.61 124  pm2.61-ocatOLD 125  pm4.81 163  oridm 243  oplem1 770  hbequid 1165  sumdmdlem2 10253

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

Copyright terms: Public domain