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  5541  ordintdif  6366  funco  6530  resdif  6793  fvcofneq  7037  fnprb  7154  fntpb  7155  fvf1pr  7253  isotr  7282  weisoeq  7301  brrpssg  7670  findsg  7839  coexg  7871  resf1extb  7876  xpexgALT  7925  fnsuppres  8132  oaass  8487  oeword  8517  oeworde  8520  mapsnd  8825  ixpssmapg  8867  enrefnn  8984  pw2f1olem  9010  domsdomtr  9041  xpen  9069  mapen  9070  mapdom1  9071  phplem2  9130  mapfienlem1  9309  elfir  9319  wdomen2  9483  carden2b  9880  harcard  9891  isinffi  9905  acnlem  9959  acndom  9962  alephdom  9992  fin23lem21  10250  fin23lem39  10261  isf32lem5  10268  fin1a2lem12  10322  axdc3lem2  10362  ttukeylem1  10420  pwcfsdom  10495  canthp1  10566  nqereu  10841  addpqf  10856  axmulf  11058  axmulass  11069  axdistr  11070  ltaddnegr  11352  negeu  11372  fimaxre3  12091  nnsub  12210  nn0sub  12476  ltsubnn0  12477  elz2  12531  uzaddcl  12843  qaddcl  12904  xltneg  13158  xleneg  13159  supxrbnd1  13262  infxrgelb  13277  iccneg  13414  uzsubsubfz  13489  fzsplit2  13492  fzadd2  13502  fzss1  13506  uzsplit  13539  fzdif1  13548  fz0fzdiffz0  13580  difelfzle  13584  difelfznle  13585  fvffz0  13589  preduz  13593  predfz  13596  fzonlt0  13626  fzouzsplit  13638  fzo0addelr  13663  eluzgtdifelfzo  13671  elfzodifsumelfzo  13675  ssfzo12  13703  elfznelfzob  13718  fllt  13754  flflp1  13755  uzsup  13811  negmod  13867  modifeq2int  13884  modfzo0difsn  13894  modsumfzodifsn  13895  om2uzlt2i  13902  nn0ennn  13930  suppssfz  13945  seqfveq2  13975  sermono  13985  seqf1o  13994  ser1const  14009  rpexpmord  14119  mulsubdivbinom2  14213  faclbnd  14241  bcval4  14258  bcpasc  14272  hashkf  14283  hashunx  14337  fz1isolem  14412  ishashinf  14414  seqcoll  14415  ccatval1  14528  ccatval21sw  14537  ccatrn  14541  ccatalpha  14545  swrdnd0  14609  swrd0  14610  swrdfv2  14613  swrdspsleq  14617  addlenpfx  14642  ccatpfx  14652  swrdswrd  14656  pfxccatin12lem2  14682  pfxccat3  14685  swrdccat  14686  revccat  14717  repswswrd  14735  cshwmodn  14746  cshwidxmod  14754  repswcshw  14763  2cshwid  14765  2cshwcom  14767  2cshwcshw  14776  cshwcshid  14778  cshwcsh2id  14779  s1co  14784  cshco  14787  trclub  14949  shftfval  15021  seqshft  15036  crim  15066  caubnd  15310  limsuplt  15430  isercolllem2  15617  fsumcvg  15663  fsumcvg2  15678  fsumshftm  15732  fsumo1  15764  isumshft  15793  harmonic  15813  cvgrat  15837  mertenslem1  15838  zprod  15891  fprodmodd  15951  bpolylem  16002  bpolysum  16007  bpolydiflem  16008  fsumkthpow  16010  rpnnen2lem12  16181  dvdsval3  16214  negdvdsb  16230  dvdsnegb  16231  dvdsmul1  16235  dvdsabseq  16271  dvdsssfz1  16276  odd2np1  16299  divalglem8  16358  ndvdsadd  16368  dfgcd2  16504  dvdssqim  16512  nn0seqcvgd  16528  seq1st  16529  algcvgblem  16535  lcmf  16591  lcmfunsnlem2  16598  cncongr2  16626  prmdvdsfz  16664  isprm7  16667  prmndvdsfaclt  16684  powm2modprm  16763  modprm0  16765  modprmn0modprm0  16767  pythagtriplem1  16776  pythagtriplem4  16779  pythagtriplem8  16783  pythagtriplem9  16784  pythagtriplem12  16786  pythagtriplem14  16788  pythagtriplem16  16790  pcexp  16819  pc2dvds  16839  pcz  16841  fldivp1  16857  pcfac  16859  oddprmdvds  16863  pockthg  16866  infpnlem1  16870  prmreclem1  16876  prmreclem2  16877  1arith  16887  4sqlem11  16915  vdwlem2  16942  vdwlem8  16948  vdwnnlem2  16956  prmgaplem7  17017  prmgaplem8  17018  cshwshashlem2  17056  cshwshashlem3  17057  pwsval  17438  isacs1i  17612  funcsetcestrclem9  18118  ismgmid  18622  mgmhmpropd  18655  mhmpropd  18749  smndex1gid  18861  smndex1gidOLD  18862  smndex1id  18871  grpsubid1  18990  mulgnnp1  19047  mulgsubcl  19053  mulgnn0z  19066  mulgnndir  19068  mulgneg2  19073  lagsubg  19159  ghmco  19200  symg2bas  19357  symgextfv  19382  pgpfi2  19570  efgsfo  19703  frgpupf  19737  frgpup1  19739  gsummptshft  19900  telgsumfzslem  19952  telgsums  19957  ablfac1eu  20039  pgpfac1lem2  20041  ablfaclem3  20053  dvdsrid  20336  dvdsrneg  20339  dvr1  20376  abv1  20791  lmodfopne  20884  lbsexg  21152  xrsds  21397  znf1o  21539  lindfmm  21815  gsummoncoe1  22282  matecl  22399  mavmul0g  22527  gsummatr01  22633  mp2pm2mplem4  22783  chfacfisf  22828  chfacfisfcpmat  22829  chfacfpmmulgsum2  22839  cpmadugsumlemF  22850  isclo  23061  resttopon  23135  restcld  23146  restcls  23155  iscn  23209  iscnp  23211  cnco  23240  cndis  23265  cnindis  23266  cmpsub  23374  hauscmplem  23380  cmpfii  23383  ptcnplem  23595  txtube  23614  txcmplem1  23615  xkoptsub  23628  qtoptop  23674  kqfval  23697  hmeoco  23746  fileln0  23824  trfil1  23860  trfil2  23861  trufil  23884  elfm3  23924  hausflf2  23972  isucn  24251  bl2in  24374  metss2lem  24485  metss2  24486  stdbdxmet  24489  metrest  24498  nmval2  24566  nmoix  24703  ioo2bl  24767  xrsxmet  24784  expcn  24848  elcncf  24865  icccvx  24926  cphsscph  25227  iscmet3  25269  causs  25274  metcld2  25283  metsscmetcld  25291  cncmet  25298  bcth3  25307  ovolgelb  25456  ovolfi  25470  shft2rab  25484  uniioombllem3  25561  dyadmax  25574  dyadmbl  25576  subopnmbl  25580  volcn  25582  mbfid  25611  mbfeqalem2  25618  mbfres  25620  cnmbf  25635  i1fmulc  25679  mbfi1fseqlem3  25693  mbfi1fseqlem4  25694  itg2seq  25718  itg2gt0  25736  itgss3  25791  dvexp  25929  plypow  26182  plyeq0lem  26187  coeidlem  26214  dgrlt  26243  dgrcolem2  26251  elqaalem2  26299  aacjcl  26306  aaliou3lem1  26321  aaliou3lem2  26322  pserdvlem2  26409  abelthlem8  26420  cosord  26511  sinord  26514  resinf1o  26516  relogexp  26576  logdivlt  26601  advlogexp  26635  logcxp  26649  cxpcl  26654  rpcxpcl  26656  cxpne0  26657  logbchbase  26752  logbgt0b  26774  birthdaylem2  26933  cxplim  26953  divsqrtsumo1  26965  zetacvg  26996  wilthlem1  27049  ftalem7  27060  basellem1  27062  issqf  27117  sqf11  27120  sgmf  27126  sgmnncl  27128  sqff1o  27163  dvdsflsumcom  27169  mpodvdsmulf1o  27175  dvdsmulf1o  27177  sgmppw  27179  chtublem  27193  chtub  27194  logexprlim  27207  bposlem3  27268  bposlem5  27270  bposlem6  27271  lgsdirnn0  27326  gausslemma2dlem1a  27347  gausslemma2dlem5a  27352  lgsquad2  27368  lgsquad3  27369  2sqreulem1  27428  2sqreunnlem1  27431  dchrisumlem1  27471  dchrisumlem2  27472  dchrisumlem3  27473  mulogsumlem  27513  noextenddif  27651  addsrid  27975  ltnegs  28056  lenegs  28057  om2noseqlt2  28311  elzn0s  28409  eln0zs  28411  peano5uzs  28415  bdayfinbndlem1  28478  brbtwn  28987  uspgrupgrushgr  29267  usgrumgruspgr  29270  cusgrfilem2  29545  finsumvtxdg2ssteplem2  29635  cyclnumvtx  29888  crctcshwlkn0lem4  29901  crctcshwlkn0lem6  29903  crctcshwlkn0lem7  29904  crctcshwlkn0  29909  elwspths2spth  30058  rusgrnumwwlk  30066  clwlkclwwlklem2fv2  30086  erclwwlknref  30159  1to2vfriswmgr  30369  4cycl2v2nb  30379  frgr2wwlkeqm  30421  nvo00  30852  nmorepnf  30859  ubthlem1  30961  normpyc  31237  occon3  31388  pjpreeq  31489  idcnop  32072  riesz3i  32153  cnlnssadj  32171  rnbra  32198  strlem3a  32343  cvcon3  32375  ssdmd1  32404  ssdmd2  32405  relfi  32692  fcobijfs2  32815  fzsplit3  32886  prmsimpcyc  33309  esumcst  34228  dmvlsiga  34294  ballotlemimin  34671  bnj545  35058  bnj929  35099  bnj953  35102  fineqvnttrclselem1  35286  pthhashvtx  35331  derangsn  35373  iscvm  35462  cvmsval  35469  cvmliftlem7  35494  cvmlift2lem12  35517  mclsssvlem  35765  supfz  35932  faclimlem3  35948  opnrebl2  36524  nn0prpwlem  36525  tailval  36576  nndivlub  36661  ctbssinf  37733  finixpnum  37937  ltflcei  37940  lindsdom  37946  lindsenlbs  37947  matunitlindflem2  37949  poimirlem4  37956  poimirlem14  37966  poimirlem15  37967  poimirlem19  37971  poimirlem20  37972  poimirlem22  37974  poimirlem24  37976  poimirlem28  37980  poimirlem30  37982  poimirlem31  37983  mblfinlem2  37990  mblfinlem3  37991  mblfinlem4  37992  ftc1anclem1  38025  ftc1anclem4  38028  ftc1anclem5  38029  ftc1anclem7  38031  ftc1anclem8  38032  ftc1anc  38033  caushft  38093  ismtyval  38132  heiborlem7  38149  heiborlem10  38152  heibor  38153  lcmineqlem8  42486  deg1gprod  42590  f1o2d2  42685  oexpreposd  42765  elrfirn  43138  ismrc  43144  nacsfix  43155  mzpcompact2lem  43194  eldiophb  43200  ellz1  43210  rexrabdioph  43237  congrep  43416  jm2.26a  43443  rngunsnply  43612  mendring  43631  iocmbl  43656  oeord2lim  43752  cantnfresb  43767  omabs2  43775  ofoafg  43797  dfno2  43870  rp-isfinite5  43959  enrelmap  44439  expgrowthi  44775  cnfex  45474  xlimclim2lem  46282  climxlim2  46289  icccncfext  46330  itgsinexp  46398  iblspltprt  46416  itgspltprt  46422  fourierdlem50  46599  fourierswlem  46673  etransclem35  46712  zm1nn  47747  subsubelfzo0  47772  ceilbi  47782  addmodne  47795  m1modmmod  47809  modlt0b  47814  iccpartres  47875  iccelpart  47890  iccpartiun  47891  iccpartnel  47895  nprmmul1  47984  goldbachthlem1  48005  goldbachth  48007  odz2prm2pw  48023  2pwp1prm  48049  evenltle  48190  fpprwpprb  48213  sbgoldbaltlem2  48253  bgoldbachlt  48286  isubgredg  48339  gricushgr  48390  uhgrimisgrgriclem  48403  gpgvtx0  48526  gpg5nbgrvtx13starlem2  48545  upgrwlkupwlk  48613  2zrngamgm  48718  lincresunit3  48954  lincreslvec3  48955  isldepslvec2  48958  blengt1fldiv2p1  49066  dignn0flhalf  49091  nn0sumshdiglemA  49092  rrx2pnedifcoorneor  49189  precofval2  49841  aacllem  50273