Definition df-tru 1537

Description: Definition of T., a tautology. T. is a constant true. In this definition biid 240 is used as an antecedent, however, any true wff, such as an axiom, can be used in its place.

Assertion

Ref	Expression
df-tru	|- ( T. <-> (ph <-> ph))

Detailed syntax breakdown of Definition df-tru

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

This definition is referenced by:  tru 1539  TTBid 14820  FFBid 14823  altdftru 14983

Copyright terms: Public domain