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

Theorem syl2anb 496
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 489 . 2 ((𝜑𝜒) → 𝜃)
51, 4sylan2b 492 1 ((𝜑𝜏) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384
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 386
This theorem is referenced by:  sylancb  698  reupick3  3904  difprsnss  4320  pwssun  5010  trin2  5507  sspred  5676  fundif  5923  fnun  5985  fco  6045  f1co  6097  foco  6112  f1oun  6143  f1oco  6146  eqfnfv  6297  eqfunfv  6302  sorpsscmpl  6933  ordsucsssuc  7008  ordsucun  7010  soxp  7275  ressuppssdif  7301  wfrlem4  7403  issmo  7430  tfrlem5  7461  ener  7987  enerOLD  7988  domtr  7994  unen  8025  xpdom2  8040  mapen  8109  unxpdomlem3  8151  fiin  8313  suc11reg  8501  xpnum  8762  pm54.43  8811  r0weon  8820  fseqen  8835  kmlem9  8965  axpre-lttrn  9972  axpre-mulgt0  9974  wloglei  10545  mulnzcnopr  10658  zaddcl  11402  zmulcl  11411  qaddcl  11789  qmulcl  11791  rpaddcl  11839  rpmulcl  11840  rpdivcl  11841  xrltnsym  11955  xrlttri  11957  xmullem  12079  xmulcom  12081  xmulneg1  12084  xmulf  12087  ge0addcl  12269  ge0mulcl  12270  ge0xaddcl  12271  ge0xmulcl  12272  serge0  12838  expclzlem  12867  expge0  12879  expge1  12880  hashfacen  13221  wwlktovf1  13681  qredeu  15353  nn0gcdsq  15441  mul4sq  15639  fpwipodrs  17145  gimco  17691  gictr  17698  symgextf1  17822  efgrelexlemb  18144  xrs1mnd  19765  lmimco  20164  lmictra  20165  cctop  20791  iscn2  21023  iscnp2  21024  paste  21079  txuni  21376  txcn  21410  txcmpb  21428  tx2ndc  21435  hmphtr  21567  snfil  21649  supfil  21680  filssufilg  21696  tsmsxp  21939  dscmet  22358  rlimcnp  24673  efnnfsumcl  24810  efchtdvds  24866  lgsne0  25041  mul2sq  25125  colinearalglem2  25768  nb3grprlem2  26264  cplgr3v  26312  crctcshwlkn0  26694  wlknwwlksnsur  26757  wlkwwlksur  26764  wwlksnextinj  26775  hsn0elch  28075  shscli  28146  hsupss  28170  5oalem6  28488  mdsldmd1i  29160  superpos  29183  bnj110  30902  msubco  31402  poseq  31724  frrlem4  31757  sltsolem1  31800  fnsingle  32001  funimage  32010  funpartfun  32025  bj-snsetex  32926  bj-snmoore  33043  riscer  33758  divrngidl  33798  mzpincl  37116  kelac2lem  37453  rp-fakenanass  37679  cllem0  37690  unhe1  37899  tz6.12-1-afv  41017  prmdvdsfmtnof1lem2  41262  sprsymrelf1  41511  uspgrsprf1  41520  2zrngamgm  41704  2zrngmmgm  41711
  Copyright terms: Public domain W3C validator