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  5542  ordintdif  6362  funco  6526  resdif  6789  fvcofneq  7031  fnprb  7148  fntpb  7149  fvf1pr  7248  isotr  7277  weisoeq  7296  brrpssg  7665  findsg  7837  coexg  7869  resf1extb  7874  xpexgALT  7923  fnsuppres  8131  oaass  8486  oeword  8515  oeworde  8518  mapsnd  8820  ixpssmapg  8862  enrefnn  8979  pw2f1olem  9005  domsdomtr  9036  xpen  9064  mapen  9065  mapdom1  9066  phplem2  9129  mapfienlem1  9314  elfir  9324  wdomen2  9488  carden2b  9882  harcard  9893  isinffi  9907  acnlem  9961  acndom  9964  alephdom  9994  fin23lem21  10252  fin23lem39  10263  isf32lem5  10270  fin1a2lem12  10324  axdc3lem2  10364  ttukeylem1  10422  pwcfsdom  10496  canthp1  10567  nqereu  10842  addpqf  10857  axmulf  11059  axmulass  11070  axdistr  11071  ltaddnegr  11351  negeu  11371  fimaxre3  12089  nnsub  12190  nn0sub  12452  ltsubnn0  12453  elz2  12507  uzaddcl  12823  qaddcl  12884  xltneg  13137  xleneg  13138  supxrbnd1  13241  infxrgelb  13256  iccneg  13393  uzsubsubfz  13467  fzsplit2  13470  fzadd2  13480  fzss1  13484  uzsplit  13517  fzdif1  13526  fz0fzdiffz0  13558  difelfzle  13562  difelfznle  13563  fvffz0  13567  preduz  13571  predfz  13574  fzonlt0  13603  fzouzsplit  13615  fzo0addelr  13640  eluzgtdifelfzo  13648  elfzodifsumelfzo  13652  ssfzo12  13680  elfznelfzob  13694  fllt  13728  flflp1  13729  uzsup  13785  negmod  13841  modifeq2int  13858  modfzo0difsn  13868  modsumfzodifsn  13869  om2uzlt2i  13876  nn0ennn  13904  suppssfz  13919  seqfveq2  13949  sermono  13959  seqf1o  13968  ser1const  13983  rpexpmord  14093  mulsubdivbinom2  14187  faclbnd  14215  bcval4  14232  bcpasc  14246  hashkf  14257  hashunx  14311  fz1isolem  14386  ishashinf  14388  seqcoll  14389  ccatval1  14502  ccatval21sw  14510  ccatrn  14514  ccatalpha  14518  swrdnd0  14582  swrd0  14583  swrdfv2  14586  swrdspsleq  14590  addlenpfx  14615  ccatpfx  14625  swrdswrd  14629  pfxccatin12lem2  14655  pfxccat3  14658  swrdccat  14659  revccat  14690  repswswrd  14708  cshwmodn  14719  cshwidxmod  14727  repswcshw  14736  2cshwid  14738  2cshwcom  14740  2cshwcshw  14750  cshwcshid  14752  cshwcsh2id  14753  s1co  14758  cshco  14761  trclub  14923  shftfval  14995  seqshft  15010  crim  15040  caubnd  15284  limsuplt  15404  isercolllem2  15591  fsumcvg  15637  fsumcvg2  15652  fsumshftm  15706  fsumo1  15737  isumshft  15764  harmonic  15784  cvgrat  15808  mertenslem1  15809  zprod  15862  fprodmodd  15922  bpolylem  15973  bpolysum  15978  bpolydiflem  15979  fsumkthpow  15981  rpnnen2lem12  16152  dvdsval3  16185  negdvdsb  16201  dvdsnegb  16202  dvdsmul1  16206  dvdsabseq  16242  dvdsssfz1  16247  odd2np1  16270  divalglem8  16329  ndvdsadd  16339  dfgcd2  16475  dvdssqim  16483  nn0seqcvgd  16499  seq1st  16500  algcvgblem  16506  lcmf  16562  lcmfunsnlem2  16569  cncongr2  16597  prmdvdsfz  16634  isprm7  16637  prmndvdsfaclt  16654  powm2modprm  16733  modprm0  16735  modprmn0modprm0  16737  pythagtriplem1  16746  pythagtriplem4  16749  pythagtriplem8  16753  pythagtriplem9  16754  pythagtriplem12  16756  pythagtriplem14  16758  pythagtriplem16  16760  pcexp  16789  pc2dvds  16809  pcz  16811  fldivp1  16827  pcfac  16829  oddprmdvds  16833  pockthg  16836  infpnlem1  16840  prmreclem1  16846  prmreclem2  16847  1arith  16857  4sqlem11  16885  vdwlem2  16912  vdwlem8  16918  vdwnnlem2  16926  prmgaplem7  16987  prmgaplem8  16988  cshwshashlem2  17026  cshwshashlem3  17027  pwsval  17408  isacs1i  17581  funcsetcestrclem9  18087  ismgmid  18557  mgmhmpropd  18590  mhmpropd  18684  smndex1gid  18795  smndex1id  18803  grpsubid1  18922  mulgnnp1  18979  mulgsubcl  18985  mulgnn0z  18998  mulgnndir  19000  mulgneg2  19005  lagsubg  19092  ghmco  19133  symg2bas  19290  symgextfv  19315  pgpfi2  19503  efgsfo  19636  frgpupf  19670  frgpup1  19672  gsummptshft  19833  telgsumfzslem  19885  telgsums  19890  ablfac1eu  19972  pgpfac1lem2  19974  ablfaclem3  19986  dvdsrid  20270  dvdsrneg  20273  dvr1  20310  abv1  20728  lmodfopne  20821  lbsexg  21089  xrsds  21334  znf1o  21476  lindfmm  21752  gsummoncoe1  22211  matecl  22328  mavmul0g  22456  gsummatr01  22562  mp2pm2mplem4  22712  chfacfisf  22757  chfacfisfcpmat  22758  chfacfpmmulgsum2  22768  cpmadugsumlemF  22779  isclo  22990  resttopon  23064  restcld  23075  restcls  23084  iscn  23138  iscnp  23140  cnco  23169  cndis  23194  cnindis  23195  cmpsub  23303  hauscmplem  23309  cmpfii  23312  ptcnplem  23524  txtube  23543  txcmplem1  23544  xkoptsub  23557  qtoptop  23603  kqfval  23626  hmeoco  23675  fileln0  23753  trfil1  23789  trfil2  23790  trufil  23813  elfm3  23853  hausflf2  23901  isucn  24181  bl2in  24304  metss2lem  24415  metss2  24416  stdbdxmet  24419  metrest  24428  nmval2  24496  nmoix  24633  ioo2bl  24697  xrsxmet  24714  expcn  24779  expcnOLD  24781  elcncf  24798  icccvx  24864  cphsscph  25167  iscmet3  25209  causs  25214  metcld2  25223  metsscmetcld  25231  cncmet  25238  bcth3  25247  ovolgelb  25397  ovolfi  25411  shft2rab  25425  uniioombllem3  25502  dyadmax  25515  dyadmbl  25517  subopnmbl  25521  volcn  25523  mbfid  25552  mbfeqalem2  25559  mbfres  25561  cnmbf  25576  i1fmulc  25620  mbfi1fseqlem3  25634  mbfi1fseqlem4  25635  itg2seq  25659  itg2gt0  25677  itgss3  25732  dvexp  25873  plypow  26126  plyeq0lem  26131  coeidlem  26158  dgrlt  26188  dgrcolem2  26196  elqaalem2  26244  aacjcl  26251  aaliou3lem1  26266  aaliou3lem2  26267  pserdvlem2  26354  abelthlem8  26365  cosord  26456  sinord  26459  resinf1o  26461  relogexp  26521  logdivlt  26546  advlogexp  26580  logcxp  26594  cxpcl  26599  rpcxpcl  26601  cxpne0  26602  logbchbase  26697  logbgt0b  26719  birthdaylem2  26878  cxplim  26898  divsqrtsumo1  26910  zetacvg  26941  wilthlem1  26994  ftalem7  27005  basellem1  27007  issqf  27062  sqf11  27065  sgmf  27071  sgmnncl  27073  sqff1o  27108  dvdsflsumcom  27114  mpodvdsmulf1o  27120  dvdsmulf1o  27122  sgmppw  27124  chtublem  27138  chtub  27139  logexprlim  27152  bposlem3  27213  bposlem5  27215  bposlem6  27216  lgsdirnn0  27271  gausslemma2dlem1a  27292  gausslemma2dlem5a  27297  lgsquad2  27313  lgsquad3  27314  2sqreulem1  27373  2sqreunnlem1  27376  dchrisumlem1  27416  dchrisumlem2  27417  dchrisumlem3  27418  mulogsumlem  27458  noextenddif  27596  addsrid  27894  sltneg  27974  sleneg  27975  om2noseqlt2  28217  elzn0s  28309  eln0zs  28311  peano5uzs  28315  brbtwn  28862  uspgrupgrushgr  29142  usgrumgruspgr  29145  cusgrfilem2  29420  finsumvtxdg2ssteplem2  29510  cyclnumvtx  29763  crctcshwlkn0lem4  29776  crctcshwlkn0lem6  29778  crctcshwlkn0lem7  29779  crctcshwlkn0  29784  elwspths2spth  29930  rusgrnumwwlk  29938  clwlkclwwlklem2fv2  29958  erclwwlknref  30031  1to2vfriswmgr  30241  4cycl2v2nb  30251  frgr2wwlkeqm  30293  nvo00  30723  nmorepnf  30730  ubthlem1  30832  normpyc  31108  occon3  31259  pjpreeq  31360  idcnop  31943  riesz3i  32024  cnlnssadj  32042  rnbra  32069  strlem3a  32214  cvcon3  32246  ssdmd1  32275  ssdmd2  32276  relfi  32564  fzsplit3  32749  prmsimpcyc  33180  esumcst  34029  dmvlsiga  34095  ballotlemimin  34473  bnj545  34861  bnj929  34902  bnj953  34905  pthhashvtx  35100  derangsn  35142  iscvm  35231  cvmsval  35238  cvmliftlem7  35263  cvmlift2lem12  35286  mclsssvlem  35534  supfz  35701  faclimlem3  35717  opnrebl2  36294  nn0prpwlem  36295  tailval  36346  nndivlub  36431  ctbssinf  37379  finixpnum  37584  ltflcei  37587  lindsdom  37593  lindsenlbs  37594  matunitlindflem2  37596  poimirlem4  37603  poimirlem14  37613  poimirlem15  37614  poimirlem19  37618  poimirlem20  37619  poimirlem22  37621  poimirlem24  37623  poimirlem28  37627  poimirlem30  37629  poimirlem31  37630  mblfinlem2  37637  mblfinlem3  37638  mblfinlem4  37639  ftc1anclem1  37672  ftc1anclem4  37675  ftc1anclem5  37676  ftc1anclem7  37678  ftc1anclem8  37679  ftc1anc  37680  caushft  37740  ismtyval  37779  heiborlem7  37796  heiborlem10  37799  heibor  37800  lcmineqlem8  42009  deg1gprod  42113  f1o2d2  42206  oexpreposd  42295  elrfirn  42668  ismrc  42674  nacsfix  42685  mzpcompact2lem  42724  eldiophb  42730  ellz1  42740  rexrabdioph  42767  congrep  42946  jm2.26a  42973  rngunsnply  43142  mendring  43161  iocmbl  43186  oeord2lim  43282  cantnfresb  43297  omabs2  43305  ofoafg  43327  dfno2  43401  rp-isfinite5  43490  enrelmap  43970  expgrowthi  44306  cnfex  45006  xlimclim2lem  45821  climxlim2  45828  icccncfext  45869  itgsinexp  45937  iblspltprt  45955  itgspltprt  45961  fourierdlem50  46138  fourierswlem  46212  etransclem35  46251  zm1nn  47287  subsubelfzo0  47311  ceilbi  47318  addmodne  47329  m1modmmod  47343  modlt0b  47348  iccpartres  47403  iccelpart  47418  iccpartiun  47419  iccpartnel  47423  goldbachthlem1  47530  goldbachth  47532  odz2prm2pw  47548  2pwp1prm  47574  evenltle  47702  fpprwpprb  47725  sbgoldbaltlem2  47765  bgoldbachlt  47798  isubgredg  47850  gricushgr  47901  uhgrimisgrgriclem  47914  gpgvtx0  48028  gpg5nbgrvtx13starlem2  48047  upgrwlkupwlk  48112  2zrngamgm  48217  lincresunit3  48454  lincreslvec3  48455  isldepslvec2  48458  blengt1fldiv2p1  48566  dignn0flhalf  48591  nn0sumshdiglemA  48592  rrx2pnedifcoorneor  48689  precofval2  49342  aacllem  49774