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

Theorem syl2anb 601
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 584 . 2 ((𝜑𝜒) → 𝜃)
51, 4sylan2b 597 1 ((𝜑𝜏) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399
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 210  df-an 400
This theorem is referenced by:  sylancb  603  rexdifi  4074  reupick3  4248  difprsnss  4726  opthhausdorff  5414  pwssun  5465  trin2  6002  sspred  6183  fundif  6446  fnun  6508  fcoOLD  6588  f1cof1  6644  f1coOLD  6646  f1oun  6698  f1oco  6701  eqfnfv  6870  eqfunfv  6875  sorpsscmpl  7540  ordsucsssuc  7620  ordsucun  7622  soxp  7916  ressuppssdif  7947  frrlem4  8050  wfrlem4  8078  issmo  8105  tfrlem5  8136  ener  8697  domtr  8703  unen  8745  xpdom2  8762  mapen  8832  unxpdomlem3  8908  fiin  9062  suc11reg  9258  djuunxp  9561  xpnum  9591  pm54.43  9641  r0weon  9650  fseqen  9665  kmlem9  9796  axpre-lttrn  10804  axpre-mulgt0  10806  wloglei  11388  mulnzcnopr  11502  zaddcl  12241  zmulcl  12250  qaddcl  12585  qmulcl  12587  rpaddcl  12632  rpmulcl  12633  rpdivcl  12635  xrltnsym  12751  xrlttri  12753  xmullem  12878  xmulcom  12880  xmulneg1  12883  xmulf  12886  ge0addcl  13072  ge0mulcl  13073  ge0xaddcl  13074  ge0xmulcl  13075  serge0  13654  expclzlem  13683  expge0  13695  expge1  13696  hashfacen  14042  hashfacenOLD  14043  wwlktovf1  14548  qredeu  16239  nn0gcdsq  16332  mul4sq  16531  fpwipodrs  18070  pwmnd  18388  gimco  18696  gictr  18703  symgextf1  18837  efgrelexlemb  19164  xrs1mnd  20425  lmimco  20830  lmictra  20831  cctop  21927  iscn2  22159  iscnp2  22160  paste  22215  txuni  22513  txcn  22547  txcmpb  22565  tx2ndc  22572  hmphtr  22704  snfil  22785  supfil  22816  filssufilg  22832  tsmsxp  23076  dscmet  23494  rlimcnp  25872  efnnfsumcl  26009  efchtdvds  26065  lgsne0  26240  mul2sq  26324  colinearalglem2  27022  nb3grprlem2  27493  cplgr3v  27547  crctcshwlkn0  27929  wwlksnextinj  28007  hsn0elch  29353  shscli  29422  hsupss  29446  5oalem6  29764  mdsldmd1i  30436  superpos  30459  bnj110  32574  msubco  33229  poseq  33565  sltsolem1  33641  fnsingle  33984  funimage  33993  funpartfun  34008  bj-nnfan  34693  bj-nnfor  34695  bj-snsetex  34916  bj-snmoore  35045  difunieq  35308  riscer  35909  divrngidl  35949  nn0rppwr  40069  nn0expgcd  40071  dvdsexpnn0  40077  mzpincl  40287  kelac2lem  40620  cllem0  40877  unhe1  41098  tz6.12-1-afv  44366  tz6.12-1-afv2  44433  sprsymrelf1  44649  prmdvdsfmtnof1lem2  44738  uspgrsprf1  45010  2zrngamgm  45198  2zrngmmgm  45205  rrx2xpref1o  45765  f1omo  45889
  Copyright terms: Public domain W3C validator