Theorem syl2anr 603

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 602	. 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 208  df-an 397

This theorem is referenced by:  swopo  5544  ordintdif  6368  funco  6532  resdif  6795  fvcofneq  7041  fnprb  7159  fntpb  7160  fvf1pr  7258  isotr  7287  weisoeq  7306  brrpssg  7675  findsg  7844  coexg  7876  resf1extb  7881  xpexgALT  7930  mpof1o2d  8072  fnsuppres  8138  oaass  8493  oeword  8523  oeworde  8526  mapsnd  8831  ixpssmapg  8873  enrefnn  8990  pw2f1olem  9016  domsdomtr  9047  xpen  9075  mapen  9076  mapdom1  9077  phplem2  9136  mapfienlem1  9315  elfir  9325  wdomen2  9489  carden2b  9889  harcard  9900  isinffi  9914  acnlem  9968  acndom  9971  alephdom  10001  fin23lem21  10259  fin23lem39  10270  isf32lem5  10277  fin1a2lem12  10331  axdc3lem2  10371  ttukeylem1  10429  pwcfsdom  10504  canthp1  10575  nqereu  10850  addpqf  10865  axmulf  11067  axmulass  11078  axdistr  11079  ltaddnegr  11361  negeu  11381  fimaxre3  12100  nnsub  12219  nn0sub  12485  ltsubnn0  12486  elz2  12540  uzaddcl  12852  qaddcl  12913  xltneg  13167  xleneg  13168  supxrbnd1  13271  infxrgelb  13286  iccneg  13423  uzsubsubfz  13498  fzsplit2  13501  fzadd2  13511  fzss1  13515  uzsplit  13548  fzdif1  13557  fz0fzdiffz0  13589  difelfzle  13593  difelfznle  13594  fvffz0  13598  preduz  13602  predfz  13605  fzonlt0  13635  fzouzsplit  13647  fzo0addelr  13672  eluzgtdifelfzo  13680  elfzodifsumelfzo  13684  ssfzo12  13712  elfznelfzob  13727  fllt  13763  flflp1  13764  uzsup  13820  negmod  13876  modifeq2int  13893  modfzo0difsn  13903  modsumfzodifsn  13904  om2uzlt2i  13911  nn0ennn  13939  suppssfz  13954  seqfveq2  13984  sermono  13994  seqf1o  14003  ser1const  14018  rpexpmord  14128  mulsubdivbinom2  14222  faclbnd  14250  bcval4  14267  bcpasc  14281  hashkf  14292  hashunx  14346  fz1isolem  14421  ishashinf  14423  seqcoll  14424  ccatval1  14537  ccatval21sw  14546  ccatrn  14550  ccatalpha  14554  swrdnd0  14618  swrd0  14619  swrdfv2  14622  swrdspsleq  14626  addlenpfx  14651  ccatpfx  14661  swrdswrd  14665  pfxccatin12lem2  14691  pfxccat3  14694  swrdccat  14695  revccat  14726  repswswrd  14744  cshwmodn  14755  cshwidxmod  14763  repswcshw  14772  2cshwid  14774  2cshwcom  14776  2cshwcshw  14785  cshwcshid  14787  cshwcsh2id  14788  s1co  14793  cshco  14796  trclub  14958  shftfval  15030  seqshft  15045  crim  15075  caubnd  15319  limsuplt  15439  isercolllem2  15626  fsumcvg  15672  fsumcvg2  15687  fsumshftm  15741  fsumo1  15773  isumshft  15802  harmonic  15822  cvgrat  15846  mertenslem1  15847  zprod  15900  fprodmodd  15960  bpolylem  16011  bpolysum  16016  bpolydiflem  16017  fsumkthpow  16019  rpnnen2lem12  16190  dvdsval3  16223  negdvdsb  16239  dvdsnegb  16240  dvdsmul1  16244  dvdsabseq  16280  dvdsssfz1  16285  odd2np1  16308  divalglem8  16367  ndvdsadd  16377  dfgcd2  16513  dvdssqim  16521  nn0seqcvgd  16537  seq1st  16538  algcvgblem  16544  lcmf  16600  lcmfunsnlem2  16607  cncongr2  16635  prmdvdsfz  16673  isprm7  16676  prmndvdsfaclt  16693  powm2modprm  16772  modprm0  16774  modprmn0modprm0  16776  pythagtriplem1  16785  pythagtriplem4  16788  pythagtriplem8  16792  pythagtriplem9  16793  pythagtriplem12  16795  pythagtriplem14  16797  pythagtriplem16  16799  pcexp  16828  pc2dvds  16848  pcz  16850  fldivp1  16866  pcfac  16868  oddprmdvds  16872  pockthg  16875  infpnlem1  16879  prmreclem1  16885  prmreclem2  16886  1arith  16896  4sqlem11  16924  vdwlem2  16951  vdwlem8  16957  vdwnnlem2  16965  prmgaplem7  17026  prmgaplem8  17027  cshwshashlem2  17065  cshwshashlem3  17066  pwsval  17447  isacs1i  17621  funcsetcestrclem9  18127  ismgmid  18631  mgmhmpropd  18664  mhmpropd  18758  smndex1gid  18870  smndex1gidOLD  18871  smndex1id  18880  grpsubid1  18999  mulgnnp1  19056  mulgsubcl  19062  mulgnn0z  19075  mulgnndir  19077  mulgneg2  19082  lagsubg  19168  ghmco  19209  symg2bas  19366  symgextfv  19391  pgpfi2  19579  efgsfo  19712  frgpupf  19746  frgpup1  19748  gsummptshft  19909  telgsumfzslem  19961  telgsums  19966  ablfac1eu  20048  pgpfac1lem2  20050  ablfaclem3  20062  dvdsrid  20345  dvdsrneg  20348  dvr1  20385  abv1  20804  lmodfopne  20897  lbsexg  21164  xrsds  21392  znf1o  21533  lindfmm  21809  gsummoncoe1  22301  matecl  22415  mavmul0g  22543  gsummatr01  22649  mp2pm2mplem4  22799  chfacfisf  22844  chfacfisfcpmat  22845  chfacfpmmulgsum2  22855  cpmadugsumlemF  22866  isclo  23077  resttopon  23151  restcld  23162  restcls  23171  iscn  23225  iscnp  23227  cnco  23256  cndis  23281  cnindis  23282  cmpsub  23390  hauscmplem  23396  cmpfii  23399  ptcnplem  23611  txtube  23630  txcmplem1  23631  xkoptsub  23644  qtoptop  23690  kqfval  23713  hmeoco  23762  fileln0  23840  trfil1  23876  trfil2  23877  trufil  23900  elfm3  23940  hausflf2  23988  isucn  24267  bl2in  24390  metss2lem  24501  metss2  24502  stdbdxmet  24505  metrest  24514  nmval2  24582  nmoix  24719  ioo2bl  24783  xrsxmet  24800  expcn  24864  elcncf  24881  icccvx  24942  cphsscph  25243  iscmet3  25285  causs  25290  metcld2  25299  metsscmetcld  25307  cncmet  25314  bcth3  25323  ovolgelb  25472  ovolfi  25486  shft2rab  25500  uniioombllem3  25577  dyadmax  25590  dyadmbl  25592  subopnmbl  25596  volcn  25598  mbfid  25627  mbfeqalem2  25634  mbfres  25636  cnmbf  25651  i1fmulc  25695  mbfi1fseqlem3  25709  mbfi1fseqlem4  25710  itg2seq  25734  itg2gt0  25752  itgss3  25807  dvexp  25945  plypow  26195  plyeq0lem  26200  coeidlem  26227  dgrlt  26256  dgrcolem2  26264  elqaalem2  26311  aacjcl  26318  aaliou3lem1  26333  aaliou3lem2  26334  pserdvlem2  26418  abelthlem8  26429  cosord  26520  sinord  26523  resinf1o  26525  relogexp  26585  logdivlt  26610  advlogexp  26644  logcxp  26658  cxpcl  26663  rpcxpcl  26665  cxpne0  26666  logbchbase  26760  logbgt0b  26782  birthdaylem2  26941  cxplim  26960  divsqrtsumo1  26972  zetacvg  27003  wilthlem1  27056  ftalem7  27067  basellem1  27069  issqf  27124  sqf11  27127  sgmf  27133  sgmnncl  27135  sqff1o  27170  dvdsflsumcom  27176  mpodvdsmulf1o  27182  dvdsmulf1o  27184  sgmppw  27185  chtublem  27199  chtub  27200  logexprlim  27213  bposlem3  27274  bposlem5  27276  bposlem6  27277  lgsdirnn0  27332  gausslemma2dlem1a  27353  gausslemma2dlem5a  27358  lgsquad2  27374  lgsquad3  27375  2sqreulem1  27434  2sqreunnlem1  27437  dchrisumlem1  27477  dchrisumlem2  27478  dchrisumlem3  27479  mulogsumlem  27519  noextenddif  27657  addsrid  27981  ltnegs  28062  lenegs  28063  om2noseqlt2  28317  elzn0s  28415  eln0zs  28417  peano5uzs  28421  bdayfinbndlem1  28484  brbtwn  28993  uspgrupgrushgr  29273  usgrumgruspgr  29276  cusgrfilem2  29550  finsumvtxdg2ssteplem2  29640  cyclnumvtx  29893  crctcshwlkn0lem4  29906  crctcshwlkn0lem6  29908  crctcshwlkn0lem7  29909  crctcshwlkn0  29914  elwspths2spth  30063  rusgrnumwwlk  30071  clwlkclwwlklem2fv2  30091  erclwwlknref  30164  1to2vfriswmgr  30374  4cycl2v2nb  30384  frgr2wwlkeqm  30426  nvo00  30857  nmorepnf  30864  ubthlem1  30966  normpyc  31242  occon3  31393  pjpreeq  31494  idcnop  32077  riesz3i  32158  cnlnssadj  32176  rnbra  32203  strlem3a  32348  cvcon3  32380  ssdmd1  32409  ssdmd2  32410  relfi  32698  fcobijfs2  32821  fzsplit3  32892  prmsimpcyc  33316  esumcst  34254  dmvlsiga  34320  ballotlemimin  34697  bnj545  35084  bnj929  35125  bnj953  35128  fineqvnttrclselem1  35312  pthhashvtx  35357  derangsn  35399  iscvm  35488  cvmsval  35495  cvmliftlem7  35520  cvmlift2lem12  35543  mclsssvlem  35791  supfz  35958  faclimlem3  35974  opnrebl2  36550  nn0prpwlem  36551  tailval  36602  nndivlub  36687  ctbssinf  37769  finixpnum  37973  ltflcei  37976  lindsdom  37982  lindsenlbs  37983  matunitlindflem2  37985  poimirlem4  37992  poimirlem14  38002  poimirlem15  38003  poimirlem19  38007  poimirlem20  38008  poimirlem22  38010  poimirlem24  38012  poimirlem28  38016  poimirlem30  38018  poimirlem31  38019  mblfinlem2  38026  mblfinlem3  38027  mblfinlem4  38028  ftc1anclem1  38061  ftc1anclem4  38064  ftc1anclem5  38065  ftc1anclem7  38067  ftc1anclem8  38068  ftc1anc  38069  caushft  38129  ismtyval  38168  heiborlem7  38185  heiborlem10  38188  heibor  38189  lcmineqlem8  42522  deg1gprod  42626  oexpreposd  42800  elrfirn  43145  ismrc  43151  nacsfix  43162  mzpcompact2lem  43201  eldiophb  43207  ellz1  43217  rexrabdioph  43240  congrep  43419  jm2.26a  43446  rngunsnply  43615  mendring  43634  iocmbl  43659  oeord2lim  43755  cantnfresb  43770  omabs2  43778  ofoafg  43800  dfno2  43873  rp-isfinite5  43962  enrelmap  44442  expgrowthi  44778  cnfex  45477  xlimclim2lem  46283  climxlim2  46290  icccncfext  46331  itgsinexp  46399  iblspltprt  46417  itgspltprt  46423  fourierdlem50  46600  fourierswlem  46674  etransclem35  46713  zm1nn  47766  subsubelfzo0  47791  ceilbi  47801  addmodne  47814  m1modmmod  47828  modlt0b  47833  iccpartres  47894  iccelpart  47909  iccpartiun  47910  iccpartnel  47914  nprmmul1  48003  goldbachthlem1  48024  goldbachth  48026  odz2prm2pw  48042  2pwp1prm  48068  evenltle  48209  fpprwpprb  48232  sbgoldbaltlem2  48272  bgoldbachlt  48305  isubgredg  48358  gricushgr  48409  uhgrimisgrgriclem  48422  gpgvtx0  48545  gpg5nbgrvtx13starlem2  48564  upgrwlkupwlk  48632  2zrngamgm  48737  lincresunit3  48973  lincreslvec3  48974  isldepslvec2  48977  blengt1fldiv2p1  49085  dignn0flhalf  49110  nn0sumshdiglemA  49111  rrx2pnedifcoorneor  49208  precofval2  49860  aacllem  50292