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 460	1 ⊢ ((𝜏 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  swopo  5600  ordintdif  6415  funco  6589  resdif  6855  fvcofneq  7095  fnprb  7210  fntpb  7211  isotr  7333  weisoeq  7352  brrpssg  7715  findsg  7890  coexg  7920  xpexgALT  7968  fnsuppres  8176  wfrlem10OLD  8318  oaass  8561  oeword  8590  oeworde  8593  mapsnd  8880  ixpssmapg  8922  enrefnn  9047  pw2f1olem  9076  domsdomtr  9112  xpen  9140  mapen  9141  mapdom1  9142  phplem2  9208  mapfienlem1  9400  elfir  9410  wdomen2  9572  carden2b  9962  harcard  9973  isinffi  9987  acnlem  10043  acndom  10046  alephdom  10076  fin23lem21  10334  fin23lem39  10345  isf32lem5  10352  fin1a2lem12  10406  axdc3lem2  10446  ttukeylem1  10504  pwcfsdom  10578  canthp1  10649  nqereu  10924  addpqf  10939  axmulf  11141  axmulass  11152  axdistr  11153  ltaddnegr  11430  negeu  11450  fimaxre3  12160  nnsub  12256  nn0sub  12522  ltsubnn0  12523  elz2  12576  uzaddcl  12888  qaddcl  12949  xltneg  13196  xleneg  13197  supxrbnd1  13300  infxrgelb  13314  iccneg  13449  uzsubsubfz  13523  fzsplit2  13526  fzadd2  13536  fzss1  13540  uzsplit  13573  fz0fzdiffz0  13610  difelfzle  13614  difelfznle  13615  fvffz0  13619  preduz  13623  predfz  13626  fzonlt0  13655  fzouzsplit  13667  fzo0addelr  13687  eluzgtdifelfzo  13694  elfzodifsumelfzo  13698  ssfzo12  13725  elfznelfzob  13738  fllt  13771  flflp1  13772  uzsup  13828  negmod  13881  modifeq2int  13898  modfzo0difsn  13908  modsumfzodifsn  13909  om2uzlt2i  13916  nn0ennn  13944  suppssfz  13959  seqfveq2  13990  sermono  14000  seqf1o  14009  ser1const  14024  rpexpmord  14133  mulsubdivbinom2  14222  faclbnd  14250  bcval4  14267  bcpasc  14281  hashkf  14292  hashunx  14346  hashfacenOLD  14414  fz1isolem  14422  ishashinf  14424  seqcoll  14425  ccatval1  14527  ccatval21sw  14535  ccatrn  14539  ccatalpha  14543  swrdnd0  14607  swrd0  14608  swrdfv2  14611  swrdspsleq  14615  addlenpfx  14641  ccatpfx  14651  swrdswrd  14655  pfxccatin12lem2  14681  pfxccat3  14684  swrdccat  14685  revccat  14716  repswswrd  14734  cshwmodn  14745  cshwidxmod  14753  repswcshw  14762  2cshwid  14764  2cshwcom  14766  2cshwcshw  14776  cshwcshid  14778  cshwcsh2id  14779  s1co  14784  cshco  14787  trclub  14945  shftfval  15017  seqshft  15032  crim  15062  caubnd  15305  limsuplt  15423  isercolllem2  15612  fsumcvg  15658  fsumcvg2  15673  fsumshftm  15727  fsumo1  15758  isumshft  15785  harmonic  15805  cvgrat  15829  mertenslem1  15830  zprod  15881  fprodmodd  15941  bpolylem  15992  bpolysum  15997  bpolydiflem  15998  fsumkthpow  16000  rpnnen2lem12  16168  dvdsval3  16201  negdvdsb  16216  dvdsnegb  16217  dvdsmul1  16221  dvdsabseq  16256  dvdsssfz1  16261  odd2np1  16284  divalglem8  16343  ndvdsadd  16353  dfgcd2  16488  dvdssqim  16496  nn0seqcvgd  16507  seq1st  16508  algcvgblem  16514  lcmf  16570  lcmfunsnlem2  16577  cncongr2  16605  prmdvdsfz  16642  isprm7  16645  prmndvdsfaclt  16662  powm2modprm  16736  modprm0  16738  modprmn0modprm0  16740  pythagtriplem1  16749  pythagtriplem4  16752  pythagtriplem8  16756  pythagtriplem9  16757  pythagtriplem12  16759  pythagtriplem14  16761  pythagtriplem16  16763  pcexp  16792  pc2dvds  16812  pcz  16814  fldivp1  16830  pcfac  16832  oddprmdvds  16836  pockthg  16839  infpnlem1  16843  prmreclem1  16849  prmreclem2  16850  1arith  16860  4sqlem11  16888  vdwlem2  16915  vdwlem8  16921  vdwnnlem2  16929  prmgaplem7  16990  prmgaplem8  16991  cshwshashlem2  17030  cshwshashlem3  17031  pwsval  17432  isacs1i  17601  funcsetcestrclem9  18115  ismgmid  18584  mhmpropd  18678  smndex1gid  18784  smndex1id  18792  grpsubid1  18908  mulgnnp1  18962  mulgsubcl  18968  mulgnn0z  18981  mulgnndir  18983  mulgneg2  18988  lagsubg  19072  ghmco  19112  symg2bas  19260  symgextfv  19286  pgpfi2  19474  efgsfo  19607  frgpupf  19641  frgpup1  19643  gsummptshft  19804  telgsumfzslem  19856  telgsums  19861  ablfac1eu  19943  pgpfac1lem2  19945  ablfaclem3  19957  dvdsrid  20181  dvdsrneg  20184  dvr1  20221  abv1  20441  lmodfopne  20510  lbsexg  20777  xrsds  20988  znf1o  21107  lindfmm  21382  gsummoncoe1  21828  matecl  21927  mavmul0g  22055  gsummatr01  22161  mp2pm2mplem4  22311  chfacfisf  22356  chfacfisfcpmat  22357  chfacfpmmulgsum2  22367  cpmadugsumlemF  22378  isclo  22591  resttopon  22665  restcld  22676  restcls  22685  iscn  22739  iscnp  22741  cnco  22770  cndis  22795  cnindis  22796  cmpsub  22904  hauscmplem  22910  cmpfii  22913  ptcnplem  23125  txtube  23144  txcmplem1  23145  xkoptsub  23158  qtoptop  23204  kqfval  23227  hmeoco  23276  fileln0  23354  trfil1  23390  trfil2  23391  trufil  23414  elfm3  23454  hausflf2  23502  isucn  23783  bl2in  23906  metss2lem  24020  metss2  24021  stdbdxmet  24024  metrest  24033  nmval2  24101  nmoix  24246  ioo2bl  24309  xrsxmet  24325  expcn  24388  elcncf  24405  icccvx  24466  cphsscph  24768  iscmet3  24810  causs  24815  metcld2  24824  metsscmetcld  24832  cncmet  24839  bcth3  24848  ovolgelb  24997  ovolfi  25011  shft2rab  25025  uniioombllem3  25102  dyadmax  25115  dyadmbl  25117  subopnmbl  25121  volcn  25123  mbfid  25152  mbfeqalem2  25159  mbfres  25161  cnmbf  25176  i1fmulc  25221  mbfi1fseqlem3  25235  mbfi1fseqlem4  25236  itg2seq  25260  itg2gt0  25278  itgss3  25332  dvexp  25470  plypow  25719  plyeq0lem  25724  coeidlem  25751  dgrlt  25780  dgrcolem2  25788  elqaalem2  25833  aacjcl  25840  aaliou3lem1  25855  aaliou3lem2  25856  pserdvlem2  25940  abelthlem8  25951  cosord  26040  sinord  26043  resinf1o  26045  relogexp  26104  logdivlt  26129  advlogexp  26163  logcxp  26177  cxpcl  26182  rpcxpcl  26184  cxpne0  26185  logbchbase  26276  logbgt0b  26298  birthdaylem2  26457  cxplim  26476  divsqrtsumo1  26488  zetacvg  26519  wilthlem1  26572  ftalem7  26583  basellem1  26585  issqf  26640  sqf11  26643  sgmf  26649  sgmnncl  26651  sqff1o  26686  dvdsflsumcom  26692  dvdsmulf1o  26698  sgmppw  26700  chtublem  26714  chtub  26715  logexprlim  26728  bposlem3  26789  bposlem5  26791  bposlem6  26792  lgsdirnn0  26847  gausslemma2dlem1a  26868  gausslemma2dlem5a  26873  lgsquad2  26889  lgsquad3  26890  2sqreulem1  26949  2sqreunnlem1  26952  dchrisumlem1  26992  dchrisumlem2  26993  dchrisumlem3  26994  mulogsumlem  27034  noextenddif  27171  addsrid  27450  sltneg  27522  sleneg  27523  brbtwn  28188  uspgrupgrushgr  28468  usgrumgruspgr  28471  cusgrfilem2  28744  finsumvtxdg2ssteplem2  28834  crctcshwlkn0lem4  29098  crctcshwlkn0lem6  29100  crctcshwlkn0lem7  29101  crctcshwlkn0  29106  elwspths2spth  29252  rusgrnumwwlk  29260  clwlkclwwlklem2fv2  29280  erclwwlknref  29353  1to2vfriswmgr  29563  4cycl2v2nb  29573  frgr2wwlkeqm  29615  nvo00  30045  nmorepnf  30052  ubthlem1  30154  normpyc  30430  occon3  30581  pjpreeq  30682  idcnop  31265  riesz3i  31346  cnlnssadj  31364  rnbra  31391  strlem3a  31536  cvcon3  31568  ssdmd1  31597  ssdmd2  31598  relfi  31864  fzsplit3  32036  prmsimpcyc  32404  esumcst  33092  dmvlsiga  33158  ballotlemimin  33535  bnj545  33937  bnj929  33978  bnj953  33981  pthhashvtx  34149  derangsn  34192  iscvm  34281  cvmsval  34288  cvmliftlem7  34313  cvmlift2lem12  34336  mclsssvlem  34584  supfz  34729  faclimlem3  34746  gg-expcn  35195  opnrebl2  35254  nn0prpwlem  35255  tailval  35306  nndivlub  35391  ctbssinf  36335  finixpnum  36521  ltflcei  36524  lindsdom  36530  lindsenlbs  36531  matunitlindflem2  36533  poimirlem4  36540  poimirlem14  36550  poimirlem15  36551  poimirlem19  36555  poimirlem20  36556  poimirlem22  36558  poimirlem24  36560  poimirlem28  36564  poimirlem30  36566  poimirlem31  36567  mblfinlem2  36574  mblfinlem3  36575  mblfinlem4  36576  ftc1anclem1  36609  ftc1anclem4  36612  ftc1anclem5  36613  ftc1anclem7  36615  ftc1anclem8  36616  ftc1anc  36617  caushft  36677  ismtyval  36716  heiborlem7  36733  heiborlem10  36736  heibor  36737  lcmineqlem8  40949  f1o2d2  41103  oexpreposd  41260  elrfirn  41481  ismrc  41487  nacsfix  41498  mzpcompact2lem  41537  eldiophb  41543  ellz1  41553  rexrabdioph  41580  congrep  41760  jm2.26a  41787  rngunsnply  41963  mendring  41982  iocmbl  42010  oeord2lim  42107  cantnfresb  42122  omabs2  42130  ofoafg  42152  dfno2  42227  rp-isfinite5  42316  enrelmap  42796  expgrowthi  43140  cnfex  43760  xlimclim2lem  44603  climxlim2  44610  icccncfext  44651  itgsinexp  44719  iblspltprt  44737  itgspltprt  44743  fourierdlem50  44920  fourierswlem  44994  etransclem35  45033  zm1nn  46058  subsubelfzo0  46082  iccpartres  46134  iccelpart  46149  iccpartiun  46150  iccpartnel  46154  goldbachthlem1  46261  goldbachth  46263  odz2prm2pw  46279  2pwp1prm  46305  evenltle  46433  fpprwpprb  46456  sbgoldbaltlem2  46496  bgoldbachlt  46529  isomushgr  46542  isomuspgrlem1  46543  isomgrtr  46555  upgrwlkupwlk  46566  mgmhmpropd  46603  2zrngamgm  46885  lincresunit3  47210  lincreslvec3  47211  isldepslvec2  47214  m1modmmod  47255  blengt1fldiv2p1  47327  dignn0flhalf  47352  nn0sumshdiglemA  47353  rrx2pnedifcoorneor  47450  aacllem  47896