Theorem pm2.01 611

Description: Reductio ad absurdum. Theorem *2.01 of [WhiteheadRussell] p. 100. This is valid intuitionistically (in the terminology of Section 1.2 of [Bauer] p. 482 it is a proof of negation not a proof by contradiction); compare with pm2.18dc 850 which only holds for some propositions. Also called weak Clavius law. (Contributed by Mario Carneiro, 12-May-2015.)

Assertion

Ref	Expression
pm2.01	|- ( ( ph -> -. ph ) -> -. ph )

Proof of Theorem pm2.01

Step	Hyp	Ref	Expression
1		ax-in1 609	1 |- ( ( ph -> -. ph ) -> -. ph )

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-in1 609

This theorem is referenced by:  pm2.01d  613  con2d  619  pm2.65i  634  pm4.8  702  notnotsnex  4173