Theorem syl2anr 598

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  swopo  5550  ordintdif  6375  funco  6539  resdif  6802  fvcofneq  7046  fnprb  7163  fntpb  7164  fvf1pr  7262  isotr  7291  weisoeq  7310  brrpssg  7679  findsg  7848  coexg  7880  resf1extb  7885  xpexgALT  7934  fnsuppres  8141  oaass  8496  oeword  8526  oeworde  8529  mapsnd  8834  ixpssmapg  8876  enrefnn  8993  pw2f1olem  9019  domsdomtr  9050  xpen  9078  mapen  9079  mapdom1  9080  phplem2  9139  mapfienlem1  9318  elfir  9328  wdomen2  9492  carden2b  9891  harcard  9902  isinffi  9916  acnlem  9970  acndom  9973  alephdom  10003  fin23lem21  10261  fin23lem39  10272  isf32lem5  10279  fin1a2lem12  10333  axdc3lem2  10373  ttukeylem1  10431  pwcfsdom  10506  canthp1  10577  nqereu  10852  addpqf  10867  axmulf  11069  axmulass  11080  axdistr  11081  ltaddnegr  11363  negeu  11383  fimaxre3  12102  nnsub  12221  nn0sub  12487  ltsubnn0  12488  elz2  12542  uzaddcl  12854  qaddcl  12915  xltneg  13169  xleneg  13170  supxrbnd1  13273  infxrgelb  13288  iccneg  13425  uzsubsubfz  13500  fzsplit2  13503  fzadd2  13513  fzss1  13517  uzsplit  13550  fzdif1  13559  fz0fzdiffz0  13591  difelfzle  13595  difelfznle  13596  fvffz0  13600  preduz  13604  predfz  13607  fzonlt0  13637  fzouzsplit  13649  fzo0addelr  13674  eluzgtdifelfzo  13682  elfzodifsumelfzo  13686  ssfzo12  13714  elfznelfzob  13729  fllt  13765  flflp1  13766  uzsup  13822  negmod  13878  modifeq2int  13895  modfzo0difsn  13905  modsumfzodifsn  13906  om2uzlt2i  13913  nn0ennn  13941  suppssfz  13956  seqfveq2  13986  sermono  13996  seqf1o  14005  ser1const  14020  rpexpmord  14130  mulsubdivbinom2  14224  faclbnd  14252  bcval4  14269  bcpasc  14283  hashkf  14294  hashunx  14348  fz1isolem  14423  ishashinf  14425  seqcoll  14426  ccatval1  14539  ccatval21sw  14548  ccatrn  14552  ccatalpha  14556  swrdnd0  14620  swrd0  14621  swrdfv2  14624  swrdspsleq  14628  addlenpfx  14653  ccatpfx  14663  swrdswrd  14667  pfxccatin12lem2  14693  pfxccat3  14696  swrdccat  14697  revccat  14728  repswswrd  14746  cshwmodn  14757  cshwidxmod  14765  repswcshw  14774  2cshwid  14776  2cshwcom  14778  2cshwcshw  14787  cshwcshid  14789  cshwcsh2id  14790  s1co  14795  cshco  14798  trclub  14960  shftfval  15032  seqshft  15047  crim  15077  caubnd  15321  limsuplt  15441  isercolllem2  15628  fsumcvg  15674  fsumcvg2  15689  fsumshftm  15743  fsumo1  15775  isumshft  15804  harmonic  15824  cvgrat  15848  mertenslem1  15849  zprod  15902  fprodmodd  15962  bpolylem  16013  bpolysum  16018  bpolydiflem  16019  fsumkthpow  16021  rpnnen2lem12  16192  dvdsval3  16225  negdvdsb  16241  dvdsnegb  16242  dvdsmul1  16246  dvdsabseq  16282  dvdsssfz1  16287  odd2np1  16310  divalglem8  16369  ndvdsadd  16379  dfgcd2  16515  dvdssqim  16523  nn0seqcvgd  16539  seq1st  16540  algcvgblem  16546  lcmf  16602  lcmfunsnlem2  16609  cncongr2  16637  prmdvdsfz  16675  isprm7  16678  prmndvdsfaclt  16695  powm2modprm  16774  modprm0  16776  modprmn0modprm0  16778  pythagtriplem1  16787  pythagtriplem4  16790  pythagtriplem8  16794  pythagtriplem9  16795  pythagtriplem12  16797  pythagtriplem14  16799  pythagtriplem16  16801  pcexp  16830  pc2dvds  16850  pcz  16852  fldivp1  16868  pcfac  16870  oddprmdvds  16874  pockthg  16877  infpnlem1  16881  prmreclem1  16887  prmreclem2  16888  1arith  16898  4sqlem11  16926  vdwlem2  16953  vdwlem8  16959  vdwnnlem2  16967  prmgaplem7  17028  prmgaplem8  17029  cshwshashlem2  17067  cshwshashlem3  17068  pwsval  17449  isacs1i  17623  funcsetcestrclem9  18129  ismgmid  18633  mgmhmpropd  18666  mhmpropd  18760  smndex1gid  18872  smndex1gidOLD  18873  smndex1id  18882  grpsubid1  19001  mulgnnp1  19058  mulgsubcl  19064  mulgnn0z  19077  mulgnndir  19079  mulgneg2  19084  lagsubg  19170  ghmco  19211  symg2bas  19368  symgextfv  19393  pgpfi2  19581  efgsfo  19714  frgpupf  19748  frgpup1  19750  gsummptshft  19911  telgsumfzslem  19963  telgsums  19968  ablfac1eu  20050  pgpfac1lem2  20052  ablfaclem3  20064  dvdsrid  20347  dvdsrneg  20350  dvr1  20387  abv1  20802  lmodfopne  20895  lbsexg  21162  xrsds  21390  znf1o  21531  lindfmm  21807  gsummoncoe1  22273  matecl  22390  mavmul0g  22518  gsummatr01  22624  mp2pm2mplem4  22774  chfacfisf  22819  chfacfisfcpmat  22820  chfacfpmmulgsum2  22830  cpmadugsumlemF  22841  isclo  23052  resttopon  23126  restcld  23137  restcls  23146  iscn  23200  iscnp  23202  cnco  23231  cndis  23256  cnindis  23257  cmpsub  23365  hauscmplem  23371  cmpfii  23374  ptcnplem  23586  txtube  23605  txcmplem1  23606  xkoptsub  23619  qtoptop  23665  kqfval  23688  hmeoco  23737  fileln0  23815  trfil1  23851  trfil2  23852  trufil  23875  elfm3  23915  hausflf2  23963  isucn  24242  bl2in  24365  metss2lem  24476  metss2  24477  stdbdxmet  24480  metrest  24489  nmval2  24557  nmoix  24694  ioo2bl  24758  xrsxmet  24775  expcn  24839  elcncf  24856  icccvx  24917  cphsscph  25218  iscmet3  25260  causs  25265  metcld2  25274  metsscmetcld  25282  cncmet  25289  bcth3  25298  ovolgelb  25447  ovolfi  25461  shft2rab  25475  uniioombllem3  25552  dyadmax  25565  dyadmbl  25567  subopnmbl  25571  volcn  25573  mbfid  25602  mbfeqalem2  25609  mbfres  25611  cnmbf  25626  i1fmulc  25670  mbfi1fseqlem3  25684  mbfi1fseqlem4  25685  itg2seq  25709  itg2gt0  25727  itgss3  25782  dvexp  25920  plypow  26170  plyeq0lem  26175  coeidlem  26202  dgrlt  26231  dgrcolem2  26239  elqaalem2  26286  aacjcl  26293  aaliou3lem1  26308  aaliou3lem2  26309  pserdvlem2  26393  abelthlem8  26404  cosord  26495  sinord  26498  resinf1o  26500  relogexp  26560  logdivlt  26585  advlogexp  26619  logcxp  26633  cxpcl  26638  rpcxpcl  26640  cxpne0  26641  logbchbase  26735  logbgt0b  26757  birthdaylem2  26916  cxplim  26935  divsqrtsumo1  26947  zetacvg  26978  wilthlem1  27031  ftalem7  27042  basellem1  27044  issqf  27099  sqf11  27102  sgmf  27108  sgmnncl  27110  sqff1o  27145  dvdsflsumcom  27151  mpodvdsmulf1o  27157  dvdsmulf1o  27159  sgmppw  27160  chtublem  27174  chtub  27175  logexprlim  27188  bposlem3  27249  bposlem5  27251  bposlem6  27252  lgsdirnn0  27307  gausslemma2dlem1a  27328  gausslemma2dlem5a  27333  lgsquad2  27349  lgsquad3  27350  2sqreulem1  27409  2sqreunnlem1  27412  dchrisumlem1  27452  dchrisumlem2  27453  dchrisumlem3  27454  mulogsumlem  27494  noextenddif  27632  addsrid  27956  ltnegs  28037  lenegs  28038  om2noseqlt2  28292  elzn0s  28390  eln0zs  28392  peano5uzs  28396  bdayfinbndlem1  28459  brbtwn  28968  uspgrupgrushgr  29248  usgrumgruspgr  29251  cusgrfilem2  29525  finsumvtxdg2ssteplem2  29615  cyclnumvtx  29868  crctcshwlkn0lem4  29881  crctcshwlkn0lem6  29883  crctcshwlkn0lem7  29884  crctcshwlkn0  29889  elwspths2spth  30038  rusgrnumwwlk  30046  clwlkclwwlklem2fv2  30066  erclwwlknref  30139  1to2vfriswmgr  30349  4cycl2v2nb  30359  frgr2wwlkeqm  30401  nvo00  30832  nmorepnf  30839  ubthlem1  30941  normpyc  31217  occon3  31368  pjpreeq  31469  idcnop  32052  riesz3i  32133  cnlnssadj  32151  rnbra  32178  strlem3a  32323  cvcon3  32355  ssdmd1  32384  ssdmd2  32385  relfi  32672  fcobijfs2  32795  fzsplit3  32866  prmsimpcyc  33289  esumcst  34207  dmvlsiga  34273  ballotlemimin  34650  bnj545  35037  bnj929  35078  bnj953  35081  fineqvnttrclselem1  35265  pthhashvtx  35310  derangsn  35352  iscvm  35441  cvmsval  35448  cvmliftlem7  35473  cvmlift2lem12  35496  mclsssvlem  35744  supfz  35911  faclimlem3  35927  opnrebl2  36503  nn0prpwlem  36504  tailval  36555  nndivlub  36640  ctbssinf  37722  finixpnum  37926  ltflcei  37929  lindsdom  37935  lindsenlbs  37936  matunitlindflem2  37938  poimirlem4  37945  poimirlem14  37955  poimirlem15  37956  poimirlem19  37960  poimirlem20  37961  poimirlem22  37963  poimirlem24  37965  poimirlem28  37969  poimirlem30  37971  poimirlem31  37972  mblfinlem2  37979  mblfinlem3  37980  mblfinlem4  37981  ftc1anclem1  38014  ftc1anclem4  38017  ftc1anclem5  38018  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022  caushft  38082  ismtyval  38121  heiborlem7  38138  heiborlem10  38141  heibor  38142  lcmineqlem8  42475  deg1gprod  42579  f1o2d2  42674  oexpreposd  42754  elrfirn  43127  ismrc  43133  nacsfix  43144  mzpcompact2lem  43183  eldiophb  43189  ellz1  43199  rexrabdioph  43222  congrep  43401  jm2.26a  43428  rngunsnply  43597  mendring  43616  iocmbl  43641  oeord2lim  43737  cantnfresb  43752  omabs2  43760  ofoafg  43782  dfno2  43855  rp-isfinite5  43944  enrelmap  44424  expgrowthi  44760  cnfex  45459  xlimclim2lem  46267  climxlim2  46274  icccncfext  46315  itgsinexp  46383  iblspltprt  46401  itgspltprt  46407  fourierdlem50  46584  fourierswlem  46658  etransclem35  46697  zm1nn  47744  subsubelfzo0  47769  ceilbi  47779  addmodne  47792  m1modmmod  47806  modlt0b  47811  iccpartres  47872  iccelpart  47887  iccpartiun  47888  iccpartnel  47892  nprmmul1  47981  goldbachthlem1  48002  goldbachth  48004  odz2prm2pw  48020  2pwp1prm  48046  evenltle  48187  fpprwpprb  48210  sbgoldbaltlem2  48250  bgoldbachlt  48283  isubgredg  48336  gricushgr  48387  uhgrimisgrgriclem  48400  gpgvtx0  48523  gpg5nbgrvtx13starlem2  48542  upgrwlkupwlk  48610  2zrngamgm  48715  lincresunit3  48951  lincreslvec3  48952  isldepslvec2  48955  blengt1fldiv2p1  49063  dignn0flhalf  49088  nn0sumshdiglemA  49089  rrx2pnedifcoorneor  49186  precofval2  49838  aacllem  50270