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

Theorem syl2anb 599
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 583 . 2 ((𝜑𝜒) → 𝜃)
51, 4sylan2b 595 1 ((𝜑𝜏) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398
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 209  df-an 399
This theorem is referenced by:  sylancb  601  rexdifi  4120  reupick3  4286  difprsnss  4724  opthhausdorff  5398  pwssun  5448  trin2  5976  sspred  6149  fundif  6396  fnun  6456  fco  6524  f1co  6578  foco  6595  f1oun  6627  f1oco  6630  eqfnfv  6795  eqfunfv  6800  sorpsscmpl  7452  ordsucsssuc  7530  ordsucun  7532  soxp  7815  ressuppssdif  7843  wfrlem4  7950  issmo  7977  tfrlem5  8008  ener  8548  domtr  8554  unen  8588  xpdom2  8604  mapen  8673  unxpdomlem3  8716  fiin  8878  suc11reg  9074  djuunxp  9342  xpnum  9372  pm54.43  9421  r0weon  9430  fseqen  9445  kmlem9  9576  axpre-lttrn  10580  axpre-mulgt0  10582  wloglei  11164  mulnzcnopr  11278  zaddcl  12014  zmulcl  12023  qaddcl  12356  qmulcl  12358  rpaddcl  12403  rpmulcl  12404  rpdivcl  12406  xrltnsym  12522  xrlttri  12524  xmullem  12649  xmulcom  12651  xmulneg1  12654  xmulf  12657  ge0addcl  12840  ge0mulcl  12841  ge0xaddcl  12842  ge0xmulcl  12843  serge0  13416  expclzlem  13445  expge0  13457  expge1  13458  hashfacen  13804  wwlktovf1  14313  qredeu  15994  nn0gcdsq  16084  mul4sq  16282  fpwipodrs  17766  pwmnd  18094  gimco  18400  gictr  18407  symgextf1  18541  efgrelexlemb  18868  xrs1mnd  20575  lmimco  20980  lmictra  20981  cctop  21606  iscn2  21838  iscnp2  21839  paste  21894  txuni  22192  txcn  22226  txcmpb  22244  tx2ndc  22251  hmphtr  22383  snfil  22464  supfil  22495  filssufilg  22511  tsmsxp  22755  dscmet  23174  rlimcnp  25535  efnnfsumcl  25672  efchtdvds  25728  lgsne0  25903  mul2sq  25987  colinearalglem2  26685  nb3grprlem2  27155  cplgr3v  27209  crctcshwlkn0  27591  wwlksnextinj  27669  hsn0elch  29017  shscli  29086  hsupss  29110  5oalem6  29428  mdsldmd1i  30100  superpos  30123  bnj110  32123  msubco  32771  poseq  33088  frrlem4  33119  sltsolem1  33173  fnsingle  33373  funimage  33382  funpartfun  33397  bj-nnfan  34070  bj-nnfor  34072  bj-snsetex  34268  bj-snmoore  34397  difunieq  34647  riscer  35258  divrngidl  35298  nn0rppwr  39172  nn0expgcd  39174  mzpincl  39321  kelac2lem  39654  cllem0  39915  unhe1  40121  tz6.12-1-afv  43363  tz6.12-1-afv2  43430  sprsymrelf1  43648  prmdvdsfmtnof1lem2  43737  uspgrsprf1  44012  2zrngamgm  44200  2zrngmmgm  44207  rrx2xpref1o  44695
  Copyright terms: Public domain W3C validator