Intuitionistic Logic Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > ILE Home > Th. List > pm2.01  Structured version Unicode version 
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 749 which only holds for some propositions. (Contributed by Mario Carneiro, 12May2015.) 
Ref  Expression 

pm2.01 
Step  Hyp  Ref  Expression 

1  axin1 544  1 
Colors of variables: wff set class 
Syntax hints: wn 3 wi 4 
This theorem was proved from axioms: axin1 544 
This theorem is referenced by: pm2.01d 548 con2d 554 pm2.65i 567 pm4.8 622 
Copyright terms: Public domain  W3C validator 