Theorem syl2anr 609

Description: A double syllogism inference. For an implication-only version, see syl2imc 42. (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 608	. 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)
5	4	ancoms 464	1 ⊢ ((𝜏 ∧ 𝜑) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  swopo  5578  ordintdif  6413  funco  6577  resdif  6843  fvcofneq  7089  fnprb  7210  fntpb  7211  fvf1pr  7311  isotr  7340  weisoeq  7361  brrpssg  7729  findsg  7897  coexg  7929  resf1extb  7934  xpexgALT  7981  mpof1o2d  8126  fnsuppres  8192  oaass  8551  oeword  8581  oeworde  8584  mapsnd  8896  ixpssmapg  8938  enrefnn  9056  pw2f1olem  9082  domsdomtr  9113  xpen  9141  mapen  9142  mapdom1  9143  phplem2  9202  mapfienlem1  9378  elfir  9388  wdomen2  9552  carden2b  9975  harcard  9986  isinffi  10000  acnlem  10054  acndom  10057  alephdom  10087  fin23lem21  10344  fin23lem39  10355  isf32lem5  10362  fin1a2lem12  10416  axdc3lem2  10456  ttukeylem1  10514  pwcfsdom  10595  canthp1  10666  nqereu  10941  addpqf  10956  axmulf  11158  axmulass  11169  axdistr  11170  ltaddnegr  11454  negeu  11474  fimaxre3  12188  nnsub  12307  nn0sub  12581  ltsubnn0  12582  elz2  12636  uzaddcl  12956  qaddcl  13017  xltneg  13271  xleneg  13272  supxrbnd1  13375  infxrgelb  13390  iccneg  13527  uzsubsubfz  13603  fzsplit2  13606  fzadd2  13616  fzss1  13620  uzsplit  13653  fzdif1  13662  fz0fzdiffz0  13694  difelfzle  13698  difelfznle  13699  fvffz0  13703  preduz  13707  predfz  13710  fzonlt0  13740  fzouzsplit  13752  fzo0addelr  13777  eluzgtdifelfzo  13785  elfzodifsumelfzo  13789  ssfzo12  13817  elfznelfzob  13832  fllt  13869  flflp1  13870  uzsup  13926  negmod  13982  modifeq2int  13999  modfzo0difsn  14009  modsumfzodifsn  14010  om2uzlt2i  14017  nn0ennn  14045  suppssfz  14060  seqfveq2  14090  sermono  14100  seqf1o  14109  ser1const  14124  rpexpmord  14234  mulsubdivbinom2  14328  faclbnd  14356  bcval4  14373  bcpasc  14387  hashkf  14398  hashunx  14452  fz1isolem  14528  ishashinf  14530  seqcoll  14531  ccatval1  14644  ccatval21sw  14653  ccatrn  14657  ccatalpha  14662  swrdnd0  14729  swrd0  14730  swrdfv2  14733  swrdspsleq  14737  addlenpfx  14762  ccatpfx  14772  swrdswrd  14776  pfxccatin12lem2  14802  pfxccat3  14805  swrdccat  14806  revccat  14837  repswswrd  14857  cshwmodn  14868  cshwidxmod  14876  repswcshw  14885  2cshwid  14887  2cshwcom  14889  2cshwcshw  14898  cshwcshid  14900  cshwcsh2id  14901  s1co  14906  cshco  14909  trclub  15073  shftfval  15145  seqshft  15160  crim  15204  caubnd  15448  limsuplt  15568  isercolllem2  15755  fsumcvg  15800  fsumcvg2  15815  fsumshftm  15869  fsumo1  15901  isumshft  15930  harmonic  15950  cvgrat  15974  mertenslem1  15975  zprod  16028  fprodmodd  16088  bpolylem  16138  bpolysum  16143  bpolydiflem  16144  fsumkthpow  16146  rpnnen2lem12  16317  dvdsval3  16350  negdvdsb  16366  dvdsnegb  16367  dvdsmul1  16371  dvdsabseq  16407  dvdsssfz1  16412  odd2np1  16435  divalglem8  16494  ndvdsadd  16504  dfgcd2  16640  dvdssqim  16648  nn0seqcvgd  16664  seq1st  16665  algcvgblem  16671  lcmf  16727  lcmfunsnlem2  16734  cncongr2  16762  prmdvdsfz  16800  isprm7  16803  prmndvdsfaclt  16820  powm2modprm  16899  modprm0  16901  modprmn0modprm0  16903  pythagtriplem1  16912  pythagtriplem4  16915  pythagtriplem8  16919  pythagtriplem9  16920  pythagtriplem12  16922  pythagtriplem14  16924  pythagtriplem16  16926  pcexp  16955  pc2dvds  16975  pcz  16977  fldivp1  16993  pcfac  16995  oddprmdvds  16999  pockthg  17002  infpnlem1  17006  prmreclem1  17012  prmreclem2  17013  1arith  17023  4sqlem11  17051  vdwlem2  17078  vdwlem8  17084  vdwnnlem2  17092  prmgaplem7  17153  prmgaplem8  17154  cshwshashlem2  17192  cshwshashlem3  17193  pwsval  17575  isacs1i  17749  funcsetcestrclem9  18255  ismgmid  18762  mgmhmpropd  18804  mhmpropd  18904  smndex1gid  19017  smndex1gidOLD  19018  smndex1id  19027  grpsubid1  19152  mulgnnp1  19209  mulgsubcl  19215  mulgnn0z  19228  mulgnndir  19230  mulgneg2  19235  lagsubg  19327  ghmco  19367  symg2bas  19524  symgextfv  19549  pgpfi2  19737  efgsfo  19870  frgpupf  19904  frgpup1  19906  gsummptshft  20067  telgsumfzslem  20119  telgsums  20124  ablfac1eu  20206  pgpfac1lem2  20208  ablfaclem3  20220  dvdsrid  20512  dvdsrneg  20515  dvr1  20552  abv1  20995  lmodfopne  21088  lbsexg  21355  xrsds  21627  znf1o  21768  lindfmm  22044  lindsdom  22067  lindsenlbs  22068  gsummoncoe1  22537  matecl  22651  mavmul0g  22779  gsummatr01  22885  matunitlindflem2  22906  mp2pm2mplem4  23038  chfacfisf  23083  chfacfisfcpmat  23084  chfacfpmmulgsum2  23094  cpmadugsumlemF  23105  isclo  23316  resttopon  23390  restcld  23401  restcls  23410  iscn  23464  iscnp  23466  cnco  23495  cndis  23520  cnindis  23521  cmpsub  23629  hauscmplem  23635  cmpfii  23638  ptcnplem  23851  txtube  23870  txcmplem1  23871  xkoptsub  23884  qtoptop  23930  kqfval  23953  hmeoco  24002  fileln0  24080  trfil1  24116  trfil2  24117  trufil  24140  elfm3  24180  hausflf2  24228  isucn  24507  bl2in  24630  metss2lem  24741  metss2  24742  stdbdxmet  24745  metrest  24754  nmval2  24822  nmoix  24959  ioo2bl  25023  xrsxmet  25040  expcn  25104  elcncf  25121  icccvx  25182  cphsscph  25483  iscmet3  25525  causs  25530  metcld2  25539  metsscmetcld  25547  cncmet  25554  bcth3  25563  ovolgelb  25712  ovolfi  25726  shft2rab  25740  uniioombllem3  25817  dyadmax  25830  dyadmbl  25832  subopnmbl  25836  volcn  25838  mbfid  25867  mbfeqalem2  25874  mbfres  25876  cnmbf  25891  i1fmulc  25935  mbfi1fseqlem3  25949  mbfi1fseqlem4  25950  itg2seq  25974  itg2gt0  25992  itgss3  26047  dvexp  26185  plypow  26435  plyeq0lem  26440  coeidlem  26467  dgrlt  26496  dgrcolem2  26504  elqaalem2  26554  aacjcl  26563  aaliou3lem1  26578  aaliou3lem2  26579  pserdvlem2  26664  abelthlem8  26675  cosord  26769  sinord  26772  resinf1o  26774  relogexp  26834  logdivlt  26859  advlogexp  26893  logcxp  26907  cxpcl  26912  rpcxpcl  26914  cxpne0  26915  logbchbase  27009  logbgt0b  27031  birthdaylem2  27190  cxplim  27209  divsqrtsumo1  27221  zetacvg  27252  wilthlem1  27305  ftalem7  27316  basellem1  27318  issqf  27373  sqf11  27376  sgmf  27382  sgmnncl  27384  sqff1o  27419  dvdsflsumcom  27425  mpodvdsmulf1o  27431  dvdsmulf1o  27433  sgmppw  27434  chtublem  27448  chtub  27449  logexprlim  27462  bposlem3  27523  bposlem5  27525  bposlem6  27526  lgsdirnn0  27581  gausslemma2dlem1a  27602  gausslemma2dlem5a  27607  lgsquad2  27623  lgsquad3  27624  2sqreulem1  27683  2sqreunnlem1  27686  dchrisumlem1  27726  dchrisumlem2  27727  dchrisumlem3  27728  mulogsumlem  27768  noextenddif  27905  addsrid  28230  ltnegs  28311  lenegs  28312  om2noseqlt2  28566  elzn0s  28664  eln0zs  28666  peano5uzs  28670  bdayfinbndlem1  28733  brbtwn  29357  uspgrupgrushgr  29640  usgrumgruspgr  29643  cusgrfilem2  29917  finsumvtxdg2ssteplem2  30007  pthhashvtx  30195  cyclnumvtx  30268  crctcshwlkn0lem4  30282  crctcshwlkn0lem6  30284  crctcshwlkn0lem7  30285  crctcshwlkn0  30290  elwspths2spth  30439  rusgrnumwwlk  30447  clwlkclwwlklem2fv2  30467  erclwwlknref  30540  1to2vfriswmgr  30760  4cycl2v2nb  30770  frgr2wwlkeqm  30812  nvo00  31243  nmorepnf  31250  ubthlem1  31352  normpyc  31628  occon3  31779  pjpreeq  31880  idcnop  32463  riesz3i  32544  cnlnssadj  32562  rnbra  32589  strlem3a  32734  cvcon3  32766  ssdmd1  32795  ssdmd2  32796  relfi  33077  fcobijfs2  33195  fzsplit3  33266  prmsimpcyc  33670  esumcst  34575  dmvlsiga  34641  ballotlemimin  35019  bnj545  35406  bnj929  35447  bnj953  35450  fineqvnttrclselem1  35649  derangsn  35751  iscvm  35840  cvmsval  35847  cvmliftlem7  35872  cvmlift2lem12  35895  mclsssvlem  36143  supfz  36310  faclimlem3  36326  opnrebl2  36942  nn0prpwlem  36943  tailval  36994  nndivlub  37079  ctbssinf  38162  finixpnum  38361  ltflcei  38364  poimirlem4  38375  poimirlem14  38385  poimirlem15  38386  poimirlem19  38390  poimirlem20  38391  poimirlem22  38393  poimirlem24  38395  poimirlem28  38399  poimirlem30  38401  poimirlem31  38402  mblfinlem2  38409  mblfinlem3  38410  mblfinlem4  38411  ftc1anclem1  38444  ftc1anclem4  38447  ftc1anclem5  38448  ftc1anclem7  38450  ftc1anclem8  38451  ftc1anc  38452  caushft  38513  ismtyval  38552  heiborlem7  38569  heiborlem10  38572  heibor  38573  lcmineqlem8  42904  deg1gprod  43008  oexpreposd  43199  elrfirn  43542  ismrc  43548  nacsfix  43559  mzpcompact2lem  43598  eldiophb  43604  ellz1  43614  rexrabdioph  43637  congrep  43816  jm2.26a  43843  rngunsnply  44012  mendring  44031  iocmbl  44056  oeord2lim  44152  cantnfresb  44167  omabs2  44175  ofoafg  44197  dfno2  44270  rp-isfinite5  44359  enrelmap  44839  expgrowthi  45159  hashnnltb  45848  cnfex  45864  xlimclim2lem  46669  climxlim2  46676  icccncfext  46717  itgsinexp  46785  iblspltprt  46803  itgspltprt  46809  fourierdlem50  46986  fourierswlem  47060  etransclem35  47099  zm1nn  48192  subsubelfzo0  48217  ceilbi  48227  addmodne  48240  m1modmmod  48254  modlt0b  48259  iccpartres  48320  iccelpart  48335  iccpartiun  48336  iccpartnel  48340  nprmmul1  48429  goldbachthlem1  48450  goldbachth  48452  odz2prm2pw  48468  2pwp1prm  48494  evenltle  48635  fpprwpprb  48658  sbgoldbaltlem2  48698  bgoldbachlt  48731  isubgredg  48784  gricushgr  48835  uhgrimisgrgriclem  48848  gpgvtx0  48971  gpg5nbgrvtx13starlem2  48990  upgrwlkupwlk  49058  2zrngamgm  49162  lincresunit3  49413  lincreslvec3  49414  isldepslvec2  49417  blengt1fldiv2p1  49525  dignn0flhalf  49550  nn0sumshdiglemA  49551  rrx2pnedifcoorneor  49648  precofval2  50297  aacllem  50774