New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > df-tru | GIF 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, 13-Oct-2010.) |
Ref | Expression |
---|---|
df-tru | ⊢ ( ⊤ ↔ (φ ↔ φ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wtru 1316 | . 2 wff ⊤ | |
2 | wph | . . 3 wff φ | |
3 | 2, 2 | wb 176 | . 2 wff (φ ↔ φ) |
4 | 1, 3 | wb 176 | 1 wff ( ⊤ ↔ (φ ↔ φ)) |
Colors of variables: wff setvar class |
This definition is referenced by: tru 1321 |
Copyright terms: Public domain | W3C validator |