Theorem syl2anr 586

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 585	. 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)
5	4	ancoms 448	1 ⊢ ((𝜏 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ∧ 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 198  df-an 385

This theorem is referenced by:  swopo  5255  ordintdif  5999  funco  6150  resdif  6382  fvcofneq  6598  fnprb  6706  fntpb  6707  isotr  6819  weisoeq  6838  brrpssg  7178  findsg  7332  coexg  7356  xpexgALT  7400  fnsuppres  7566  wfrlem10  7669  oaass  7887  oeword  7916  oeworde  7919  ixpssmapg  8184  pw2f1olem  8312  domsdomtr  8343  xpen  8371  mapen  8372  mapdom1  8373  mapfienlem1  8558  elfir  8569  wdomen2  8730  carden2b  9085  harcard  9096  isinffi  9110  acnlem  9163  acndom  9166  alephdom  9196  fin23lem21  9455  fin23lem39  9466  isf32lem5  9473  fin1a2lem12  9527  axdc3lem2  9567  ttukeylem1  9625  pwcfsdom  9699  canthp1  9770  nqereu  10045  addpqf  10060  axmulf  10261  axmulass  10272  axdistr  10273  ltaddnegr  10546  negeu  10565  fimaxre3  11264  nnsub  11356  nn0sub  11628  ltsubnn0  11629  elz2  11679  uzaddcl  11981  qaddcl  12042  xltneg  12285  xleneg  12286  supxrbnd1  12388  infxrgelb  12402  iccneg  12533  uzsubsubfz  12605  fzsplit2  12608  fzadd2  12618  fzss1  12622  uzsplit  12654  fz0fzdiffz0  12691  difelfzle  12695  difelfznle  12696  fvffz0  12700  preduz  12704  predfz  12707  fzonlt0  12734  fzouzsplit  12746  fzo0addelr  12766  eluzgtdifelfzo  12773  elfzodifsumelfzo  12777  ssfzo12  12804  elfznelfzob  12817  fllt  12850  flflp1  12851  uzsup  12905  negmod  12958  modifeq2int  12975  modfzo0difsn  12985  modsumfzodifsn  12986  om2uzlt2i  12993  nn0ennn  13021  suppssfz  13036  seqfveq2  13065  sermono  13075  seqf1o  13084  ser1const  13099  mulsubdivbinom2  13288  faclbnd  13316  bcval4  13333  bcpasc  13347  hashkf  13358  hashunx  13412  hashfacen  13474  fz1isolem  13481  ishashinf  13483  seqcoll  13484  ccatval21sw  13601  ccatalpha  13609  swrd0  13677  swrdfv2  13689  swrdspsleq  13692  swrdswrd  13703  swrdccatin12lem2  13732  swrdccat3  13735  revccat  13758  repswswrd  13774  cshwmodn  13784  cshwidxmod  13792  repswcshw  13801  2cshwid  13803  2cshwcom  13805  2cshwcshw  13814  cshwcshid  13816  cshwcsh2id  13817  s1co  13822  cshco  13825  trclub  13981  shftfval  14052  seqshft  14067  crim  14097  caubnd  14340  limsuplt  14452  isercolllem2  14638  fsumcvg  14685  fsumcvg2  14700  fsumshftm  14754  fsumo1  14785  isumshft  14812  harmonic  14832  cvgrat  14855  mertenslem1  14856  zprod  14907  fprodmodd  14967  bpolylem  15018  bpolysum  15023  bpolydiflem  15024  fsumkthpow  15026  rpnnen2lem12  15193  dvdsval3  15226  negdvdsb  15240  dvdsnegb  15241  dvdsmul1  15245  dvdsabseq  15277  dvdsssfz1  15282  odd2np1  15304  divalglem8  15362  ndvdsadd  15372  dfgcd2  15501  dvdssqim  15511  nn0seqcvgd  15521  seq1st  15522  algcvgblem  15528  lcmf  15584  lcmfunsnlem2  15591  cncongr2  15619  prmdvdsfz  15653  isprm7  15656  prmndvdsfaclt  15671  powm2modprm  15744  modprm0  15746  modprmn0modprm0  15748  pythagtriplem1  15757  pythagtriplem4  15760  pythagtriplem8  15764  pythagtriplem9  15765  pythagtriplem12  15767  pythagtriplem14  15769  pythagtriplem16  15771  pcexp  15800  pc2dvds  15819  pcz  15821  fldivp1  15837  pcfac  15839  oddprmdvds  15843  pockthg  15846  infpnlem1  15850  prmreclem1  15856  prmreclem2  15857  1arith  15867  4sqlem11  15895  vdwlem2  15922  vdwlem8  15928  vdwnnlem2  15936  prmgaplem7  15997  prmgaplem8  15998  cshwshashlem2  16034  cshwshashlem3  16035  pwsval  16370  isacs1i  16541  funcsetcestrclem9  17027  ismgmid  17488  mhmpropd  17565  grpsubid1  17724  mulgnnp1  17773  mulgsubcl  17779  mulgnn0z  17790  mulgnndir  17792  mulgneg2  17797  lagsubg  17877  ghmco  17901  symg2bas  18038  symgextfv  18058  pgpfi2  18241  efgsfo  18372  frgpupf  18406  frgpup1  18408  gsummptshft  18556  telgsumfzslem  18606  telgsums  18611  ablfac1eu  18693  pgpfac1lem2  18695  ablfaclem3  18707  dvdsrid  18872  dvdsrneg  18875  dvr1  18910  abv1  19056  lmodfopne  19124  lbsexg  19392  gsummoncoe1  19901  xrsds  20016  znf1o  20126  lindfmm  20396  matecl  20461  mavmul0g  20590  gsummatr01  20697  mp2pm2mplem4  20847  chfacfisf  20892  chfacfisfcpmat  20893  chfacfpmmulgsum2  20903  cpmadugsumlemF  20914  isclo  21125  resttopon  21199  restcld  21210  restcls  21219  iscn  21273  iscnp  21275  cnco  21304  cndis  21329  cnindis  21330  cmpsub  21437  hauscmplem  21443  cmpfii  21446  ptcnplem  21658  txtube  21677  txcmplem1  21678  xkoptsub  21691  qtoptop  21737  kqfval  21760  hmeoco  21809  fileln0  21887  trfil1  21923  trfil2  21924  trufil  21947  elfm3  21987  hausflf2  22035  isucn  22315  bl2in  22438  metss2lem  22549  metss2  22550  stdbdxmet  22553  metrest  22562  nmfval2  22628  nmval2  22629  nmoix  22766  ioo2bl  22829  xrsxmet  22845  expcn  22908  elcncf  22925  icccvx  22982  iscmet3  23324  causs  23329  metcld2  23338  cmetss  23346  cncmet  23352  bcth3  23361  ovolgelb  23483  ovolfi  23497  shft2rab  23511  uniioombllem3  23588  dyadmax  23601  dyadmbl  23603  subopnmbl  23607  volcn  23609  mbfid  23638  mbfeqalem2  23645  mbfres  23647  cnmbf  23662  i1fmulc  23706  mbfi1fseqlem3  23720  mbfi1fseqlem4  23721  itg2seq  23745  itg2gt0  23763  itgss3  23817  dvexp  23952  plypow  24197  plyeq0lem  24202  coeidlem  24229  dgrlt  24258  dgrcolem2  24266  elqaalem2  24311  aacjcl  24318  aaliou3lem1  24333  aaliou3lem2  24334  pserdvlem2  24418  abelthlem8  24429  cosord  24515  sinord  24517  resinf1o  24519  relogexp  24578  logdivlt  24603  advlogexp  24637  logcxp  24651  cxpcl  24656  rpcxpcl  24658  cxpne0  24659  logbchbase  24745  birthdaylem2  24915  cxplim  24934  divsqrtsumo1  24946  zetacvg  24977  wilthlem1  25030  ftalem7  25041  basellem1  25043  issqf  25098  sqf11  25101  sgmf  25107  sgmnncl  25109  sqff1o  25144  dvdsflsumcom  25150  dvdsmulf1o  25156  sgmppw  25158  chtublem  25172  chtub  25173  logexprlim  25186  bposlem3  25247  bposlem5  25249  bposlem6  25250  lgsdirnn0  25305  gausslemma2dlem1a  25326  gausslemma2dlem5a  25331  lgsquad2  25347  lgsquad3  25348  dchrisumlem1  25414  dchrisumlem2  25415  dchrisumlem3  25416  mulogsumlem  25456  brbtwn  26015  uspgrupgrushgr  26309  usgrumgruspgr  26312  cusgrfilem2  26602  finsumvtxdg2ssteplem2  26692  crctcshwlkn0lem4  26956  crctcshwlkn0lem6  26958  crctcshwlkn0lem7  26959  crctcshwlkn0  26964  elwspths2spth  27131  rusgrnumwwlk  27139  clwwlkccatlem  27154  clwlkclwwlklem2fv2  27161  erclwwlknref  27242  clwwlknonex2e  27301  1to2vfriswmgr  27476  4cycl2v2nb  27486  frgr2wwlkeqm  27528  nvo00  27966  nmorepnf  27973  ubthlem1  28076  normpyc  28353  occon3  28506  pjpreeq  28607  idcnop  29190  riesz3i  29271  cnlnssadj  29289  rnbra  29316  strlem3a  29461  cvcon3  29493  ssdmd1  29522  ssdmd2  29523  relfi  29762  fzsplit3  29902  esumcst  30472  dmvlsiga  30539  ballotlemimin  30914  bnj545  31309  bnj929  31350  bnj953  31353  derangsn  31496  iscvm  31585  cvmsval  31592  cvmliftlem7  31617  cvmlift2lem12  31640  mclsssvlem  31803  supfz  31956  faclimlem3  31974  noextenddif  32163  opnrebl2  32658  nn0prpwlem  32659  tailval  32710  nndivlub  32795  finixpnum  33725  ltflcei  33728  lindsdom  33734  lindsenlbs  33735  matunitlindflem2  33737  poimirlem4  33744  poimirlem14  33754  poimirlem15  33755  poimirlem19  33759  poimirlem20  33760  poimirlem22  33762  poimirlem24  33764  poimirlem28  33768  poimirlem30  33770  poimirlem31  33771  mblfinlem2  33778  mblfinlem3  33779  mblfinlem4  33780  ftc1anclem1  33815  ftc1anclem4  33818  ftc1anclem5  33819  ftc1anclem7  33821  ftc1anclem8  33822  ftc1anc  33823  caushft  33886  ismtyval  33928  heiborlem7  33945  heiborlem10  33948  heibor  33949  elrfirn  37777  ismrc  37783  nacsfix  37794  mzpcompact2lem  37833  eldiophb  37839  ellz1  37849  rexrabdioph  37877  rpexpmord  38031  congrep  38058  jm2.26a  38085  rngunsnply  38261  mendring  38280  iocmbl  38315  rp-isfinite5  38380  enrelmap  38808  expgrowthi  39049  cnfex  39698  xlimclim2lem  40562  climxlim2  40569  icccncfext  40597  itgsinexp  40667  iblspltprt  40685  itgspltprt  40691  fourierdlem50  40869  fourierswlem  40943  etransclem35  40982  zm1nn  41909  subsubelfzo0  41928  iccpartres  41946  iccelpart  41961  iccpartiun  41962  iccpartnel  41966  addlenpfx  41990  pfxccatin12lem2  42016  pfxccat3  42018  goldbachthlem1  42049  goldbachth  42051  odz2prm2pw  42067  2pwp1prm  42095  evenltle  42218  sbgoldbaltlem2  42260  bgoldbachlt  42293  upgrwlkupwlk  42306  mgmhmpropd  42370  2zrngamgm  42524  lincresunit3  42855  lincreslvec3  42856  isldepslvec2  42859  m1modmmod  42901  blengt1fldiv2p1  42972  dignn0flhalf  42997  nn0sumshdiglemA  42998  aacllem  43135