Theorem syl2anr 596

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 595	. 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 206  df-an 396

This theorem is referenced by:  swopo  5505  ordintdif  6300  funco  6458  resdif  6720  fvcofneq  6951  fnprb  7066  fntpb  7067  isotr  7187  weisoeq  7206  brrpssg  7556  findsg  7720  coexg  7750  xpexgALT  7797  fnsuppres  7978  wfrlem10OLD  8120  oaass  8354  oeword  8383  oeworde  8386  mapsnd  8632  ixpssmapg  8674  enrefnn  8791  pw2f1olem  8816  domsdomtr  8848  xpen  8876  mapen  8877  mapdom1  8878  mapfienlem1  9094  elfir  9104  wdomen2  9266  carden2b  9656  harcard  9667  isinffi  9681  acnlem  9735  acndom  9738  alephdom  9768  fin23lem21  10026  fin23lem39  10037  isf32lem5  10044  fin1a2lem12  10098  axdc3lem2  10138  ttukeylem1  10196  pwcfsdom  10270  canthp1  10341  nqereu  10616  addpqf  10631  axmulf  10833  axmulass  10844  axdistr  10845  ltaddnegr  11121  negeu  11141  fimaxre3  11851  nnsub  11947  nn0sub  12213  ltsubnn0  12214  elz2  12267  uzaddcl  12573  qaddcl  12634  xltneg  12880  xleneg  12881  supxrbnd1  12984  infxrgelb  12998  iccneg  13133  uzsubsubfz  13207  fzsplit2  13210  fzadd2  13220  fzss1  13224  uzsplit  13257  fz0fzdiffz0  13294  difelfzle  13298  difelfznle  13299  fvffz0  13303  preduz  13307  predfz  13310  fzonlt0  13338  fzouzsplit  13350  fzo0addelr  13370  eluzgtdifelfzo  13377  elfzodifsumelfzo  13381  ssfzo12  13408  elfznelfzob  13421  fllt  13454  flflp1  13455  uzsup  13511  negmod  13564  modifeq2int  13581  modfzo0difsn  13591  modsumfzodifsn  13592  om2uzlt2i  13599  nn0ennn  13627  suppssfz  13642  seqfveq2  13673  sermono  13683  seqf1o  13692  ser1const  13707  rpexpmord  13814  mulsubdivbinom2  13904  faclbnd  13932  bcval4  13949  bcpasc  13963  hashkf  13974  hashunx  14029  hashfacenOLD  14095  fz1isolem  14103  ishashinf  14105  seqcoll  14106  ccatval1  14209  ccatval21sw  14218  ccatrn  14222  ccatalpha  14226  swrdnd0  14298  swrd0  14299  swrdfv2  14302  swrdspsleq  14306  addlenpfx  14332  ccatpfx  14342  swrdswrd  14346  pfxccatin12lem2  14372  pfxccat3  14375  swrdccat  14376  revccat  14407  repswswrd  14425  cshwmodn  14436  cshwidxmod  14444  repswcshw  14453  2cshwid  14455  2cshwcom  14457  2cshwcshw  14466  cshwcshid  14468  cshwcsh2id  14469  s1co  14474  cshco  14477  trclub  14637  shftfval  14709  seqshft  14724  crim  14754  caubnd  14998  limsuplt  15116  isercolllem2  15305  fsumcvg  15352  fsumcvg2  15367  fsumshftm  15421  fsumo1  15452  isumshft  15479  harmonic  15499  cvgrat  15523  mertenslem1  15524  zprod  15575  fprodmodd  15635  bpolylem  15686  bpolysum  15691  bpolydiflem  15692  fsumkthpow  15694  rpnnen2lem12  15862  dvdsval3  15895  negdvdsb  15910  dvdsnegb  15911  dvdsmul1  15915  dvdsabseq  15950  dvdsssfz1  15955  odd2np1  15978  divalglem8  16037  ndvdsadd  16047  dfgcd2  16182  dvdssqim  16192  nn0seqcvgd  16203  seq1st  16204  algcvgblem  16210  lcmf  16266  lcmfunsnlem2  16273  cncongr2  16301  prmdvdsfz  16338  isprm7  16341  prmndvdsfaclt  16358  powm2modprm  16432  modprm0  16434  modprmn0modprm0  16436  pythagtriplem1  16445  pythagtriplem4  16448  pythagtriplem8  16452  pythagtriplem9  16453  pythagtriplem12  16455  pythagtriplem14  16457  pythagtriplem16  16459  pcexp  16488  pc2dvds  16508  pcz  16510  fldivp1  16526  pcfac  16528  oddprmdvds  16532  pockthg  16535  infpnlem1  16539  prmreclem1  16545  prmreclem2  16546  1arith  16556  4sqlem11  16584  vdwlem2  16611  vdwlem8  16617  vdwnnlem2  16625  prmgaplem7  16686  prmgaplem8  16687  cshwshashlem2  16726  cshwshashlem3  16727  pwsval  17114  isacs1i  17283  funcsetcestrclem9  17796  ismgmid  18264  mhmpropd  18351  smndex1gid  18457  smndex1id  18465  grpsubid1  18575  mulgnnp1  18627  mulgsubcl  18633  mulgnn0z  18645  mulgnndir  18647  mulgneg2  18652  lagsubg  18733  ghmco  18769  symg2bas  18915  symgextfv  18941  pgpfi2  19126  efgsfo  19260  frgpupf  19294  frgpup1  19296  gsummptshft  19452  telgsumfzslem  19504  telgsums  19509  ablfac1eu  19591  pgpfac1lem2  19593  ablfaclem3  19605  dvdsrid  19808  dvdsrneg  19811  dvr1  19846  abv1  20008  lmodfopne  20076  lbsexg  20341  xrsds  20553  znf1o  20671  lindfmm  20944  gsummoncoe1  21385  matecl  21482  mavmul0g  21610  gsummatr01  21716  mp2pm2mplem4  21866  chfacfisf  21911  chfacfisfcpmat  21912  chfacfpmmulgsum2  21922  cpmadugsumlemF  21933  isclo  22146  resttopon  22220  restcld  22231  restcls  22240  iscn  22294  iscnp  22296  cnco  22325  cndis  22350  cnindis  22351  cmpsub  22459  hauscmplem  22465  cmpfii  22468  ptcnplem  22680  txtube  22699  txcmplem1  22700  xkoptsub  22713  qtoptop  22759  kqfval  22782  hmeoco  22831  fileln0  22909  trfil1  22945  trfil2  22946  trufil  22969  elfm3  23009  hausflf2  23057  isucn  23338  bl2in  23461  metss2lem  23573  metss2  23574  stdbdxmet  23577  metrest  23586  nmval2  23654  nmoix  23799  ioo2bl  23862  xrsxmet  23878  expcn  23941  elcncf  23958  icccvx  24019  cphsscph  24320  iscmet3  24362  causs  24367  metcld2  24376  metsscmetcld  24384  cncmet  24391  bcth3  24400  ovolgelb  24549  ovolfi  24563  shft2rab  24577  uniioombllem3  24654  dyadmax  24667  dyadmbl  24669  subopnmbl  24673  volcn  24675  mbfid  24704  mbfeqalem2  24711  mbfres  24713  cnmbf  24728  i1fmulc  24773  mbfi1fseqlem3  24787  mbfi1fseqlem4  24788  itg2seq  24812  itg2gt0  24830  itgss3  24884  dvexp  25022  plypow  25271  plyeq0lem  25276  coeidlem  25303  dgrlt  25332  dgrcolem2  25340  elqaalem2  25385  aacjcl  25392  aaliou3lem1  25407  aaliou3lem2  25408  pserdvlem2  25492  abelthlem8  25503  cosord  25592  sinord  25595  resinf1o  25597  relogexp  25656  logdivlt  25681  advlogexp  25715  logcxp  25729  cxpcl  25734  rpcxpcl  25736  cxpne0  25737  logbchbase  25826  logbgt0b  25848  birthdaylem2  26007  cxplim  26026  divsqrtsumo1  26038  zetacvg  26069  wilthlem1  26122  ftalem7  26133  basellem1  26135  issqf  26190  sqf11  26193  sgmf  26199  sgmnncl  26201  sqff1o  26236  dvdsflsumcom  26242  dvdsmulf1o  26248  sgmppw  26250  chtublem  26264  chtub  26265  logexprlim  26278  bposlem3  26339  bposlem5  26341  bposlem6  26342  lgsdirnn0  26397  gausslemma2dlem1a  26418  gausslemma2dlem5a  26423  lgsquad2  26439  lgsquad3  26440  2sqreulem1  26499  2sqreunnlem1  26502  dchrisumlem1  26542  dchrisumlem2  26543  dchrisumlem3  26544  mulogsumlem  26584  brbtwn  27170  uspgrupgrushgr  27450  usgrumgruspgr  27453  cusgrfilem2  27726  finsumvtxdg2ssteplem2  27816  crctcshwlkn0lem4  28079  crctcshwlkn0lem6  28081  crctcshwlkn0lem7  28082  crctcshwlkn0  28087  elwspths2spth  28233  rusgrnumwwlk  28241  clwlkclwwlklem2fv2  28261  erclwwlknref  28334  1to2vfriswmgr  28544  4cycl2v2nb  28554  frgr2wwlkeqm  28596  nvo00  29024  nmorepnf  29031  ubthlem1  29133  normpyc  29409  occon3  29560  pjpreeq  29661  idcnop  30244  riesz3i  30325  cnlnssadj  30343  rnbra  30370  strlem3a  30515  cvcon3  30547  ssdmd1  30576  ssdmd2  30577  relfi  30842  fzsplit3  31017  prmsimpcyc  31383  esumcst  31931  dmvlsiga  31997  ballotlemimin  32372  bnj545  32775  bnj929  32816  bnj953  32819  pthhashvtx  32989  derangsn  33032  iscvm  33121  cvmsval  33128  cvmliftlem7  33153  cvmlift2lem12  33176  mclsssvlem  33424  supfz  33600  faclimlem3  33617  noextenddif  33798  addsid1  34054  opnrebl2  34437  nn0prpwlem  34438  tailval  34489  nndivlub  34574  ctbssinf  35504  finixpnum  35689  ltflcei  35692  lindsdom  35698  lindsenlbs  35699  matunitlindflem2  35701  poimirlem4  35708  poimirlem14  35718  poimirlem15  35719  poimirlem19  35723  poimirlem20  35724  poimirlem22  35726  poimirlem24  35728  poimirlem28  35732  poimirlem30  35734  poimirlem31  35735  mblfinlem2  35742  mblfinlem3  35743  mblfinlem4  35744  ftc1anclem1  35777  ftc1anclem4  35780  ftc1anclem5  35781  ftc1anclem7  35783  ftc1anclem8  35784  ftc1anc  35785  caushft  35846  ismtyval  35885  heiborlem7  35902  heiborlem10  35905  heibor  35906  lcmineqlem8  39972  oexpreposd  40242  elrfirn  40433  ismrc  40439  nacsfix  40450  mzpcompact2lem  40489  eldiophb  40495  ellz1  40505  rexrabdioph  40532  congrep  40711  jm2.26a  40738  rngunsnply  40914  mendring  40933  iocmbl  40960  rp-isfinite5  41022  enrelmap  41494  expgrowthi  41840  cnfex  42460  xlimclim2lem  43270  climxlim2  43277  icccncfext  43318  itgsinexp  43386  iblspltprt  43404  itgspltprt  43410  fourierdlem50  43587  fourierswlem  43661  etransclem35  43700  zm1nn  44682  subsubelfzo0  44706  iccpartres  44758  iccelpart  44773  iccpartiun  44774  iccpartnel  44778  goldbachthlem1  44885  goldbachth  44887  odz2prm2pw  44903  2pwp1prm  44929  evenltle  45057  fpprwpprb  45080  sbgoldbaltlem2  45120  bgoldbachlt  45153  isomushgr  45166  isomuspgrlem1  45167  isomgrtr  45179  upgrwlkupwlk  45190  mgmhmpropd  45227  2zrngamgm  45385  lincresunit3  45710  lincreslvec3  45711  isldepslvec2  45714  m1modmmod  45755  blengt1fldiv2p1  45827  dignn0flhalf  45852  nn0sumshdiglemA  45853  rrx2pnedifcoorneor  45950  aacllem  46391