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

Theorem trul 37
Description: Deduction form of tru 41.
Hypothesis
Ref Expression
trul.1 |- (T., R) |= S
Assertion
Ref Expression
trul |- R |= S

Proof of Theorem trul
StepHypRef Expression
1 trul.1 . . . . 5 |- (T., R) |= S
21ax-cb1 29 . . . 4 |- (T., R):*
32wctr 32 . . 3 |- R:*
43trud 27 . 2 |- R |= T.
53id 25 . 2 |- R |= R
64, 5, 1syl2anc 19 1 |- R |= S
Colors of variables: type var term
Syntax hints:  T.kt 8  kct 10   |= wffMMJ2 11
This theorem was proved from axioms:  ax-syl 15  ax-jca 17  ax-id 24  ax-trud 26  ax-cb1 29
This theorem is referenced by:  alnex  174  exnal1  175
  Copyright terms: Public domain W3C validator