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

Definition df-tru 1315
Description: Definition of  T., a tautology.  T. is a constant true. In this definition biid 229 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  |-  (  T.  <->  (
ph 
<-> 
ph ) )

Detailed syntax breakdown of Definition df-tru
StepHypRef Expression
1 wtru 1312 . 2  wff  T.
2 wph . . 3  wff  ph
32, 2wb 178 . 2  wff  ( ph  <->  ph )
41, 3wb 178 1  wff  (  T.  <->  (
ph 
<-> 
ph ) )
Colors of variables: wff set class
This definition is referenced by:  tru  1317  tru2OLD  1318  altdftru  24113  uunT1  27245
  Copyright terms: Public domain W3C validator