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. (Contributed by Mario Carneiro, 8-Oct-2014.)
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 was proved from axioms:  ax-syl 15
This theorem is referenced by:  syl2anc  19  a1i  28  simpld  37  simprd  38  adantr  55  pm2.21  153  con3d  162  ecase  163  exlimdv2  166  cla4ev  169  19.8a  170  eta  178  exlimd  183  eximdv  185  exnal1  187  ac  197  exmid  199  notnot  200  ax3  205  ax7  209  ax9  212  ax11  214  axrep  220  axpow  221  axun  222
  Copyright terms: Public domain W3C validator