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 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  5557  ordintdif  6383  funco  6556  resdif  6821  fvcofneq  7065  fnprb  7182  fntpb  7183  fvf1pr  7282  isotr  7311  weisoeq  7330  brrpssg  7701  findsg  7873  coexg  7905  resf1extb  7910  xpexgALT  7960  fnsuppres  8170  oaass  8525  oeword  8554  oeworde  8557  mapsnd  8859  ixpssmapg  8901  enrefnn  9018  pw2f1olem  9045  domsdomtr  9076  xpen  9104  mapen  9105  mapdom1  9106  phplem2  9169  mapfienlem1  9356  elfir  9366  wdomen2  9530  carden2b  9920  harcard  9931  isinffi  9945  acnlem  10001  acndom  10004  alephdom  10034  fin23lem21  10292  fin23lem39  10303  isf32lem5  10310  fin1a2lem12  10364  axdc3lem2  10404  ttukeylem1  10462  pwcfsdom  10536  canthp1  10607  nqereu  10882  addpqf  10897  axmulf  11099  axmulass  11110  axdistr  11111  ltaddnegr  11391  negeu  11411  fimaxre3  12129  nnsub  12230  nn0sub  12492  ltsubnn0  12493  elz2  12547  uzaddcl  12863  qaddcl  12924  xltneg  13177  xleneg  13178  supxrbnd1  13281  infxrgelb  13296  iccneg  13433  uzsubsubfz  13507  fzsplit2  13510  fzadd2  13520  fzss1  13524  uzsplit  13557  fzdif1  13566  fz0fzdiffz0  13598  difelfzle  13602  difelfznle  13603  fvffz0  13607  preduz  13611  predfz  13614  fzonlt0  13643  fzouzsplit  13655  fzo0addelr  13680  eluzgtdifelfzo  13688  elfzodifsumelfzo  13692  ssfzo12  13720  elfznelfzob  13734  fllt  13768  flflp1  13769  uzsup  13825  negmod  13881  modifeq2int  13898  modfzo0difsn  13908  modsumfzodifsn  13909  om2uzlt2i  13916  nn0ennn  13944  suppssfz  13959  seqfveq2  13989  sermono  13999  seqf1o  14008  ser1const  14023  rpexpmord  14133  mulsubdivbinom2  14227  faclbnd  14255  bcval4  14272  bcpasc  14286  hashkf  14297  hashunx  14351  fz1isolem  14426  ishashinf  14428  seqcoll  14429  ccatval1  14542  ccatval21sw  14550  ccatrn  14554  ccatalpha  14558  swrdnd0  14622  swrd0  14623  swrdfv2  14626  swrdspsleq  14630  addlenpfx  14656  ccatpfx  14666  swrdswrd  14670  pfxccatin12lem2  14696  pfxccat3  14699  swrdccat  14700  revccat  14731  repswswrd  14749  cshwmodn  14760  cshwidxmod  14768  repswcshw  14777  2cshwid  14779  2cshwcom  14781  2cshwcshw  14791  cshwcshid  14793  cshwcsh2id  14794  s1co  14799  cshco  14802  trclub  14964  shftfval  15036  seqshft  15051  crim  15081  caubnd  15325  limsuplt  15445  isercolllem2  15632  fsumcvg  15678  fsumcvg2  15693  fsumshftm  15747  fsumo1  15778  isumshft  15805  harmonic  15825  cvgrat  15849  mertenslem1  15850  zprod  15903  fprodmodd  15963  bpolylem  16014  bpolysum  16019  bpolydiflem  16020  fsumkthpow  16022  rpnnen2lem12  16193  dvdsval3  16226  negdvdsb  16242  dvdsnegb  16243  dvdsmul1  16247  dvdsabseq  16283  dvdsssfz1  16288  odd2np1  16311  divalglem8  16370  ndvdsadd  16380  dfgcd2  16516  dvdssqim  16524  nn0seqcvgd  16540  seq1st  16541  algcvgblem  16547  lcmf  16603  lcmfunsnlem2  16610  cncongr2  16638  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  17618  funcsetcestrclem9  18124  ismgmid  18592  mgmhmpropd  18625  mhmpropd  18719  smndex1gid  18830  smndex1id  18838  grpsubid1  18957  mulgnnp1  19014  mulgsubcl  19020  mulgnn0z  19033  mulgnndir  19035  mulgneg2  19040  lagsubg  19127  ghmco  19168  symg2bas  19323  symgextfv  19348  pgpfi2  19536  efgsfo  19669  frgpupf  19703  frgpup1  19705  gsummptshft  19866  telgsumfzslem  19918  telgsums  19923  ablfac1eu  20005  pgpfac1lem2  20007  ablfaclem3  20019  dvdsrid  20276  dvdsrneg  20279  dvr1  20316  abv1  20734  lmodfopne  20806  lbsexg  21074  xrsds  21326  znf1o  21461  lindfmm  21736  gsummoncoe1  22195  matecl  22312  mavmul0g  22440  gsummatr01  22546  mp2pm2mplem4  22696  chfacfisf  22741  chfacfisfcpmat  22742  chfacfpmmulgsum2  22752  cpmadugsumlemF  22763  isclo  22974  resttopon  23048  restcld  23059  restcls  23068  iscn  23122  iscnp  23124  cnco  23153  cndis  23178  cnindis  23179  cmpsub  23287  hauscmplem  23293  cmpfii  23296  ptcnplem  23508  txtube  23527  txcmplem1  23528  xkoptsub  23541  qtoptop  23587  kqfval  23610  hmeoco  23659  fileln0  23737  trfil1  23773  trfil2  23774  trufil  23797  elfm3  23837  hausflf2  23885  isucn  24165  bl2in  24288  metss2lem  24399  metss2  24400  stdbdxmet  24403  metrest  24412  nmval2  24480  nmoix  24617  ioo2bl  24681  xrsxmet  24698  expcn  24763  expcnOLD  24765  elcncf  24782  icccvx  24848  cphsscph  25151  iscmet3  25193  causs  25198  metcld2  25207  metsscmetcld  25215  cncmet  25222  bcth3  25231  ovolgelb  25381  ovolfi  25395  shft2rab  25409  uniioombllem3  25486  dyadmax  25499  dyadmbl  25501  subopnmbl  25505  volcn  25507  mbfid  25536  mbfeqalem2  25543  mbfres  25545  cnmbf  25560  i1fmulc  25604  mbfi1fseqlem3  25618  mbfi1fseqlem4  25619  itg2seq  25643  itg2gt0  25661  itgss3  25716  dvexp  25857  plypow  26110  plyeq0lem  26115  coeidlem  26142  dgrlt  26172  dgrcolem2  26180  elqaalem2  26228  aacjcl  26235  aaliou3lem1  26250  aaliou3lem2  26251  pserdvlem2  26338  abelthlem8  26349  cosord  26440  sinord  26443  resinf1o  26445  relogexp  26505  logdivlt  26530  advlogexp  26564  logcxp  26578  cxpcl  26583  rpcxpcl  26585  cxpne0  26586  logbchbase  26681  logbgt0b  26703  birthdaylem2  26862  cxplim  26882  divsqrtsumo1  26894  zetacvg  26925  wilthlem1  26978  ftalem7  26989  basellem1  26991  issqf  27046  sqf11  27049  sgmf  27055  sgmnncl  27057  sqff1o  27092  dvdsflsumcom  27098  mpodvdsmulf1o  27104  dvdsmulf1o  27106  sgmppw  27108  chtublem  27122  chtub  27123  logexprlim  27136  bposlem3  27197  bposlem5  27199  bposlem6  27200  lgsdirnn0  27255  gausslemma2dlem1a  27276  gausslemma2dlem5a  27281  lgsquad2  27297  lgsquad3  27298  2sqreulem1  27357  2sqreunnlem1  27360  dchrisumlem1  27400  dchrisumlem2  27401  dchrisumlem3  27402  mulogsumlem  27442  noextenddif  27580  addsrid  27871  sltneg  27951  sleneg  27952  om2noseqlt2  28194  elzn0s  28286  eln0zs  28288  peano5uzs  28292  brbtwn  28826  uspgrupgrushgr  29106  usgrumgruspgr  29109  cusgrfilem2  29384  finsumvtxdg2ssteplem2  29474  cyclnumvtx  29730  crctcshwlkn0lem4  29743  crctcshwlkn0lem6  29745  crctcshwlkn0lem7  29746  crctcshwlkn0  29751  elwspths2spth  29897  rusgrnumwwlk  29905  clwlkclwwlklem2fv2  29925  erclwwlknref  29998  1to2vfriswmgr  30208  4cycl2v2nb  30218  frgr2wwlkeqm  30260  nvo00  30690  nmorepnf  30697  ubthlem1  30799  normpyc  31075  occon3  31226  pjpreeq  31327  idcnop  31910  riesz3i  31991  cnlnssadj  32009  rnbra  32036  strlem3a  32181  cvcon3  32213  ssdmd1  32242  ssdmd2  32243  relfi  32531  fzsplit3  32716  prmsimpcyc  33181  esumcst  34053  dmvlsiga  34119  ballotlemimin  34497  bnj545  34885  bnj929  34926  bnj953  34929  pthhashvtx  35115  derangsn  35157  iscvm  35246  cvmsval  35253  cvmliftlem7  35278  cvmlift2lem12  35301  mclsssvlem  35549  supfz  35716  faclimlem3  35732  opnrebl2  36309  nn0prpwlem  36310  tailval  36361  nndivlub  36446  ctbssinf  37394  finixpnum  37599  ltflcei  37602  lindsdom  37608  lindsenlbs  37609  matunitlindflem2  37611  poimirlem4  37618  poimirlem14  37628  poimirlem15  37629  poimirlem19  37633  poimirlem20  37634  poimirlem22  37636  poimirlem24  37638  poimirlem28  37642  poimirlem30  37644  poimirlem31  37645  mblfinlem2  37652  mblfinlem3  37653  mblfinlem4  37654  ftc1anclem1  37687  ftc1anclem4  37690  ftc1anclem5  37691  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  caushft  37755  ismtyval  37794  heiborlem7  37811  heiborlem10  37814  heibor  37815  lcmineqlem8  42024  deg1gprod  42128  f1o2d2  42221  oexpreposd  42310  elrfirn  42683  ismrc  42689  nacsfix  42700  mzpcompact2lem  42739  eldiophb  42745  ellz1  42755  rexrabdioph  42782  congrep  42962  jm2.26a  42989  rngunsnply  43158  mendring  43177  iocmbl  43202  oeord2lim  43298  cantnfresb  43313  omabs2  43321  ofoafg  43343  dfno2  43417  rp-isfinite5  43506  enrelmap  43986  expgrowthi  44322  cnfex  45022  xlimclim2lem  45837  climxlim2  45844  icccncfext  45885  itgsinexp  45953  iblspltprt  45971  itgspltprt  45977  fourierdlem50  46154  fourierswlem  46228  etransclem35  46267  zm1nn  47303  subsubelfzo0  47327  ceilbi  47334  addmodne  47345  m1modmmod  47359  modlt0b  47364  iccpartres  47419  iccelpart  47434  iccpartiun  47435  iccpartnel  47439  goldbachthlem1  47546  goldbachth  47548  odz2prm2pw  47564  2pwp1prm  47590  evenltle  47718  fpprwpprb  47741  sbgoldbaltlem2  47781  bgoldbachlt  47814  isubgredg  47866  gricushgr  47917  uhgrimisgrgriclem  47930  gpgvtx0  48044  gpg5nbgrvtx13starlem2  48063  upgrwlkupwlk  48128  2zrngamgm  48233  lincresunit3  48470  lincreslvec3  48471  isldepslvec2  48474  blengt1fldiv2p1  48582  dignn0flhalf  48607  nn0sumshdiglemA  48608  rrx2pnedifcoorneor  48705  precofval2  49358  aacllem  49790