Theorem syl2anr 597

Description: A double syllogism inference. For an implication-only version, see syl2imc 41. (Contributed by NM, 17-Sep-2013.)

Hypotheses

Ref	Expression
syl2an.1	⊢ (𝜑 → 𝜓)
syl2an.2	⊢ (𝜏 → 𝜒)
syl2an.3	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
syl2anr	⊢ ((𝜏 ∧ 𝜑) → 𝜃)

Proof of Theorem syl2anr

Step	Hyp	Ref	Expression
1		syl2an.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl2an.2	. . 3 ⊢ (𝜏 → 𝜒)
3		syl2an.3	. . 3 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
4	1, 2, 3	syl2an 596	. 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)
5	4	ancoms 459	1 ⊢ ((𝜏 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  swopo  5515  ordintdif  6319  funco  6481  resdif  6746  fvcofneq  6978  fnprb  7093  fntpb  7094  isotr  7216  weisoeq  7235  brrpssg  7587  findsg  7755  coexg  7785  xpexgALT  7833  fnsuppres  8016  wfrlem10OLD  8158  oaass  8401  oeword  8430  oeworde  8433  mapsnd  8683  ixpssmapg  8725  enrefnn  8846  pw2f1olem  8872  domsdomtr  8908  xpen  8936  mapen  8937  mapdom1  8938  phplem2  9000  mapfienlem1  9173  elfir  9183  wdomen2  9345  carden2b  9734  harcard  9745  isinffi  9759  acnlem  9813  acndom  9816  alephdom  9846  fin23lem21  10104  fin23lem39  10115  isf32lem5  10122  fin1a2lem12  10176  axdc3lem2  10216  ttukeylem1  10274  pwcfsdom  10348  canthp1  10419  nqereu  10694  addpqf  10709  axmulf  10911  axmulass  10922  axdistr  10923  ltaddnegr  11200  negeu  11220  fimaxre3  11930  nnsub  12026  nn0sub  12292  ltsubnn0  12293  elz2  12346  uzaddcl  12653  qaddcl  12714  xltneg  12960  xleneg  12961  supxrbnd1  13064  infxrgelb  13078  iccneg  13213  uzsubsubfz  13287  fzsplit2  13290  fzadd2  13300  fzss1  13304  uzsplit  13337  fz0fzdiffz0  13374  difelfzle  13378  difelfznle  13379  fvffz0  13383  preduz  13387  predfz  13390  fzonlt0  13419  fzouzsplit  13431  fzo0addelr  13451  eluzgtdifelfzo  13458  elfzodifsumelfzo  13462  ssfzo12  13489  elfznelfzob  13502  fllt  13535  flflp1  13536  uzsup  13592  negmod  13645  modifeq2int  13662  modfzo0difsn  13672  modsumfzodifsn  13673  om2uzlt2i  13680  nn0ennn  13708  suppssfz  13723  seqfveq2  13754  sermono  13764  seqf1o  13773  ser1const  13788  rpexpmord  13895  mulsubdivbinom2  13985  faclbnd  14013  bcval4  14030  bcpasc  14044  hashkf  14055  hashunx  14110  hashfacenOLD  14176  fz1isolem  14184  ishashinf  14186  seqcoll  14187  ccatval1  14290  ccatval21sw  14299  ccatrn  14303  ccatalpha  14307  swrdnd0  14379  swrd0  14380  swrdfv2  14383  swrdspsleq  14387  addlenpfx  14413  ccatpfx  14423  swrdswrd  14427  pfxccatin12lem2  14453  pfxccat3  14456  swrdccat  14457  revccat  14488  repswswrd  14506  cshwmodn  14517  cshwidxmod  14525  repswcshw  14534  2cshwid  14536  2cshwcom  14538  2cshwcshw  14547  cshwcshid  14549  cshwcsh2id  14550  s1co  14555  cshco  14558  trclub  14718  shftfval  14790  seqshft  14805  crim  14835  caubnd  15079  limsuplt  15197  isercolllem2  15386  fsumcvg  15433  fsumcvg2  15448  fsumshftm  15502  fsumo1  15533  isumshft  15560  harmonic  15580  cvgrat  15604  mertenslem1  15605  zprod  15656  fprodmodd  15716  bpolylem  15767  bpolysum  15772  bpolydiflem  15773  fsumkthpow  15775  rpnnen2lem12  15943  dvdsval3  15976  negdvdsb  15991  dvdsnegb  15992  dvdsmul1  15996  dvdsabseq  16031  dvdsssfz1  16036  odd2np1  16059  divalglem8  16118  ndvdsadd  16128  dfgcd2  16263  dvdssqim  16273  nn0seqcvgd  16284  seq1st  16285  algcvgblem  16291  lcmf  16347  lcmfunsnlem2  16354  cncongr2  16382  prmdvdsfz  16419  isprm7  16422  prmndvdsfaclt  16439  powm2modprm  16513  modprm0  16515  modprmn0modprm0  16517  pythagtriplem1  16526  pythagtriplem4  16529  pythagtriplem8  16533  pythagtriplem9  16534  pythagtriplem12  16536  pythagtriplem14  16538  pythagtriplem16  16540  pcexp  16569  pc2dvds  16589  pcz  16591  fldivp1  16607  pcfac  16609  oddprmdvds  16613  pockthg  16616  infpnlem1  16620  prmreclem1  16626  prmreclem2  16627  1arith  16637  4sqlem11  16665  vdwlem2  16692  vdwlem8  16698  vdwnnlem2  16706  prmgaplem7  16767  prmgaplem8  16768  cshwshashlem2  16807  cshwshashlem3  16808  pwsval  17206  isacs1i  17375  funcsetcestrclem9  17889  ismgmid  18358  mhmpropd  18445  smndex1gid  18551  smndex1id  18559  grpsubid1  18669  mulgnnp1  18721  mulgsubcl  18727  mulgnn0z  18739  mulgnndir  18741  mulgneg2  18746  lagsubg  18827  ghmco  18863  symg2bas  19009  symgextfv  19035  pgpfi2  19220  efgsfo  19354  frgpupf  19388  frgpup1  19390  gsummptshft  19546  telgsumfzslem  19598  telgsums  19603  ablfac1eu  19685  pgpfac1lem2  19687  ablfaclem3  19699  dvdsrid  19902  dvdsrneg  19905  dvr1  19940  abv1  20102  lmodfopne  20170  lbsexg  20435  xrsds  20650  znf1o  20768  lindfmm  21043  gsummoncoe1  21484  matecl  21583  mavmul0g  21711  gsummatr01  21817  mp2pm2mplem4  21967  chfacfisf  22012  chfacfisfcpmat  22013  chfacfpmmulgsum2  22023  cpmadugsumlemF  22034  isclo  22247  resttopon  22321  restcld  22332  restcls  22341  iscn  22395  iscnp  22397  cnco  22426  cndis  22451  cnindis  22452  cmpsub  22560  hauscmplem  22566  cmpfii  22569  ptcnplem  22781  txtube  22800  txcmplem1  22801  xkoptsub  22814  qtoptop  22860  kqfval  22883  hmeoco  22932  fileln0  23010  trfil1  23046  trfil2  23047  trufil  23070  elfm3  23110  hausflf2  23158  isucn  23439  bl2in  23562  metss2lem  23676  metss2  23677  stdbdxmet  23680  metrest  23689  nmval2  23757  nmoix  23902  ioo2bl  23965  xrsxmet  23981  expcn  24044  elcncf  24061  icccvx  24122  cphsscph  24424  iscmet3  24466  causs  24471  metcld2  24480  metsscmetcld  24488  cncmet  24495  bcth3  24504  ovolgelb  24653  ovolfi  24667  shft2rab  24681  uniioombllem3  24758  dyadmax  24771  dyadmbl  24773  subopnmbl  24777  volcn  24779  mbfid  24808  mbfeqalem2  24815  mbfres  24817  cnmbf  24832  i1fmulc  24877  mbfi1fseqlem3  24891  mbfi1fseqlem4  24892  itg2seq  24916  itg2gt0  24934  itgss3  24988  dvexp  25126  plypow  25375  plyeq0lem  25380  coeidlem  25407  dgrlt  25436  dgrcolem2  25444  elqaalem2  25489  aacjcl  25496  aaliou3lem1  25511  aaliou3lem2  25512  pserdvlem2  25596  abelthlem8  25607  cosord  25696  sinord  25699  resinf1o  25701  relogexp  25760  logdivlt  25785  advlogexp  25819  logcxp  25833  cxpcl  25838  rpcxpcl  25840  cxpne0  25841  logbchbase  25930  logbgt0b  25952  birthdaylem2  26111  cxplim  26130  divsqrtsumo1  26142  zetacvg  26173  wilthlem1  26226  ftalem7  26237  basellem1  26239  issqf  26294  sqf11  26297  sgmf  26303  sgmnncl  26305  sqff1o  26340  dvdsflsumcom  26346  dvdsmulf1o  26352  sgmppw  26354  chtublem  26368  chtub  26369  logexprlim  26382  bposlem3  26443  bposlem5  26445  bposlem6  26446  lgsdirnn0  26501  gausslemma2dlem1a  26522  gausslemma2dlem5a  26527  lgsquad2  26543  lgsquad3  26544  2sqreulem1  26603  2sqreunnlem1  26606  dchrisumlem1  26646  dchrisumlem2  26647  dchrisumlem3  26648  mulogsumlem  26688  brbtwn  27276  uspgrupgrushgr  27556  usgrumgruspgr  27559  cusgrfilem2  27832  finsumvtxdg2ssteplem2  27922  crctcshwlkn0lem4  28187  crctcshwlkn0lem6  28189  crctcshwlkn0lem7  28190  crctcshwlkn0  28195  elwspths2spth  28341  rusgrnumwwlk  28349  clwlkclwwlklem2fv2  28369  erclwwlknref  28442  1to2vfriswmgr  28652  4cycl2v2nb  28662  frgr2wwlkeqm  28704  nvo00  29132  nmorepnf  29139  ubthlem1  29241  normpyc  29517  occon3  29668  pjpreeq  29769  idcnop  30352  riesz3i  30433  cnlnssadj  30451  rnbra  30478  strlem3a  30623  cvcon3  30655  ssdmd1  30684  ssdmd2  30685  relfi  30950  fzsplit3  31124  prmsimpcyc  31490  esumcst  32040  dmvlsiga  32106  ballotlemimin  32481  bnj545  32884  bnj929  32925  bnj953  32928  pthhashvtx  33098  derangsn  33141  iscvm  33230  cvmsval  33237  cvmliftlem7  33262  cvmlift2lem12  33285  mclsssvlem  33533  supfz  33703  faclimlem3  33720  noextenddif  33880  addsid1  34136  opnrebl2  34519  nn0prpwlem  34520  tailval  34571  nndivlub  34656  ctbssinf  35586  finixpnum  35771  ltflcei  35774  lindsdom  35780  lindsenlbs  35781  matunitlindflem2  35783  poimirlem4  35790  poimirlem14  35800  poimirlem15  35801  poimirlem19  35805  poimirlem20  35806  poimirlem22  35808  poimirlem24  35810  poimirlem28  35814  poimirlem30  35816  poimirlem31  35817  mblfinlem2  35824  mblfinlem3  35825  mblfinlem4  35826  ftc1anclem1  35859  ftc1anclem4  35862  ftc1anclem5  35863  ftc1anclem7  35865  ftc1anclem8  35866  ftc1anc  35867  caushft  35928  ismtyval  35967  heiborlem7  35984  heiborlem10  35987  heibor  35988  lcmineqlem8  40051  oexpreposd  40328  elrfirn  40524  ismrc  40530  nacsfix  40541  mzpcompact2lem  40580  eldiophb  40586  ellz1  40596  rexrabdioph  40623  congrep  40802  jm2.26a  40829  rngunsnply  41005  mendring  41024  iocmbl  41051  rp-isfinite5  41131  enrelmap  41612  expgrowthi  41958  cnfex  42578  xlimclim2lem  43387  climxlim2  43394  icccncfext  43435  itgsinexp  43503  iblspltprt  43521  itgspltprt  43527  fourierdlem50  43704  fourierswlem  43778  etransclem35  43817  zm1nn  44805  subsubelfzo0  44829  iccpartres  44881  iccelpart  44896  iccpartiun  44897  iccpartnel  44901  goldbachthlem1  45008  goldbachth  45010  odz2prm2pw  45026  2pwp1prm  45052  evenltle  45180  fpprwpprb  45203  sbgoldbaltlem2  45243  bgoldbachlt  45276  isomushgr  45289  isomuspgrlem1  45290  isomgrtr  45302  upgrwlkupwlk  45313  mgmhmpropd  45350  2zrngamgm  45508  lincresunit3  45833  lincreslvec3  45834  isldepslvec2  45837  m1modmmod  45878  blengt1fldiv2p1  45950  dignn0flhalf  45975  nn0sumshdiglemA  45976  rrx2pnedifcoorneor  46073  aacllem  46516