NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-tru Structured version   Unicode version

Definition df-tru 1319
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, 13-Oct-2010.)
Assertion
Ref Expression
df-tru

Detailed syntax breakdown of Definition df-tru
StepHypRef Expression
1 wtru 1316 . 2
2 wph . . 3
32, 2wb 176 . 2
41, 3wb 176 1
Colors of variables: wff set class
This definition is referenced by:  tru  1321
  Copyright terms: Public domain W3C validator