Theorem syl2anr 605

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

Syntax hints:   → wi 4   ∧ 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:  swopo  5559  ordintdif  6386  funco  6550  resdif  6817  fvcofneq  7063  fnprb  7181  fntpb  7182  fvf1pr  7280  isotr  7309  weisoeq  7328  brrpssg  7697  findsg  7867  coexg  7899  resf1extb  7904  xpexgALT  7951  mpof1o2d  8093  fnsuppres  8159  oaass  8518  oeword  8548  oeworde  8551  mapsnd  8857  ixpssmapg  8899  enrefnn  9016  pw2f1olem  9042  domsdomtr  9073  xpen  9101  mapen  9102  mapdom1  9103  phplem2  9162  mapfienlem1  9341  elfir  9351  wdomen2  9515  carden2b  9915  harcard  9926  isinffi  9940  acnlem  9994  acndom  9997  alephdom  10027  fin23lem21  10286  fin23lem39  10297  isf32lem5  10304  fin1a2lem12  10358  axdc3lem2  10398  ttukeylem1  10456  pwcfsdom  10531  canthp1  10602  nqereu  10877  addpqf  10892  axmulf  11094  axmulass  11105  axdistr  11106  ltaddnegr  11390  negeu  11410  fimaxre3  12128  nnsub  12247  nn0sub  12521  ltsubnn0  12522  elz2  12576  uzaddcl  12895  qaddcl  12956  xltneg  13210  xleneg  13211  supxrbnd1  13314  infxrgelb  13329  iccneg  13466  uzsubsubfz  13541  fzsplit2  13544  fzadd2  13554  fzss1  13558  uzsplit  13591  fzdif1  13600  fz0fzdiffz0  13632  difelfzle  13636  difelfznle  13637  fvffz0  13641  preduz  13645  predfz  13648  fzonlt0  13678  fzouzsplit  13690  fzo0addelr  13715  eluzgtdifelfzo  13723  elfzodifsumelfzo  13727  ssfzo12  13755  elfznelfzob  13770  fllt  13806  flflp1  13807  uzsup  13863  negmod  13919  modifeq2int  13936  modfzo0difsn  13946  modsumfzodifsn  13947  om2uzlt2i  13954  nn0ennn  13982  suppssfz  13997  seqfveq2  14027  sermono  14037  seqf1o  14046  ser1const  14061  rpexpmord  14171  mulsubdivbinom2  14265  faclbnd  14293  bcval4  14310  bcpasc  14324  hashkf  14335  hashunx  14389  fz1isolem  14464  ishashinf  14466  seqcoll  14467  ccatval1  14580  ccatval21sw  14589  ccatrn  14593  ccatalpha  14597  swrdnd0  14661  swrd0  14662  swrdfv2  14665  swrdspsleq  14669  addlenpfx  14694  ccatpfx  14704  swrdswrd  14708  pfxccatin12lem2  14734  pfxccat3  14737  swrdccat  14738  revccat  14769  repswswrd  14787  cshwmodn  14798  cshwidxmod  14806  repswcshw  14815  2cshwid  14817  2cshwcom  14819  2cshwcshw  14828  cshwcshid  14830  cshwcsh2id  14831  s1co  14836  cshco  14839  trclub  15001  shftfval  15073  seqshft  15088  crim  15118  caubnd  15362  limsuplt  15482  isercolllem2  15669  fsumcvg  15715  fsumcvg2  15730  fsumshftm  15784  fsumo1  15816  isumshft  15845  harmonic  15865  cvgrat  15889  mertenslem1  15890  zprod  15943  fprodmodd  16003  bpolylem  16054  bpolysum  16059  bpolydiflem  16060  fsumkthpow  16062  rpnnen2lem12  16233  dvdsval3  16266  negdvdsb  16282  dvdsnegb  16283  dvdsmul1  16287  dvdsabseq  16323  dvdsssfz1  16328  odd2np1  16351  divalglem8  16410  ndvdsadd  16420  dfgcd2  16556  dvdssqim  16564  nn0seqcvgd  16580  seq1st  16581  algcvgblem  16587  lcmf  16643  lcmfunsnlem2  16650  cncongr2  16678  prmdvdsfz  16716  isprm7  16719  prmndvdsfaclt  16736  powm2modprm  16815  modprm0  16817  modprmn0modprm0  16819  pythagtriplem1  16828  pythagtriplem4  16831  pythagtriplem8  16835  pythagtriplem9  16836  pythagtriplem12  16838  pythagtriplem14  16840  pythagtriplem16  16842  pcexp  16871  pc2dvds  16891  pcz  16893  fldivp1  16909  pcfac  16911  oddprmdvds  16915  pockthg  16918  infpnlem1  16922  prmreclem1  16928  prmreclem2  16929  1arith  16939  4sqlem11  16967  vdwlem2  16994  vdwlem8  17000  vdwnnlem2  17008  prmgaplem7  17069  prmgaplem8  17070  cshwshashlem2  17108  cshwshashlem3  17109  pwsval  17491  isacs1i  17665  funcsetcestrclem9  18171  ismgmid  18675  mgmhmpropd  18708  mhmpropd  18802  smndex1gid  18914  smndex1gidOLD  18915  smndex1id  18924  grpsubid1  19043  mulgnnp1  19100  mulgsubcl  19106  mulgnn0z  19119  mulgnndir  19121  mulgneg2  19126  lagsubg  19212  ghmco  19252  symg2bas  19409  symgextfv  19434  pgpfi2  19622  efgsfo  19755  frgpupf  19789  frgpup1  19791  gsummptshft  19952  telgsumfzslem  20004  telgsums  20009  ablfac1eu  20091  pgpfac1lem2  20093  ablfaclem3  20105  dvdsrid  20388  dvdsrneg  20391  dvr1  20428  abv1  20847  lmodfopne  20940  lbsexg  21207  xrsds  21435  znf1o  21576  lindfmm  21852  gsummoncoe1  22344  matecl  22458  mavmul0g  22586  gsummatr01  22692  mp2pm2mplem4  22842  chfacfisf  22887  chfacfisfcpmat  22888  chfacfpmmulgsum2  22898  cpmadugsumlemF  22909  isclo  23120  resttopon  23194  restcld  23205  restcls  23214  iscn  23268  iscnp  23270  cnco  23299  cndis  23324  cnindis  23325  cmpsub  23433  hauscmplem  23439  cmpfii  23442  ptcnplem  23654  txtube  23673  txcmplem1  23674  xkoptsub  23687  qtoptop  23733  kqfval  23756  hmeoco  23805  fileln0  23883  trfil1  23919  trfil2  23920  trufil  23943  elfm3  23983  hausflf2  24031  isucn  24310  bl2in  24433  metss2lem  24544  metss2  24545  stdbdxmet  24548  metrest  24557  nmval2  24625  nmoix  24762  ioo2bl  24826  xrsxmet  24843  expcn  24907  elcncf  24924  icccvx  24985  cphsscph  25286  iscmet3  25328  causs  25333  metcld2  25342  metsscmetcld  25350  cncmet  25357  bcth3  25366  ovolgelb  25515  ovolfi  25529  shft2rab  25543  uniioombllem3  25620  dyadmax  25633  dyadmbl  25635  subopnmbl  25639  volcn  25641  mbfid  25670  mbfeqalem2  25677  mbfres  25679  cnmbf  25694  i1fmulc  25738  mbfi1fseqlem3  25752  mbfi1fseqlem4  25753  itg2seq  25777  itg2gt0  25795  itgss3  25850  dvexp  25988  plypow  26238  plyeq0lem  26243  coeidlem  26270  dgrlt  26299  dgrcolem2  26307  elqaalem2  26354  aacjcl  26361  aaliou3lem1  26376  aaliou3lem2  26377  pserdvlem2  26461  abelthlem8  26472  cosord  26566  sinord  26569  resinf1o  26571  relogexp  26631  logdivlt  26656  advlogexp  26690  logcxp  26704  cxpcl  26709  rpcxpcl  26711  cxpne0  26712  logbchbase  26806  logbgt0b  26828  birthdaylem2  26987  cxplim  27006  divsqrtsumo1  27018  zetacvg  27049  wilthlem1  27102  ftalem7  27113  basellem1  27115  issqf  27170  sqf11  27173  sgmf  27179  sgmnncl  27181  sqff1o  27216  dvdsflsumcom  27222  mpodvdsmulf1o  27228  dvdsmulf1o  27230  sgmppw  27231  chtublem  27245  chtub  27246  logexprlim  27259  bposlem3  27320  bposlem5  27322  bposlem6  27323  lgsdirnn0  27378  gausslemma2dlem1a  27399  gausslemma2dlem5a  27404  lgsquad2  27420  lgsquad3  27421  2sqreulem1  27480  2sqreunnlem1  27483  dchrisumlem1  27523  dchrisumlem2  27524  dchrisumlem3  27525  mulogsumlem  27565  noextenddif  27702  addsrid  28027  ltnegs  28108  lenegs  28109  om2noseqlt2  28363  elzn0s  28461  eln0zs  28463  peano5uzs  28467  bdayfinbndlem1  28530  brbtwn  29039  uspgrupgrushgr  29319  usgrumgruspgr  29322  cusgrfilem2  29596  finsumvtxdg2ssteplem2  29686  cyclnumvtx  29939  crctcshwlkn0lem4  29952  crctcshwlkn0lem6  29954  crctcshwlkn0lem7  29955  crctcshwlkn0  29960  elwspths2spth  30109  rusgrnumwwlk  30117  clwlkclwwlklem2fv2  30137  erclwwlknref  30210  1to2vfriswmgr  30420  4cycl2v2nb  30430  frgr2wwlkeqm  30472  nvo00  30903  nmorepnf  30910  ubthlem1  31012  normpyc  31288  occon3  31439  pjpreeq  31540  idcnop  32123  riesz3i  32204  cnlnssadj  32222  rnbra  32249  strlem3a  32394  cvcon3  32426  ssdmd1  32455  ssdmd2  32456  relfi  32744  fcobijfs2  32867  fzsplit3  32938  prmsimpcyc  33362  esumcst  34314  dmvlsiga  34380  ballotlemimin  34757  bnj545  35147  bnj929  35188  bnj953  35191  fineqvnttrclselem1  35372  pthhashvtx  35426  derangsn  35468  iscvm  35557  cvmsval  35564  cvmliftlem7  35589  cvmlift2lem12  35612  mclsssvlem  35860  supfz  36027  faclimlem3  36043  opnrebl2  36629  nn0prpwlem  36630  tailval  36681  nndivlub  36766  ctbssinf  37848  finixpnum  38052  ltflcei  38055  lindsdom  38061  lindsenlbs  38062  matunitlindflem2  38064  poimirlem4  38071  poimirlem14  38081  poimirlem15  38082  poimirlem19  38086  poimirlem20  38087  poimirlem22  38089  poimirlem24  38091  poimirlem28  38095  poimirlem30  38097  poimirlem31  38098  mblfinlem2  38105  mblfinlem3  38106  mblfinlem4  38107  ftc1anclem1  38140  ftc1anclem4  38143  ftc1anclem5  38144  ftc1anclem7  38146  ftc1anclem8  38147  ftc1anc  38148  caushft  38208  ismtyval  38247  heiborlem7  38264  heiborlem10  38267  heibor  38268  lcmineqlem8  42601  deg1gprod  42705  oexpreposd  42879  elrfirn  43224  ismrc  43230  nacsfix  43241  mzpcompact2lem  43280  eldiophb  43286  ellz1  43296  rexrabdioph  43319  congrep  43498  jm2.26a  43525  rngunsnply  43694  mendring  43713  iocmbl  43738  oeord2lim  43834  cantnfresb  43849  omabs2  43857  ofoafg  43879  dfno2  43952  rp-isfinite5  44041  enrelmap  44521  expgrowthi  44857  cnfex  45556  xlimclim2lem  46361  climxlim2  46368  icccncfext  46409  itgsinexp  46477  iblspltprt  46495  itgspltprt  46501  fourierdlem50  46678  fourierswlem  46752  etransclem35  46791  zm1nn  47844  subsubelfzo0  47869  ceilbi  47879  addmodne  47892  m1modmmod  47906  modlt0b  47911  iccpartres  47972  iccelpart  47987  iccpartiun  47988  iccpartnel  47992  nprmmul1  48081  goldbachthlem1  48102  goldbachth  48104  odz2prm2pw  48120  2pwp1prm  48146  evenltle  48287  fpprwpprb  48310  sbgoldbaltlem2  48350  bgoldbachlt  48383  isubgredg  48436  gricushgr  48487  uhgrimisgrgriclem  48500  gpgvtx0  48623  gpg5nbgrvtx13starlem2  48642  upgrwlkupwlk  48710  2zrngamgm  48815  lincresunit3  49051  lincreslvec3  49052  isldepslvec2  49055  blengt1fldiv2p1  49163  dignn0flhalf  49188  nn0sumshdiglemA  49189  rrx2pnedifcoorneor  49286  precofval2  49938  aacllem  50370