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	⊢ ((𝜑 → ¬ 𝜑) → ¬ 𝜑)

Proof of Theorem pm2.01

Step	Hyp	Ref	Expression
1		ax-in1 615	1 ⊢ ((𝜑 → ¬ 𝜑) → ¬ 𝜑)

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