MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl2anb Unicode version

Theorem syl2anb 479
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 472 . 2
51, 4sylan2b 475 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369
This theorem is referenced by:  sylancb  665  2eu6OLD  2384  reupick3  3782  difprsnss  4165  pwssun  4791  trin2  5395  fnun  5692  fco  5746  f1co  5795  foco  5810  f1oun  5840  f1oco  5843  eqfnfv  5981  eqfunfv  5986  sorpsscmpl  6591  ordsucsssuc  6658  ordsucun  6660  soxp  6913  ressuppssdif  6940  issmo  7038  tfrlem5  7068  ener  7582  domtr  7588  unen  7618  xpdom2  7632  mapen  7701  unxpdomlem3  7746  fiin  7902  suc11reg  8057  xpnum  8353  pm54.43  8402  r0weon  8411  fseqen  8429  kmlem9  8559  axpre-lttrn  9564  axpre-mulgt0  9566  wloglei  10110  mulnzcnopr  10220  zaddcl  10929  zmulcl  10937  qaddcl  11227  qmulcl  11229  rpaddcl  11269  rpmulcl  11270  rpdivcl  11271  xrltnsym  11372  xrlttri  11374  xmullem  11485  xmulcom  11487  xmulneg1  11490  xmulf  11493  ge0addcl  11661  ge0mulcl  11662  ge0xaddcl  11663  ge0xmulcl  11664  serge0  12161  expclzlem  12190  expge0  12202  expge1  12203  hashfacen  12503  wwlktovf1  12895  xpnnenOLD  13943  qredeu  14248  nn0gcdsq  14285  mul4sq  14472  fpwipodrs  15794  gimco  16316  gictr  16323  symgextf1  16446  efgrelexlemb  16768  xrs1mnd  18456  lmimco  18879  lmictra  18880  iscn2  19739  iscnp2  19740  paste  19795  txuni  20093  txcn  20127  txcmpb  20145  tx2ndc  20152  hmphtr  20284  snfil  20365  supfil  20396  filssufilg  20412  tsmsxp  20657  dscmet  21093  rlimcnp  23295  efnnfsumcl  23376  efchtdvds  23433  lgsne0  23608  mul2sq  23640  colinearalglem2  24210  nb3graprlem2  24452  wlkntrllem3  24563  wlknwwlknsur  24712  wlkiswwlksur  24719  wwlkextinj  24730  frgra3v  25002  ablosn  25349  ablomul  25357  hsn0elch  26166  shscli  26235  hsupss  26259  5oalem6  26577  mdsldmd1i  27250  superpos  27273  msubco  28891  ghomsn  29028  sspred  29252  poseq  29333  wfrlem4  29346  frrlem4  29390  sltsolem1  29428  fnsingle  29569  funimage  29578  funpartfun  29593  riscer  30391  divrngidl  30425  mzpincl  30666  kelac2lem  31010  tz6.12-1-afv  32259  2zrngamgm  32745  2zrngmmgm  32752  bnj110  33916  bj-snsetex  34521  rp-fakenanass  37739  cllem0  37751  unhe1  37808
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
  Copyright terms: Public domain W3C validator