Definition df-tru 1319

Description: Definition of T., a tautology. T. 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	|- ( T. <-> (ph <-> ph))

Detailed syntax breakdown of Definition df-tru

Step	Hyp	Ref	Expression
1		wtru 1316	. 2 wff T.
2		wph	. . 3 wff ph
3	2, 2	wb 176	. 2 wff (ph <-> ph)
4	1, 3	wb 176	1 wff ( T. <-> (ph <-> ph))

This definition is referenced by:  tru  1321