Theorem syl2anr 608

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 607	. 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜃)
5	4	ancoms 463	1 ⊢ ((𝜏 ∧ 𝜑) → 𝜃)

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

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 401

This theorem is used by:  swopo  5579  ordintdif  6412  funco  6576  resdif  6842  fvcofneq  7088  fnprb  7206  fntpb  7207  fvf1pr  7305  isotr  7334  weisoeq  7355  brrpssg  7724  findsg  7892  coexg  7924  resf1extb  7929  xpexgALT  7976  mpof1o2d  8119  fnsuppres  8185  oaass  8544  oeword  8574  oeworde  8577  mapsnd  8882  ixpssmapg  8924  enrefnn  9041  pw2f1olem  9067  domsdomtr  9098  xpen  9126  mapen  9127  mapdom1  9128  phplem2  9187  mapfienlem1  9363  elfir  9373  wdomen2  9537  carden2b  9960  harcard  9971  isinffi  9985  acnlem  10039  acndom  10042  alephdom  10072  fin23lem21  10329  fin23lem39  10340  isf32lem5  10347  fin1a2lem12  10401  axdc3lem2  10441  ttukeylem1  10499  pwcfsdom  10574  canthp1  10645  nqereu  10920  addpqf  10935  axmulf  11137  axmulass  11148  axdistr  11149  ltaddnegr  11433  negeu  11453  fimaxre3  12167  nnsub  12286  nn0sub  12560  ltsubnn0  12561  elz2  12615  uzaddcl  12934  qaddcl  12995  xltneg  13249  xleneg  13250  supxrbnd1  13353  infxrgelb  13368  iccneg  13505  uzsubsubfz  13581  fzsplit2  13584  fzadd2  13594  fzss1  13598  uzsplit  13631  fzdif1  13640  fz0fzdiffz0  13672  difelfzle  13676  difelfznle  13677  fvffz0  13681  preduz  13685  predfz  13688  fzonlt0  13718  fzouzsplit  13730  fzo0addelr  13755  eluzgtdifelfzo  13763  elfzodifsumelfzo  13767  ssfzo12  13795  elfznelfzob  13810  fllt  13846  flflp1  13847  uzsup  13903  negmod  13959  modifeq2int  13976  modfzo0difsn  13986  modsumfzodifsn  13987  om2uzlt2i  13994  nn0ennn  14022  suppssfz  14037  seqfveq2  14067  sermono  14077  seqf1o  14086  ser1const  14101  rpexpmord  14211  mulsubdivbinom2  14305  faclbnd  14333  bcval4  14350  bcpasc  14364  hashkf  14375  hashunx  14429  fz1isolem  14505  ishashinf  14507  seqcoll  14508  ccatval1  14621  ccatval21sw  14630  ccatrn  14634  ccatalpha  14638  swrdnd0  14702  swrd0  14703  swrdfv2  14706  swrdspsleq  14710  addlenpfx  14735  ccatpfx  14745  swrdswrd  14749  pfxccatin12lem2  14775  pfxccat3  14778  swrdccat  14779  revccat  14810  repswswrd  14828  cshwmodn  14839  cshwidxmod  14847  repswcshw  14856  2cshwid  14858  2cshwcom  14860  2cshwcshw  14869  cshwcshid  14871  cshwcsh2id  14872  s1co  14877  cshco  14880  trclub  15042  shftfval  15114  seqshft  15129  crim  15173  caubnd  15417  limsuplt  15537  isercolllem2  15724  fsumcvg  15770  fsumcvg2  15785  fsumshftm  15839  fsumo1  15871  isumshft  15900  harmonic  15920  cvgrat  15944  mertenslem1  15945  zprod  15998  fprodmodd  16058  bpolylem  16108  bpolysum  16113  bpolydiflem  16114  fsumkthpow  16116  rpnnen2lem12  16287  dvdsval3  16320  negdvdsb  16336  dvdsnegb  16337  dvdsmul1  16341  dvdsabseq  16377  dvdsssfz1  16382  odd2np1  16405  divalglem8  16464  ndvdsadd  16474  dfgcd2  16610  dvdssqim  16618  nn0seqcvgd  16634  seq1st  16635  algcvgblem  16641  lcmf  16697  lcmfunsnlem2  16704  cncongr2  16732  prmdvdsfz  16770  isprm7  16773  prmndvdsfaclt  16790  powm2modprm  16869  modprm0  16871  modprmn0modprm0  16873  pythagtriplem1  16882  pythagtriplem4  16885  pythagtriplem8  16889  pythagtriplem9  16890  pythagtriplem12  16892  pythagtriplem14  16894  pythagtriplem16  16896  pcexp  16925  pc2dvds  16945  pcz  16947  fldivp1  16963  pcfac  16965  oddprmdvds  16969  pockthg  16972  infpnlem1  16976  prmreclem1  16982  prmreclem2  16983  1arith  16993  4sqlem11  17021  vdwlem2  17048  vdwlem8  17054  vdwnnlem2  17062  prmgaplem7  17123  prmgaplem8  17124  cshwshashlem2  17162  cshwshashlem3  17163  pwsval  17545  isacs1i  17719  funcsetcestrclem9  18225  ismgmid  18729  mgmhmpropd  18762  mhmpropd  18856  smndex1gid  18969  smndex1gidOLD  18970  smndex1id  18979  grpsubid1  19097  mulgnnp1  19154  mulgsubcl  19160  mulgnn0z  19173  mulgnndir  19175  mulgneg2  19180  lagsubg  19272  ghmco  19312  symg2bas  19469  symgextfv  19494  pgpfi2  19682  efgsfo  19815  frgpupf  19849  frgpup1  19851  gsummptshft  20012  telgsumfzslem  20064  telgsums  20069  ablfac1eu  20151  pgpfac1lem2  20153  ablfaclem3  20165  dvdsrid  20456  dvdsrneg  20459  dvr1  20496  abv1  20939  lmodfopne  21032  lbsexg  21299  xrsds  21571  znf1o  21712  lindfmm  21988  gsummoncoe1  22479  matecl  22593  mavmul0g  22721  gsummatr01  22827  mp2pm2mplem4  22977  chfacfisf  23022  chfacfisfcpmat  23023  chfacfpmmulgsum2  23033  cpmadugsumlemF  23044  isclo  23255  resttopon  23329  restcld  23340  restcls  23349  iscn  23403  iscnp  23405  cnco  23434  cndis  23459  cnindis  23460  cmpsub  23568  hauscmplem  23574  cmpfii  23577  ptcnplem  23789  txtube  23808  txcmplem1  23809  xkoptsub  23822  qtoptop  23868  kqfval  23891  hmeoco  23940  fileln0  24018  trfil1  24054  trfil2  24055  trufil  24078  elfm3  24118  hausflf2  24166  isucn  24445  bl2in  24568  metss2lem  24679  metss2  24680  stdbdxmet  24683  metrest  24692  nmval2  24760  nmoix  24897  ioo2bl  24961  xrsxmet  24978  expcn  25042  elcncf  25059  icccvx  25120  cphsscph  25421  iscmet3  25463  causs  25468  metcld2  25477  metsscmetcld  25485  cncmet  25492  bcth3  25501  ovolgelb  25650  ovolfi  25664  shft2rab  25678  uniioombllem3  25755  dyadmax  25768  dyadmbl  25770  subopnmbl  25774  volcn  25776  mbfid  25805  mbfeqalem2  25812  mbfres  25814  cnmbf  25829  i1fmulc  25873  mbfi1fseqlem3  25887  mbfi1fseqlem4  25888  itg2seq  25912  itg2gt0  25930  itgss3  25985  dvexp  26123  plypow  26373  plyeq0lem  26378  coeidlem  26405  dgrlt  26434  dgrcolem2  26442  elqaalem2  26492  aacjcl  26501  aaliou3lem1  26516  aaliou3lem2  26517  pserdvlem2  26602  abelthlem8  26613  cosord  26707  sinord  26710  resinf1o  26712  relogexp  26772  logdivlt  26797  advlogexp  26831  logcxp  26845  cxpcl  26850  rpcxpcl  26852  cxpne0  26853  logbchbase  26947  logbgt0b  26969  birthdaylem2  27128  cxplim  27147  divsqrtsumo1  27159  zetacvg  27190  wilthlem1  27243  ftalem7  27254  basellem1  27256  issqf  27311  sqf11  27314  sgmf  27320  sgmnncl  27322  sqff1o  27357  dvdsflsumcom  27363  mpodvdsmulf1o  27369  dvdsmulf1o  27371  sgmppw  27372  chtublem  27386  chtub  27387  logexprlim  27400  bposlem3  27461  bposlem5  27463  bposlem6  27464  lgsdirnn0  27519  gausslemma2dlem1a  27540  gausslemma2dlem5a  27545  lgsquad2  27561  lgsquad3  27562  2sqreulem1  27621  2sqreunnlem1  27624  dchrisumlem1  27664  dchrisumlem2  27665  dchrisumlem3  27666  mulogsumlem  27706  noextenddif  27843  addsrid  28168  ltnegs  28249  lenegs  28250  om2noseqlt2  28504  elzn0s  28602  eln0zs  28604  peano5uzs  28608  bdayfinbndlem1  28671  brbtwn  29260  uspgrupgrushgr  29540  usgrumgruspgr  29543  cusgrfilem2  29817  finsumvtxdg2ssteplem2  29907  cyclnumvtx  30160  crctcshwlkn0lem4  30173  crctcshwlkn0lem6  30175  crctcshwlkn0lem7  30176  crctcshwlkn0  30181  elwspths2spth  30330  rusgrnumwwlk  30338  clwlkclwwlklem2fv2  30358  erclwwlknref  30431  1to2vfriswmgr  30641  4cycl2v2nb  30651  frgr2wwlkeqm  30693  nvo00  31124  nmorepnf  31131  ubthlem1  31233  normpyc  31509  occon3  31660  pjpreeq  31761  idcnop  32344  riesz3i  32425  cnlnssadj  32443  rnbra  32470  strlem3a  32615  cvcon3  32647  ssdmd1  32676  ssdmd2  32677  relfi  32958  fcobijfs2  33078  fzsplit3  33149  prmsimpcyc  33557  esumcst  34462  dmvlsiga  34528  ballotlemimin  34905  bnj545  35292  bnj929  35333  bnj953  35336  fineqvnttrclselem1  35542  pthhashvtx  35628  derangsn  35670  iscvm  35759  cvmsval  35766  cvmliftlem7  35791  cvmlift2lem12  35814  mclsssvlem  36062  supfz  36229  faclimlem3  36245  opnrebl2  36860  nn0prpwlem  36861  tailval  36912  nndivlub  36997  ctbssinf  38080  finixpnum  38284  ltflcei  38287  lindsdom  38293  lindsenlbs  38294  matunitlindflem2  38296  poimirlem4  38303  poimirlem14  38313  poimirlem15  38314  poimirlem19  38318  poimirlem20  38319  poimirlem22  38321  poimirlem24  38323  poimirlem28  38327  poimirlem30  38329  poimirlem31  38330  mblfinlem2  38337  mblfinlem3  38338  mblfinlem4  38339  ftc1anclem1  38372  ftc1anclem4  38375  ftc1anclem5  38376  ftc1anclem7  38378  ftc1anclem8  38379  ftc1anc  38380  caushft  38440  ismtyval  38479  heiborlem7  38496  heiborlem10  38499  heibor  38500  lcmineqlem8  42831  deg1gprod  42935  oexpreposd  43111  elrfirn  43454  ismrc  43460  nacsfix  43471  mzpcompact2lem  43510  eldiophb  43516  ellz1  43526  rexrabdioph  43549  congrep  43728  jm2.26a  43755  rngunsnply  43924  mendring  43943  iocmbl  43968  oeord2lim  44064  cantnfresb  44079  omabs2  44087  ofoafg  44109  dfno2  44182  rp-isfinite5  44271  enrelmap  44751  expgrowthi  45071  hashnnltb  45760  cnfex  45776  xlimclim2lem  46581  climxlim2  46588  icccncfext  46629  itgsinexp  46697  iblspltprt  46715  itgspltprt  46721  fourierdlem50  46898  fourierswlem  46972  etransclem35  47011  zm1nn  48067  subsubelfzo0  48092  ceilbi  48102  addmodne  48115  m1modmmod  48129  modlt0b  48134  iccpartres  48195  iccelpart  48210  iccpartiun  48211  iccpartnel  48215  nprmmul1  48304  goldbachthlem1  48325  goldbachth  48327  odz2prm2pw  48343  2pwp1prm  48369  evenltle  48510  fpprwpprb  48533  sbgoldbaltlem2  48573  bgoldbachlt  48606  isubgredg  48659  gricushgr  48710  uhgrimisgrgriclem  48723  gpgvtx0  48846  gpg5nbgrvtx13starlem2  48865  upgrwlkupwlk  48933  2zrngamgm  49038  lincresunit3  49289  lincreslvec3  49290  isldepslvec2  49293  blengt1fldiv2p1  49401  dignn0flhalf  49426  nn0sumshdiglemA  49427  rrx2pnedifcoorneor  49524  precofval2  50175  aacllem  50649