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

Proof of Theorem pm2.01

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

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