MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-tru Unicode version

Definition df-tru 1355
Description: Definition of the truth value "true", or "verum", denoted by . This is a tautology, as proved by tru 1357. In this definition, biid 230 is used as the definiens, although any tautology, such as an axiom, can be used in its place. This definition should be referenced directly only by tru 1357, and other proofs should depend on tru 1357 (directly or indirectly) instead of this definition, since there are many alternative ways to define . (Contributed by Anthony Hart, 13-Oct-2010.) (New usage is discouraged.)
Assertion
Ref Expression
df-tru

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