Theorem trud 27

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

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⊧⊤

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  39  hbov  111  ax4g  149  dfan2  154  hbct  155  axun  222