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  5561  ordintdif  6372  funco  6546  resdif  6810  fvcofneq  7048  fnprb  7163  fntpb  7164  isotr  7286  weisoeq  7305  brrpssg  7667  findsg  7841  coexg  7871  xpexgALT  7919  fnsuppres  8127  wfrlem10OLD  8269  oaass  8513  oeword  8542  oeworde  8545  mapsnd  8831  ixpssmapg  8873  enrefnn  8998  pw2f1olem  9027  domsdomtr  9063  xpen  9091  mapen  9092  mapdom1  9093  phplem2  9159  mapfienlem1  9350  elfir  9360  wdomen2  9522  carden2b  9912  harcard  9923  isinffi  9937  acnlem  9993  acndom  9996  alephdom  10026  fin23lem21  10284  fin23lem39  10295  isf32lem5  10302  fin1a2lem12  10356  axdc3lem2  10396  ttukeylem1  10454  pwcfsdom  10528  canthp1  10599  nqereu  10874  addpqf  10889  axmulf  11091  axmulass  11102  axdistr  11103  ltaddnegr  11380  negeu  11400  fimaxre3  12110  nnsub  12206  nn0sub  12472  ltsubnn0  12473  elz2  12526  uzaddcl  12838  qaddcl  12899  xltneg  13146  xleneg  13147  supxrbnd1  13250  infxrgelb  13264  iccneg  13399  uzsubsubfz  13473  fzsplit2  13476  fzadd2  13486  fzss1  13490  uzsplit  13523  fz0fzdiffz0  13560  difelfzle  13564  difelfznle  13565  fvffz0  13569  preduz  13573  predfz  13576  fzonlt0  13605  fzouzsplit  13617  fzo0addelr  13637  eluzgtdifelfzo  13644  elfzodifsumelfzo  13648  ssfzo12  13675  elfznelfzob  13688  fllt  13721  flflp1  13722  uzsup  13778  negmod  13831  modifeq2int  13848  modfzo0difsn  13858  modsumfzodifsn  13859  om2uzlt2i  13866  nn0ennn  13894  suppssfz  13909  seqfveq2  13940  sermono  13950  seqf1o  13959  ser1const  13974  rpexpmord  14083  mulsubdivbinom2  14172  faclbnd  14200  bcval4  14217  bcpasc  14231  hashkf  14242  hashunx  14296  hashfacenOLD  14364  fz1isolem  14372  ishashinf  14374  seqcoll  14375  ccatval1  14477  ccatval21sw  14485  ccatrn  14489  ccatalpha  14493  swrdnd0  14557  swrd0  14558  swrdfv2  14561  swrdspsleq  14565  addlenpfx  14591  ccatpfx  14601  swrdswrd  14605  pfxccatin12lem2  14631  pfxccat3  14634  swrdccat  14635  revccat  14666  repswswrd  14684  cshwmodn  14695  cshwidxmod  14703  repswcshw  14712  2cshwid  14714  2cshwcom  14716  2cshwcshw  14726  cshwcshid  14728  cshwcsh2id  14729  s1co  14734  cshco  14737  trclub  14895  shftfval  14967  seqshft  14982  crim  15012  caubnd  15255  limsuplt  15373  isercolllem2  15562  fsumcvg  15608  fsumcvg2  15623  fsumshftm  15677  fsumo1  15708  isumshft  15735  harmonic  15755  cvgrat  15779  mertenslem1  15780  zprod  15831  fprodmodd  15891  bpolylem  15942  bpolysum  15947  bpolydiflem  15948  fsumkthpow  15950  rpnnen2lem12  16118  dvdsval3  16151  negdvdsb  16166  dvdsnegb  16167  dvdsmul1  16171  dvdsabseq  16206  dvdsssfz1  16211  odd2np1  16234  divalglem8  16293  ndvdsadd  16303  dfgcd2  16438  dvdssqim  16446  nn0seqcvgd  16457  seq1st  16458  algcvgblem  16464  lcmf  16520  lcmfunsnlem2  16527  cncongr2  16555  prmdvdsfz  16592  isprm7  16595  prmndvdsfaclt  16612  powm2modprm  16686  modprm0  16688  modprmn0modprm0  16690  pythagtriplem1  16699  pythagtriplem4  16702  pythagtriplem8  16706  pythagtriplem9  16707  pythagtriplem12  16709  pythagtriplem14  16711  pythagtriplem16  16713  pcexp  16742  pc2dvds  16762  pcz  16764  fldivp1  16780  pcfac  16782  oddprmdvds  16786  pockthg  16789  infpnlem1  16793  prmreclem1  16799  prmreclem2  16800  1arith  16810  4sqlem11  16838  vdwlem2  16865  vdwlem8  16871  vdwnnlem2  16879  prmgaplem7  16940  prmgaplem8  16941  cshwshashlem2  16980  cshwshashlem3  16981  pwsval  17382  isacs1i  17551  funcsetcestrclem9  18065  ismgmid  18534  mhmpropd  18622  smndex1gid  18727  smndex1id  18735  grpsubid1  18846  mulgnnp1  18898  mulgsubcl  18904  mulgnn0z  18917  mulgnndir  18919  mulgneg2  18924  lagsubg  19006  ghmco  19042  symg2bas  19188  symgextfv  19214  pgpfi2  19402  efgsfo  19535  frgpupf  19569  frgpup1  19571  gsummptshft  19727  telgsumfzslem  19779  telgsums  19784  ablfac1eu  19866  pgpfac1lem2  19868  ablfaclem3  19880  dvdsrid  20094  dvdsrneg  20097  dvr1  20132  abv1  20348  lmodfopne  20417  lbsexg  20684  xrsds  20877  znf1o  20995  lindfmm  21270  gsummoncoe1  21712  matecl  21811  mavmul0g  21939  gsummatr01  22045  mp2pm2mplem4  22195  chfacfisf  22240  chfacfisfcpmat  22241  chfacfpmmulgsum2  22251  cpmadugsumlemF  22262  isclo  22475  resttopon  22549  restcld  22560  restcls  22569  iscn  22623  iscnp  22625  cnco  22654  cndis  22679  cnindis  22680  cmpsub  22788  hauscmplem  22794  cmpfii  22797  ptcnplem  23009  txtube  23028  txcmplem1  23029  xkoptsub  23042  qtoptop  23088  kqfval  23111  hmeoco  23160  fileln0  23238  trfil1  23274  trfil2  23275  trufil  23298  elfm3  23338  hausflf2  23386  isucn  23667  bl2in  23790  metss2lem  23904  metss2  23905  stdbdxmet  23908  metrest  23917  nmval2  23985  nmoix  24130  ioo2bl  24193  xrsxmet  24209  expcn  24272  elcncf  24289  icccvx  24350  cphsscph  24652  iscmet3  24694  causs  24699  metcld2  24708  metsscmetcld  24716  cncmet  24723  bcth3  24732  ovolgelb  24881  ovolfi  24895  shft2rab  24909  uniioombllem3  24986  dyadmax  24999  dyadmbl  25001  subopnmbl  25005  volcn  25007  mbfid  25036  mbfeqalem2  25043  mbfres  25045  cnmbf  25060  i1fmulc  25105  mbfi1fseqlem3  25119  mbfi1fseqlem4  25120  itg2seq  25144  itg2gt0  25162  itgss3  25216  dvexp  25354  plypow  25603  plyeq0lem  25608  coeidlem  25635  dgrlt  25664  dgrcolem2  25672  elqaalem2  25717  aacjcl  25724  aaliou3lem1  25739  aaliou3lem2  25740  pserdvlem2  25824  abelthlem8  25835  cosord  25924  sinord  25927  resinf1o  25929  relogexp  25988  logdivlt  26013  advlogexp  26047  logcxp  26061  cxpcl  26066  rpcxpcl  26068  cxpne0  26069  logbchbase  26158  logbgt0b  26180  birthdaylem2  26339  cxplim  26358  divsqrtsumo1  26370  zetacvg  26401  wilthlem1  26454  ftalem7  26465  basellem1  26467  issqf  26522  sqf11  26525  sgmf  26531  sgmnncl  26533  sqff1o  26568  dvdsflsumcom  26574  dvdsmulf1o  26580  sgmppw  26582  chtublem  26596  chtub  26597  logexprlim  26610  bposlem3  26671  bposlem5  26673  bposlem6  26674  lgsdirnn0  26729  gausslemma2dlem1a  26750  gausslemma2dlem5a  26755  lgsquad2  26771  lgsquad3  26772  2sqreulem1  26831  2sqreunnlem1  26834  dchrisumlem1  26874  dchrisumlem2  26875  dchrisumlem3  26876  mulogsumlem  26916  noextenddif  27053  addsrid  27319  sltneg  27386  sleneg  27387  brbtwn  27911  uspgrupgrushgr  28191  usgrumgruspgr  28194  cusgrfilem2  28467  finsumvtxdg2ssteplem2  28557  crctcshwlkn0lem4  28821  crctcshwlkn0lem6  28823  crctcshwlkn0lem7  28824  crctcshwlkn0  28829  elwspths2spth  28975  rusgrnumwwlk  28983  clwlkclwwlklem2fv2  29003  erclwwlknref  29076  1to2vfriswmgr  29286  4cycl2v2nb  29296  frgr2wwlkeqm  29338  nvo00  29766  nmorepnf  29773  ubthlem1  29875  normpyc  30151  occon3  30302  pjpreeq  30403  idcnop  30986  riesz3i  31067  cnlnssadj  31085  rnbra  31112  strlem3a  31257  cvcon3  31289  ssdmd1  31318  ssdmd2  31319  relfi  31587  fzsplit3  31765  prmsimpcyc  32133  esumcst  32751  dmvlsiga  32817  ballotlemimin  33194  bnj545  33596  bnj929  33637  bnj953  33640  pthhashvtx  33808  derangsn  33851  iscvm  33940  cvmsval  33947  cvmliftlem7  33972  cvmlift2lem12  33995  mclsssvlem  34243  supfz  34387  faclimlem3  34404  opnrebl2  34869  nn0prpwlem  34870  tailval  34921  nndivlub  35006  ctbssinf  35950  finixpnum  36136  ltflcei  36139  lindsdom  36145  lindsenlbs  36146  matunitlindflem2  36148  poimirlem4  36155  poimirlem14  36165  poimirlem15  36166  poimirlem19  36170  poimirlem20  36171  poimirlem22  36173  poimirlem24  36175  poimirlem28  36179  poimirlem30  36181  poimirlem31  36182  mblfinlem2  36189  mblfinlem3  36190  mblfinlem4  36191  ftc1anclem1  36224  ftc1anclem4  36227  ftc1anclem5  36228  ftc1anclem7  36230  ftc1anclem8  36231  ftc1anc  36232  caushft  36293  ismtyval  36332  heiborlem7  36349  heiborlem10  36352  heibor  36353  lcmineqlem8  40566  oexpreposd  40865  elrfirn  41076  ismrc  41082  nacsfix  41093  mzpcompact2lem  41132  eldiophb  41138  ellz1  41148  rexrabdioph  41175  congrep  41355  jm2.26a  41382  rngunsnply  41558  mendring  41577  iocmbl  41605  oeord2lim  41702  cantnfresb  41717  omabs2  41725  ofoafg  41747  dfno2  41822  rp-isfinite5  41911  enrelmap  42391  expgrowthi  42735  cnfex  43355  xlimclim2lem  44200  climxlim2  44207  icccncfext  44248  itgsinexp  44316  iblspltprt  44334  itgspltprt  44340  fourierdlem50  44517  fourierswlem  44591  etransclem35  44630  zm1nn  45654  subsubelfzo0  45678  iccpartres  45730  iccelpart  45745  iccpartiun  45746  iccpartnel  45750  goldbachthlem1  45857  goldbachth  45859  odz2prm2pw  45875  2pwp1prm  45901  evenltle  46029  fpprwpprb  46052  sbgoldbaltlem2  46092  bgoldbachlt  46125  isomushgr  46138  isomuspgrlem1  46139  isomgrtr  46151  upgrwlkupwlk  46162  mgmhmpropd  46199  2zrngamgm  46357  lincresunit3  46682  lincreslvec3  46683  isldepslvec2  46686  m1modmmod  46727  blengt1fldiv2p1  46799  dignn0flhalf  46824  nn0sumshdiglemA  46825  rrx2pnedifcoorneor  46922  aacllem  47368