Mathbox for BJ 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > Mathboxes > bjnimn  Structured version Unicode version 
Description: If a formula is true, then it does not imply its negation. (Contributed by BJ, 19Mar2020.) A shorter proof is possible using id 22 and jc 150, however, the present proof uses theorems that are more basic than jc 150. (Proof modification is discouraged.) 
Ref  Expression 

bjnimn 
Step  Hyp  Ref  Expression 

1  pm2.01 171  . 2  
2  1  con2i 123  1 
Colors of variables: wff setvar class 
Syntax hints: wn 3 wi 4 
This theorem was proved from axioms: axmp 5 ax1 6 ax2 7 ax3 8 
This theorem is referenced by: bjnimni 31144 
Copyright terms: Public domain  W3C validator 