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

Theorem syl 16
Description: Syllogism inference.
Hypotheses
Ref Expression
ax-syl.1 |- R |= S
ax-syl.2 |- S |= T
Assertion
Ref Expression
syl |- R |= T

Proof of Theorem syl
StepHypRef Expression
1 ax-syl.1 . 2 |- R |= S
2 ax-syl.2 . 2 |- S |= T
31, 2ax-syl 15 1 |- R |= T
Colors of variables: type var term
Syntax hints:   |= wffMMJ2 11
This theorem is referenced by:  syl2anc  19  a1i  28  simpld  35  simprd  36  adantr  50  pm2.21  143  con3d  152  ecase  153  exlimdv2  156  cla4ev  159  19.8a  160  eta  166  exlimd  171  eximdv  173  exnal1  175  ac  184  exmid  186  notnot  187  ax3  192  ax7  196  ax9  199  ax11  201  axrep  207  axpow  208  axun  209
This theorem was proved from axioms:  ax-syl 15
  Copyright terms: Public domain W3C validator