ax-trud - Higher-Order Logic Explorer

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

Axiom ax-trud 26

Description: Deduction form of tru 44. (Contributed by Mario Carneiro, 7-Oct-2014.)

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

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

**Detailed syntax breakdown of Axiom ax-trud**
Step	Hyp	Ref	Expression
1		tr	. 2 term R
2		kt 8	. 2 term ⊤
3	1, 2	wffMMJ2 11	1 wff R⊧⊤

Colors of variables: type var term

This axiom is referenced by: trud 27 a1i 28