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

---

Theorem trud 27

Description: Deduction form of tru 41.

Hypothesis

Ref	Expression
ax-trud.1

Assertion

Ref	Expression
trud

---

Proof of Theorem trud

Step	Hyp	Ref	Expression
1		ax-trud.1	. 2
2	1	ax-trud 26	1

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

Copyright terms: Public domain

W3C validator