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

Theorem syl2anb 577
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 562 . 2 ((𝜑𝜒) → 𝜃)
51, 4sylan2b 573 1 ((𝜑𝜏) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382
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 197  df-an 383
This theorem is referenced by:  sylancb  579  reupick3  4058  difprsnss  4463  opthhausdorff  5110  pwssun  5153  trin2  5660  sspred  5831  fundif  6078  fnun  6137  fco  6198  f1co  6251  foco  6266  f1oun  6297  f1oco  6300  eqfnfv  6454  eqfunfv  6459  sorpsscmpl  7094  ordsucsssuc  7169  ordsucun  7171  soxp  7440  ressuppssdif  7466  wfrlem4  7569  wfrlem4OLD  7570  issmo  7597  tfrlem5  7628  ener  8155  domtr  8161  unen  8195  xpdom2  8210  mapen  8279  unxpdomlem3  8321  fiin  8483  suc11reg  8679  djuunxp  8946  xpnum  8976  pm54.43  9025  r0weon  9034  fseqen  9049  kmlem9  9181  axpre-lttrn  10188  axpre-mulgt0  10190  wloglei  10761  mulnzcnopr  10874  zaddcl  11618  zmulcl  11627  qaddcl  12006  qmulcl  12008  rpaddcl  12056  rpmulcl  12057  rpdivcl  12058  xrltnsym  12174  xrlttri  12176  xmullem  12298  xmulcom  12300  xmulneg1  12303  xmulf  12306  ge0addcl  12490  ge0mulcl  12491  ge0xaddcl  12492  ge0xmulcl  12493  serge0  13061  expclzlem  13090  expge0  13102  expge1  13103  hashfacen  13439  wwlktovf1  13909  qredeu  15578  nn0gcdsq  15666  mul4sq  15864  fpwipodrs  17371  gimco  17917  gictr  17924  symgextf1  18047  efgrelexlemb  18369  xrs1mnd  19998  lmimco  20399  lmictra  20400  cctop  21030  iscn2  21262  iscnp2  21263  paste  21318  txuni  21615  txcn  21649  txcmpb  21667  tx2ndc  21674  hmphtr  21806  snfil  21887  supfil  21918  filssufilg  21934  tsmsxp  22177  dscmet  22596  rlimcnp  24912  efnnfsumcl  25049  efchtdvds  25105  lgsne0  25280  mul2sq  25364  colinearalglem2  26007  nb3grprlem2  26505  cplgr3v  26565  crctcshwlkn0  26948  wlknwwlksnsur  27023  wlkwwlksur  27030  wwlksnextinj  27041  hsn0elch  28439  shscli  28510  hsupss  28534  5oalem6  28852  mdsldmd1i  29524  superpos  29547  bnj110  31260  msubco  31760  poseq  32084  frrlem4  32114  sltsolem1  32157  fnsingle  32357  funimage  32366  funpartfun  32381  bj-snsetex  33276  bj-snmoore  33393  riscer  34112  divrngidl  34152  mzpincl  37816  kelac2lem  38153  rp-fakenanass  38379  cllem0  38390  unhe1  38598  tz6.12-1-afv  41768  prmdvdsfmtnof1lem2  42015  sprsymrelf1  42264  uspgrsprf1  42273  2zrngamgm  42457  2zrngmmgm  42464
  Copyright terms: Public domain W3C validator