Theorem pm2.01 617

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

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-in1 615

This theorem is referenced by:  pm2.01d  619  con2d  625  pm2.65i  640  pm4.8  708  notnotsnex  4220