Theorem tru 44

Description: Tautology is provable. (Contributed by Mario Carneiro, 7-Oct-2014.)

Assertion

Ref	Expression
tru	⊢ ⊤⊧⊤

Proof of Theorem tru

Step	Hyp	Ref	Expression
1		wtru 43	. 2 ⊢ ⊤:∗
2	1	id 25	1 ⊢ ⊤⊧⊤

This proof depends on syntax axioms:  ⊤kt 8  ⊧wffMMJ2 11

This proof depends on axioms:  ax-id 24  ax-cb1 29  ax-weq 40  ax-refl 42

This theorem is used by:  eqtru  86