Higher-Order Logic Explorer		< Previous   Next > Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  tru		Unicode version

---

Theorem tru 41

Description: Tautology is provable.

Assertion

Ref	Expression
tru

---

Proof of Theorem tru

Step	Hyp	Ref	Expression
1		wtru 40	. 2
2	1	id 25	1

Colors of variables: type var term

Syntax hints:  kt 8   wffMMJ2 11

This theorem was proved from axioms:  ax-id 24  ax-cb1 29  ax-refl 39

This theorem is referenced by:  eqtru  76

Copyright terms: Public domain

W3C validator