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

Theorem sylan 59
Description: Syllogism inference. (Contributed by Mario Carneiro, 8-Oct-2014.)
Hypotheses
Ref Expression
sylan.1 |- R |= S
sylan.2 |- (S, T) |= A
Assertion
Ref Expression
sylan |- (R, T) |= A

Proof of Theorem sylan
StepHypRef Expression
1 sylan.1 . . 3 |- R |= S
2 sylan.2 . . . . 5 |- (S, T) |= A
32ax-cb1 29 . . . 4 |- (S, T):*
43wctr 34 . . 3 |- T:*
51, 4adantr 55 . 2 |- (R, T) |= S
61ax-cb1 29 . . 3 |- R:*
76, 4simpr 23 . 2 |- (R, T) |= T
85, 7, 2syl2anc 19 1 |- (R, T) |= A
Colors of variables: type var term
Syntax hints:  kct 10   |= wffMMJ2 11
This theorem was proved from axioms:  ax-syl 15  ax-jca 17  ax-simpl 20  ax-simpr 21  ax-cb1 29  ax-wctr 32
This theorem is referenced by:  anasss  61
  Copyright terms: Public domain W3C validator