Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl2anb Unicode version

Theorem syl2anb 289
 Description: A double syllogism inference. (Contributed by NM, 29-Jul-1999.)
Hypotheses
Ref Expression
syl2anb.1
syl2anb.2
syl2anb.3
Assertion
Ref Expression
syl2anb

Proof of Theorem syl2anb
StepHypRef Expression
1 syl2anb.2 . 2
2 syl2anb.1 . . 3
3 syl2anb.3 . . 3
42, 3sylanb 282 . 2
51, 4sylan2b 285 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wb 104 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  sylancb  414  stdcndc  830  reupick3  3356  difprsnss  3653  trin2  4925  imadiflem  5197  fnun  5224  fco  5283  f1co  5335  foco  5350  f1oun  5380  f1oco  5383  eqfunfv  5516  ftpg  5597  issmo  6178  tfrlem5  6204  ener  6666  domtr  6672  unen  6703  xpdom2  6718  mapen  6733  pm54.43  7039  axpre-lttrn  7685  axpre-mulgt0  7688  zmulcl  9100  qaddcl  9420  qmulcl  9422  rpaddcl  9458  rpmulcl  9459  rpdivcl  9460  xrltnsym  9572  xrlttri3  9576  ge0addcl  9757  ge0mulcl  9758  ge0xaddcl  9759  expclzaplem  10310  expge0  10322  expge1  10323  hashfacen  10572  qredeu  11767  nn0gcdsq  11867  cnovex  12354  iscn2  12358  txuni  12421  txcn  12433
 Copyright terms: Public domain W3C validator