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  5540  ordintdif  6365  funco  6529  resdif  6792  fvcofneq  7035  fnprb  7151  fntpb  7152  fvf1pr  7250  isotr  7279  weisoeq  7298  brrpssg  7667  findsg  7836  coexg  7868  resf1extb  7873  xpexgALT  7922  fnsuppres  8130  oaass  8485  oeword  8514  oeworde  8517  mapsnd  8819  ixpssmapg  8861  enrefnn  8978  pw2f1olem  9004  domsdomtr  9035  xpen  9063  mapen  9064  mapdom1  9065  phplem2  9124  mapfienlem1  9299  elfir  9309  wdomen2  9473  carden2b  9870  harcard  9881  isinffi  9895  acnlem  9949  acndom  9952  alephdom  9982  fin23lem21  10240  fin23lem39  10251  isf32lem5  10258  fin1a2lem12  10312  axdc3lem2  10352  ttukeylem1  10410  pwcfsdom  10484  canthp1  10555  nqereu  10830  addpqf  10845  axmulf  11047  axmulass  11058  axdistr  11059  ltaddnegr  11340  negeu  11360  fimaxre3  12078  nnsub  12179  nn0sub  12441  ltsubnn0  12442  elz2  12496  uzaddcl  12812  qaddcl  12873  xltneg  13126  xleneg  13127  supxrbnd1  13230  infxrgelb  13245  iccneg  13382  uzsubsubfz  13456  fzsplit2  13459  fzadd2  13469  fzss1  13473  uzsplit  13506  fzdif1  13515  fz0fzdiffz0  13547  difelfzle  13551  difelfznle  13552  fvffz0  13556  preduz  13560  predfz  13563  fzonlt0  13592  fzouzsplit  13604  fzo0addelr  13629  eluzgtdifelfzo  13637  elfzodifsumelfzo  13641  ssfzo12  13669  elfznelfzob  13684  fllt  13720  flflp1  13721  uzsup  13777  negmod  13833  modifeq2int  13850  modfzo0difsn  13860  modsumfzodifsn  13861  om2uzlt2i  13868  nn0ennn  13896  suppssfz  13911  seqfveq2  13941  sermono  13951  seqf1o  13960  ser1const  13975  rpexpmord  14085  mulsubdivbinom2  14179  faclbnd  14207  bcval4  14224  bcpasc  14238  hashkf  14249  hashunx  14303  fz1isolem  14378  ishashinf  14380  seqcoll  14381  ccatval1  14494  ccatval21sw  14503  ccatrn  14507  ccatalpha  14511  swrdnd0  14575  swrd0  14576  swrdfv2  14579  swrdspsleq  14583  addlenpfx  14608  ccatpfx  14618  swrdswrd  14622  pfxccatin12lem2  14648  pfxccat3  14651  swrdccat  14652  revccat  14683  repswswrd  14701  cshwmodn  14712  cshwidxmod  14720  repswcshw  14729  2cshwid  14731  2cshwcom  14733  2cshwcshw  14742  cshwcshid  14744  cshwcsh2id  14745  s1co  14750  cshco  14753  trclub  14915  shftfval  14987  seqshft  15002  crim  15032  caubnd  15276  limsuplt  15396  isercolllem2  15583  fsumcvg  15629  fsumcvg2  15644  fsumshftm  15698  fsumo1  15729  isumshft  15756  harmonic  15776  cvgrat  15800  mertenslem1  15801  zprod  15854  fprodmodd  15914  bpolylem  15965  bpolysum  15970  bpolydiflem  15971  fsumkthpow  15973  rpnnen2lem12  16144  dvdsval3  16177  negdvdsb  16193  dvdsnegb  16194  dvdsmul1  16198  dvdsabseq  16234  dvdsssfz1  16239  odd2np1  16262  divalglem8  16321  ndvdsadd  16331  dfgcd2  16467  dvdssqim  16475  nn0seqcvgd  16491  seq1st  16492  algcvgblem  16498  lcmf  16554  lcmfunsnlem2  16561  cncongr2  16589  prmdvdsfz  16626  isprm7  16629  prmndvdsfaclt  16646  powm2modprm  16725  modprm0  16727  modprmn0modprm0  16729  pythagtriplem1  16738  pythagtriplem4  16741  pythagtriplem8  16745  pythagtriplem9  16746  pythagtriplem12  16748  pythagtriplem14  16750  pythagtriplem16  16752  pcexp  16781  pc2dvds  16801  pcz  16803  fldivp1  16819  pcfac  16821  oddprmdvds  16825  pockthg  16828  infpnlem1  16832  prmreclem1  16838  prmreclem2  16839  1arith  16849  4sqlem11  16877  vdwlem2  16904  vdwlem8  16910  vdwnnlem2  16918  prmgaplem7  16979  prmgaplem8  16980  cshwshashlem2  17018  cshwshashlem3  17019  pwsval  17400  isacs1i  17573  funcsetcestrclem9  18079  ismgmid  18583  mgmhmpropd  18616  mhmpropd  18710  smndex1gid  18821  smndex1id  18829  grpsubid1  18948  mulgnnp1  19005  mulgsubcl  19011  mulgnn0z  19024  mulgnndir  19026  mulgneg2  19031  lagsubg  19117  ghmco  19158  symg2bas  19315  symgextfv  19340  pgpfi2  19528  efgsfo  19661  frgpupf  19695  frgpup1  19697  gsummptshft  19858  telgsumfzslem  19910  telgsums  19915  ablfac1eu  19997  pgpfac1lem2  19999  ablfaclem3  20011  dvdsrid  20295  dvdsrneg  20298  dvr1  20335  abv1  20750  lmodfopne  20843  lbsexg  21111  xrsds  21356  znf1o  21498  lindfmm  21774  gsummoncoe1  22233  matecl  22350  mavmul0g  22478  gsummatr01  22584  mp2pm2mplem4  22734  chfacfisf  22779  chfacfisfcpmat  22780  chfacfpmmulgsum2  22790  cpmadugsumlemF  22801  isclo  23012  resttopon  23086  restcld  23097  restcls  23106  iscn  23160  iscnp  23162  cnco  23191  cndis  23216  cnindis  23217  cmpsub  23325  hauscmplem  23331  cmpfii  23334  ptcnplem  23546  txtube  23565  txcmplem1  23566  xkoptsub  23579  qtoptop  23625  kqfval  23648  hmeoco  23697  fileln0  23775  trfil1  23811  trfil2  23812  trufil  23835  elfm3  23875  hausflf2  23923  isucn  24202  bl2in  24325  metss2lem  24436  metss2  24437  stdbdxmet  24440  metrest  24449  nmval2  24517  nmoix  24654  ioo2bl  24718  xrsxmet  24735  expcn  24800  expcnOLD  24802  elcncf  24819  icccvx  24885  cphsscph  25188  iscmet3  25230  causs  25235  metcld2  25244  metsscmetcld  25252  cncmet  25259  bcth3  25268  ovolgelb  25418  ovolfi  25432  shft2rab  25446  uniioombllem3  25523  dyadmax  25536  dyadmbl  25538  subopnmbl  25542  volcn  25544  mbfid  25573  mbfeqalem2  25580  mbfres  25582  cnmbf  25597  i1fmulc  25641  mbfi1fseqlem3  25655  mbfi1fseqlem4  25656  itg2seq  25680  itg2gt0  25698  itgss3  25753  dvexp  25894  plypow  26147  plyeq0lem  26152  coeidlem  26179  dgrlt  26209  dgrcolem2  26217  elqaalem2  26265  aacjcl  26272  aaliou3lem1  26287  aaliou3lem2  26288  pserdvlem2  26375  abelthlem8  26386  cosord  26477  sinord  26480  resinf1o  26482  relogexp  26542  logdivlt  26567  advlogexp  26601  logcxp  26615  cxpcl  26620  rpcxpcl  26622  cxpne0  26623  logbchbase  26718  logbgt0b  26740  birthdaylem2  26899  cxplim  26919  divsqrtsumo1  26931  zetacvg  26962  wilthlem1  27015  ftalem7  27026  basellem1  27028  issqf  27083  sqf11  27086  sgmf  27092  sgmnncl  27094  sqff1o  27129  dvdsflsumcom  27135  mpodvdsmulf1o  27141  dvdsmulf1o  27143  sgmppw  27145  chtublem  27159  chtub  27160  logexprlim  27173  bposlem3  27234  bposlem5  27236  bposlem6  27237  lgsdirnn0  27292  gausslemma2dlem1a  27313  gausslemma2dlem5a  27318  lgsquad2  27334  lgsquad3  27335  2sqreulem1  27394  2sqreunnlem1  27397  dchrisumlem1  27437  dchrisumlem2  27438  dchrisumlem3  27439  mulogsumlem  27479  noextenddif  27617  addsrid  27917  sltneg  27997  sleneg  27998  om2noseqlt2  28240  elzn0s  28332  eln0zs  28334  peano5uzs  28338  brbtwn  28888  uspgrupgrushgr  29168  usgrumgruspgr  29171  cusgrfilem2  29446  finsumvtxdg2ssteplem2  29536  cyclnumvtx  29789  crctcshwlkn0lem4  29802  crctcshwlkn0lem6  29804  crctcshwlkn0lem7  29805  crctcshwlkn0  29810  elwspths2spth  29959  rusgrnumwwlk  29967  clwlkclwwlklem2fv2  29987  erclwwlknref  30060  1to2vfriswmgr  30270  4cycl2v2nb  30280  frgr2wwlkeqm  30322  nvo00  30752  nmorepnf  30759  ubthlem1  30861  normpyc  31137  occon3  31288  pjpreeq  31389  idcnop  31972  riesz3i  32053  cnlnssadj  32071  rnbra  32098  strlem3a  32243  cvcon3  32275  ssdmd1  32304  ssdmd2  32305  relfi  32593  fcobijfs2  32716  fzsplit3  32787  prmsimpcyc  33208  esumcst  34087  dmvlsiga  34153  ballotlemimin  34530  bnj545  34918  bnj929  34959  bnj953  34962  fineqvnttrclselem1  35152  pthhashvtx  35183  derangsn  35225  iscvm  35314  cvmsval  35321  cvmliftlem7  35346  cvmlift2lem12  35369  mclsssvlem  35617  supfz  35784  faclimlem3  35800  opnrebl2  36376  nn0prpwlem  36377  tailval  36428  nndivlub  36513  ctbssinf  37461  finixpnum  37655  ltflcei  37658  lindsdom  37664  lindsenlbs  37665  matunitlindflem2  37667  poimirlem4  37674  poimirlem14  37684  poimirlem15  37685  poimirlem19  37689  poimirlem20  37690  poimirlem22  37692  poimirlem24  37694  poimirlem28  37698  poimirlem30  37700  poimirlem31  37701  mblfinlem2  37708  mblfinlem3  37709  mblfinlem4  37710  ftc1anclem1  37743  ftc1anclem4  37746  ftc1anclem5  37747  ftc1anclem7  37749  ftc1anclem8  37750  ftc1anc  37751  caushft  37811  ismtyval  37850  heiborlem7  37867  heiborlem10  37870  heibor  37871  lcmineqlem8  42139  deg1gprod  42243  f1o2d2  42341  oexpreposd  42430  elrfirn  42802  ismrc  42808  nacsfix  42819  mzpcompact2lem  42858  eldiophb  42864  ellz1  42874  rexrabdioph  42901  congrep  43080  jm2.26a  43107  rngunsnply  43276  mendring  43295  iocmbl  43320  oeord2lim  43416  cantnfresb  43431  omabs2  43439  ofoafg  43461  dfno2  43535  rp-isfinite5  43624  enrelmap  44104  expgrowthi  44440  cnfex  45139  xlimclim2lem  45951  climxlim2  45958  icccncfext  45999  itgsinexp  46067  iblspltprt  46085  itgspltprt  46091  fourierdlem50  46268  fourierswlem  46342  etransclem35  46381  zm1nn  47416  subsubelfzo0  47440  ceilbi  47447  addmodne  47458  m1modmmod  47472  modlt0b  47477  iccpartres  47532  iccelpart  47547  iccpartiun  47548  iccpartnel  47552  goldbachthlem1  47659  goldbachth  47661  odz2prm2pw  47677  2pwp1prm  47703  evenltle  47831  fpprwpprb  47854  sbgoldbaltlem2  47894  bgoldbachlt  47927  isubgredg  47980  gricushgr  48031  uhgrimisgrgriclem  48044  gpgvtx0  48167  gpg5nbgrvtx13starlem2  48186  upgrwlkupwlk  48254  2zrngamgm  48359  lincresunit3  48596  lincreslvec3  48597  isldepslvec2  48600  blengt1fldiv2p1  48708  dignn0flhalf  48733  nn0sumshdiglemA  48734  rrx2pnedifcoorneor  48831  precofval2  49484  aacllem  49916