Intuitionistic Logic Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > ILE Home > Th. List > pm2.01  GIF version 
Description: Reductio ad absurdum. Theorem *2.01 of [WhiteheadRussell] p. 100. This is valid intuitionistically (in the terminology of [Bauer] p. 482 it is a proof of negation not a proof by contradiction); compare with pm2.18 722 which is not. (Contributed by Mario Carneiro, 12May2015.) 
Ref  Expression 

pm2.01  ⊢ ((φ → ¬ φ) → ¬ φ) 
Step  Hyp  Ref  Expression 

1  axin1 526  1 ⊢ ((φ → ¬ φ) → ¬ φ) 
Colors of variables: wff set class 
Syntax hints: ¬ wn 3 → wi 4 
This theorem is referenced by: pm2.01d 530 con2d 535 pm2.65i 546 pm4.8 601 
This theorem was proved from axioms: axin1 526 
Copyright terms: Public domain  W3C validator 