trud - Higher-Order Logic Explorer

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

Theorem trud 27

Description: Deduction form of tru 41.

**Hypothesis**
Ref	Expression
ax-trud.1	⊢ R:∗

**Assertion**
Ref	Expression
trud	⊢ R⊧⊤

**Proof of Theorem trud**
Step	Hyp	Ref	Expression
1		ax-trud.1	. 2 ⊢ R:∗
2	1	ax-trud 26	1 ⊢ R⊧⊤

Colors of variables: type var term

Syntax hints: ∗hb 3 ⊤kt 8 ⊧wffMMJ2 11 wffMMJ2t 12

This theorem was proved from axioms: ax-trud 26

This theorem is referenced by: trul 37 hbov 101 ax4g 139 dfan2 144 hbct 145 axun 209