New Foundations Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > NFE Home > Th. List > dftru  Unicode version 
Description: Definition of , a tautology. is a constant true. In this definition biid 227 is used as an antecedent, however, any true wff, such as an axiom, can be used in its place. (Contributed by Anthony Hart, 13Oct2010.) 
Ref  Expression 

dftru 
Step  Hyp  Ref  Expression 

1  wtru 1316  . 2  
2  wph  . . 3  
3  2, 2  wb 176  . 2 
4  1, 3  wb 176  1 
Colors of variables: wff set class 
This definition is referenced by: tru 1321 
Copyright terms: Public domain  W3C validator 