Theorem pm2.01 606

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

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-in1 604

This theorem is referenced by:  pm2.01d  608  con2d  614  pm2.65i  629  pm4.8  697  notnotsnex  4166