Intuitionistic Logic Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > ILE Home > Th. List > tbtru  Structured version Unicode version 
Description: A proposition is equivalent to itself being equivalent to . (Contributed by Anthony Hart, 14Aug2011.) 
Ref  Expression 

tbtru 
Step  Hyp  Ref  Expression 

1  tru 1246  . 2  
2  1  tbt 236  1 
Colors of variables: wff set class 
Syntax hints: wb 98 wtru 1243 
This theorem was proved from axioms: ax1 5 ax2 6 axmp 7 axia1 99 axia2 100 axia3 101 
This theorem depends on definitions: dfbi 110 dftru 1245 
This theorem is referenced by: (None) 
Copyright terms: Public domain  W3C validator 