Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > tbt  Unicode version 
Description: A wff is equivalent to its equivalence with truth. (Contributed by NM, 18Aug1993.) (Proof shortened by Andrew Salmon, 13May2011.) 
Ref  Expression 

tbt.1 
Ref  Expression 

tbt 
Step  Hyp  Ref  Expression 

1  tbt.1  . 2  
2  ibibr 333  . . 3  
3  2  pm5.74ri 238  . 2 
4  1, 3  axmp 8  1 
Colors of variables: wff set class 
Syntax hints: wb 177 
This theorem is referenced by: tbtru 1330 exists1 2343 reu6 3083 eqv 3603 vprc 4301 elnev 27506 
This theorem was proved from axioms: ax1 5 ax2 6 ax3 7 axmp 8 
This theorem depends on definitions: dfbi 178 
Copyright terms: Public domain  W3C validator 