ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-tru GIF version

Definition df-tru 1201
Description: Definition of , a tautology. is a constant true. In this definition biid 158 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 1198 . 2 wff
2 wph . . 3 wff φ
32, 2wb 96 . 2 wff (φφ)
41, 3wb 96 1 wff ( ⊤ ↔ (φφ))
Colors of variables: wff set class
This definition is referenced by:  tru  1203
  Copyright terms: Public domain W3C validator