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 ⊢ ((𝜏 ∧ 𝜑) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  swopo  5571  ordintdif  6401  funco  6565  resdif  6832  fvcofneq  7078  fnprb  7196  fntpb  7197  fvf1pr  7295  isotr  7324  weisoeq  7343  brrpssg  7712  findsg  7882  coexg  7914  resf1extb  7919  xpexgALT  7966  mpof1o2d  8109  fnsuppres  8175  oaass  8534  oeword  8564  oeworde  8567  mapsnd  8872  ixpssmapg  8914  enrefnn  9031  pw2f1olem  9057  domsdomtr  9088  xpen  9116  mapen  9117  mapdom1  9118  phplem2  9177  mapfienlem1  9353  elfir  9363  wdomen2  9527  carden2b  9941  harcard  9952  isinffi  9966  acnlem  10020  acndom  10023  alephdom  10053  fin23lem21  10311  fin23lem39  10322  isf32lem5  10329  fin1a2lem12  10383  axdc3lem2  10423  ttukeylem1  10481  pwcfsdom  10556  canthp1  10627  nqereu  10902  addpqf  10917  axmulf  11119  axmulass  11130  axdistr  11131  ltaddnegr  11415  negeu  11435  fimaxre3  12152  nnsub  12271  nn0sub  12545  ltsubnn0  12546  elz2  12600  uzaddcl  12919  qaddcl  12980  xltneg  13234  xleneg  13235  supxrbnd1  13338  infxrgelb  13353  iccneg  13490  uzsubsubfz  13565  fzsplit2  13568  fzadd2  13578  fzss1  13582  uzsplit  13615  fzdif1  13624  fz0fzdiffz0  13656  difelfzle  13660  difelfznle  13661  fvffz0  13665  preduz  13669  predfz  13672  fzonlt0  13702  fzouzsplit  13714  fzo0addelr  13739  eluzgtdifelfzo  13747  elfzodifsumelfzo  13751  ssfzo12  13779  elfznelfzob  13794  fllt  13830  flflp1  13831  uzsup  13887  negmod  13943  modifeq2int  13960  modfzo0difsn  13970  modsumfzodifsn  13971  om2uzlt2i  13978  nn0ennn  14006  suppssfz  14021  seqfveq2  14051  sermono  14061  seqf1o  14070  ser1const  14085  rpexpmord  14195  mulsubdivbinom2  14289  faclbnd  14317  bcval4  14334  bcpasc  14348  hashkf  14359  hashunx  14413  fz1isolem  14488  ishashinf  14490  seqcoll  14491  ccatval1  14604  ccatval21sw  14613  ccatrn  14617  ccatalpha  14621  swrdnd0  14685  swrd0  14686  swrdfv2  14689  swrdspsleq  14693  addlenpfx  14718  ccatpfx  14728  swrdswrd  14732  pfxccatin12lem2  14758  pfxccat3  14761  swrdccat  14762  revccat  14793  repswswrd  14811  cshwmodn  14822  cshwidxmod  14830  repswcshw  14839  2cshwid  14841  2cshwcom  14843  2cshwcshw  14852  cshwcshid  14854  cshwcsh2id  14855  s1co  14860  cshco  14863  trclub  15025  shftfval  15097  seqshft  15112  crim  15156  caubnd  15400  limsuplt  15520  isercolllem2  15707  fsumcvg  15753  fsumcvg2  15768  fsumshftm  15822  fsumo1  15854  isumshft  15883  harmonic  15903  cvgrat  15927  mertenslem1  15928  zprod  15981  fprodmodd  16041  bpolylem  16092  bpolysum  16097  bpolydiflem  16098  fsumkthpow  16100  rpnnen2lem12  16271  dvdsval3  16304  negdvdsb  16320  dvdsnegb  16321  dvdsmul1  16325  dvdsabseq  16361  dvdsssfz1  16366  odd2np1  16389  divalglem8  16448  ndvdsadd  16458  dfgcd2  16594  dvdssqim  16602  nn0seqcvgd  16618  seq1st  16619  algcvgblem  16625  lcmf  16681  lcmfunsnlem2  16688  cncongr2  16716  prmdvdsfz  16754  isprm7  16757  prmndvdsfaclt  16774  powm2modprm  16853  modprm0  16855  modprmn0modprm0  16857  pythagtriplem1  16866  pythagtriplem4  16869  pythagtriplem8  16873  pythagtriplem9  16874  pythagtriplem12  16876  pythagtriplem14  16878  pythagtriplem16  16880  pcexp  16909  pc2dvds  16929  pcz  16931  fldivp1  16947  pcfac  16949  oddprmdvds  16953  pockthg  16956  infpnlem1  16960  prmreclem1  16966  prmreclem2  16967  1arith  16977  4sqlem11  17005  vdwlem2  17032  vdwlem8  17038  vdwnnlem2  17046  prmgaplem7  17107  prmgaplem8  17108  cshwshashlem2  17146  cshwshashlem3  17147  pwsval  17529  isacs1i  17703  funcsetcestrclem9  18209  ismgmid  18713  mgmhmpropd  18746  mhmpropd  18840  smndex1gid  18953  smndex1gidOLD  18954  smndex1id  18963  grpsubid1  19082  mulgnnp1  19139  mulgsubcl  19145  mulgnn0z  19158  mulgnndir  19160  mulgneg2  19165  lagsubg  19257  ghmco  19297  symg2bas  19454  symgextfv  19479  pgpfi2  19667  efgsfo  19800  frgpupf  19834  frgpup1  19836  gsummptshft  19997  telgsumfzslem  20049  telgsums  20054  ablfac1eu  20136  pgpfac1lem2  20138  ablfaclem3  20150  dvdsrid  20440  dvdsrneg  20443  dvr1  20480  abv1  20897  lmodfopne  20990  lbsexg  21257  xrsds  21520  znf1o  21661  lindfmm  21937  gsummoncoe1  22429  matecl  22543  mavmul0g  22671  gsummatr01  22777  mp2pm2mplem4  22927  chfacfisf  22972  chfacfisfcpmat  22973  chfacfpmmulgsum2  22983  cpmadugsumlemF  22994  isclo  23205  resttopon  23279  restcld  23290  restcls  23299  iscn  23353  iscnp  23355  cnco  23384  cndis  23409  cnindis  23410  cmpsub  23518  hauscmplem  23524  cmpfii  23527  ptcnplem  23739  txtube  23758  txcmplem1  23759  xkoptsub  23772  qtoptop  23818  kqfval  23841  hmeoco  23890  fileln0  23968  trfil1  24004  trfil2  24005  trufil  24028  elfm3  24068  hausflf2  24116  isucn  24395  bl2in  24518  metss2lem  24629  metss2  24630  stdbdxmet  24633  metrest  24642  nmval2  24710  nmoix  24847  ioo2bl  24911  xrsxmet  24928  expcn  24992  elcncf  25009  icccvx  25070  cphsscph  25371  iscmet3  25413  causs  25418  metcld2  25427  metsscmetcld  25435  cncmet  25442  bcth3  25451  ovolgelb  25600  ovolfi  25614  shft2rab  25628  uniioombllem3  25705  dyadmax  25718  dyadmbl  25720  subopnmbl  25724  volcn  25726  mbfid  25755  mbfeqalem2  25762  mbfres  25764  cnmbf  25779  i1fmulc  25823  mbfi1fseqlem3  25837  mbfi1fseqlem4  25838  itg2seq  25862  itg2gt0  25880  itgss3  25935  dvexp  26073  plypow  26323  plyeq0lem  26328  coeidlem  26355  dgrlt  26384  dgrcolem2  26392  elqaalem2  26442  aacjcl  26449  aaliou3lem1  26464  aaliou3lem2  26465  pserdvlem2  26549  abelthlem8  26560  cosord  26654  sinord  26657  resinf1o  26659  relogexp  26719  logdivlt  26744  advlogexp  26778  logcxp  26792  cxpcl  26797  rpcxpcl  26799  cxpne0  26800  logbchbase  26894  logbgt0b  26916  birthdaylem2  27075  cxplim  27094  divsqrtsumo1  27106  zetacvg  27137  wilthlem1  27190  ftalem7  27201  basellem1  27203  issqf  27258  sqf11  27261  sgmf  27267  sgmnncl  27269  sqff1o  27304  dvdsflsumcom  27310  mpodvdsmulf1o  27316  dvdsmulf1o  27318  sgmppw  27319  chtublem  27333  chtub  27334  logexprlim  27347  bposlem3  27408  bposlem5  27410  bposlem6  27411  lgsdirnn0  27466  gausslemma2dlem1a  27487  gausslemma2dlem5a  27492  lgsquad2  27508  lgsquad3  27509  2sqreulem1  27568  2sqreunnlem1  27571  dchrisumlem1  27611  dchrisumlem2  27612  dchrisumlem3  27613  mulogsumlem  27653  noextenddif  27790  addsrid  28115  ltnegs  28196  lenegs  28197  om2noseqlt2  28451  elzn0s  28549  eln0zs  28551  peano5uzs  28555  bdayfinbndlem1  28618  brbtwn  29158  uspgrupgrushgr  29438  usgrumgruspgr  29441  cusgrfilem2  29715  finsumvtxdg2ssteplem2  29805  cyclnumvtx  30058  crctcshwlkn0lem4  30071  crctcshwlkn0lem6  30073  crctcshwlkn0lem7  30074  crctcshwlkn0  30079  elwspths2spth  30228  rusgrnumwwlk  30236  clwlkclwwlklem2fv2  30256  erclwwlknref  30329  1to2vfriswmgr  30539  4cycl2v2nb  30549  frgr2wwlkeqm  30591  nvo00  31022  nmorepnf  31029  ubthlem1  31131  normpyc  31407  occon3  31558  pjpreeq  31659  idcnop  32242  riesz3i  32323  cnlnssadj  32341  rnbra  32368  strlem3a  32513  cvcon3  32545  ssdmd1  32574  ssdmd2  32575  relfi  32857  fcobijfs2  32979  fzsplit3  33050  prmsimpcyc  33461  esumcst  34370  dmvlsiga  34436  ballotlemimin  34813  bnj545  35200  bnj929  35241  bnj953  35244  fineqvnttrclselem1  35429  pthhashvtx  35491  derangsn  35533  iscvm  35622  cvmsval  35629  cvmliftlem7  35654  cvmlift2lem12  35677  mclsssvlem  35925  supfz  36092  faclimlem3  36108  opnrebl2  36694  nn0prpwlem  36695  tailval  36746  nndivlub  36831  ctbssinf  37912  finixpnum  38116  ltflcei  38119  lindsdom  38125  lindsenlbs  38126  matunitlindflem2  38128  poimirlem4  38135  poimirlem14  38145  poimirlem15  38146  poimirlem19  38150  poimirlem20  38151  poimirlem22  38153  poimirlem24  38155  poimirlem28  38159  poimirlem30  38161  poimirlem31  38162  mblfinlem2  38169  mblfinlem3  38170  mblfinlem4  38171  ftc1anclem1  38204  ftc1anclem4  38207  ftc1anclem5  38208  ftc1anclem7  38210  ftc1anclem8  38211  ftc1anc  38212  caushft  38272  ismtyval  38311  heiborlem7  38328  heiborlem10  38331  heibor  38332  lcmineqlem8  42665  deg1gprod  42769  oexpreposd  42943  elrfirn  43288  ismrc  43294  nacsfix  43305  mzpcompact2lem  43344  eldiophb  43350  ellz1  43360  rexrabdioph  43383  congrep  43562  jm2.26a  43589  rngunsnply  43758  mendring  43777  iocmbl  43802  oeord2lim  43898  cantnfresb  43913  omabs2  43921  ofoafg  43943  dfno2  44016  rp-isfinite5  44105  enrelmap  44585  expgrowthi  44907  cnfex  45606  xlimclim2lem  46411  climxlim2  46418  icccncfext  46459  itgsinexp  46527  iblspltprt  46545  itgspltprt  46551  fourierdlem50  46728  fourierswlem  46802  etransclem35  46841  zm1nn  47894  subsubelfzo0  47919  ceilbi  47929  addmodne  47942  m1modmmod  47956  modlt0b  47961  iccpartres  48022  iccelpart  48037  iccpartiun  48038  iccpartnel  48042  nprmmul1  48131  goldbachthlem1  48152  goldbachth  48154  odz2prm2pw  48170  2pwp1prm  48196  evenltle  48337  fpprwpprb  48360  sbgoldbaltlem2  48400  bgoldbachlt  48433  isubgredg  48486  gricushgr  48537  uhgrimisgrgriclem  48550  gpgvtx0  48673  gpg5nbgrvtx13starlem2  48692  upgrwlkupwlk  48760  2zrngamgm  48865  lincresunit3  49112  lincreslvec3  49113  isldepslvec2  49116  blengt1fldiv2p1  49224  dignn0flhalf  49249  nn0sumshdiglemA  49250  rrx2pnedifcoorneor  49347  precofval2  49998  aacllem  50430