Theorem syl2anr 598

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  swopo  5600  ordintdif  6415  funco  6589  resdif  6855  fvcofneq  7095  fnprb  7210  fntpb  7211  isotr  7333  weisoeq  7352  brrpssg  7715  findsg  7890  coexg  7920  xpexgALT  7968  fnsuppres  8176  wfrlem10OLD  8318  oaass  8561  oeword  8590  oeworde  8593  mapsnd  8880  ixpssmapg  8922  enrefnn  9047  pw2f1olem  9076  domsdomtr  9112  xpen  9140  mapen  9141  mapdom1  9142  phplem2  9208  mapfienlem1  9400  elfir  9410  wdomen2  9572  carden2b  9962  harcard  9973  isinffi  9987  acnlem  10043  acndom  10046  alephdom  10076  fin23lem21  10334  fin23lem39  10345  isf32lem5  10352  fin1a2lem12  10406  axdc3lem2  10446  ttukeylem1  10504  pwcfsdom  10578  canthp1  10649  nqereu  10924  addpqf  10939  axmulf  11141  axmulass  11152  axdistr  11153  ltaddnegr  11430  negeu  11450  fimaxre3  12160  nnsub  12256  nn0sub  12522  ltsubnn0  12523  elz2  12576  uzaddcl  12888  qaddcl  12949  xltneg  13196  xleneg  13197  supxrbnd1  13300  infxrgelb  13314  iccneg  13449  uzsubsubfz  13523  fzsplit2  13526  fzadd2  13536  fzss1  13540  uzsplit  13573  fz0fzdiffz0  13610  difelfzle  13614  difelfznle  13615  fvffz0  13619  preduz  13623  predfz  13626  fzonlt0  13655  fzouzsplit  13667  fzo0addelr  13687  eluzgtdifelfzo  13694  elfzodifsumelfzo  13698  ssfzo12  13725  elfznelfzob  13738  fllt  13771  flflp1  13772  uzsup  13828  negmod  13881  modifeq2int  13898  modfzo0difsn  13908  modsumfzodifsn  13909  om2uzlt2i  13916  nn0ennn  13944  suppssfz  13959  seqfveq2  13990  sermono  14000  seqf1o  14009  ser1const  14024  rpexpmord  14133  mulsubdivbinom2  14222  faclbnd  14250  bcval4  14267  bcpasc  14281  hashkf  14292  hashunx  14346  hashfacenOLD  14414  fz1isolem  14422  ishashinf  14424  seqcoll  14425  ccatval1  14527  ccatval21sw  14535  ccatrn  14539  ccatalpha  14543  swrdnd0  14607  swrd0  14608  swrdfv2  14611  swrdspsleq  14615  addlenpfx  14641  ccatpfx  14651  swrdswrd  14655  pfxccatin12lem2  14681  pfxccat3  14684  swrdccat  14685  revccat  14716  repswswrd  14734  cshwmodn  14745  cshwidxmod  14753  repswcshw  14762  2cshwid  14764  2cshwcom  14766  2cshwcshw  14776  cshwcshid  14778  cshwcsh2id  14779  s1co  14784  cshco  14787  trclub  14945  shftfval  15017  seqshft  15032  crim  15062  caubnd  15305  limsuplt  15423  isercolllem2  15612  fsumcvg  15658  fsumcvg2  15673  fsumshftm  15727  fsumo1  15758  isumshft  15785  harmonic  15805  cvgrat  15829  mertenslem1  15830  zprod  15881  fprodmodd  15941  bpolylem  15992  bpolysum  15997  bpolydiflem  15998  fsumkthpow  16000  rpnnen2lem12  16168  dvdsval3  16201  negdvdsb  16216  dvdsnegb  16217  dvdsmul1  16221  dvdsabseq  16256  dvdsssfz1  16261  odd2np1  16284  divalglem8  16343  ndvdsadd  16353  dfgcd2  16488  dvdssqim  16496  nn0seqcvgd  16507  seq1st  16508  algcvgblem  16514  lcmf  16570  lcmfunsnlem2  16577  cncongr2  16605  prmdvdsfz  16642  isprm7  16645  prmndvdsfaclt  16662  powm2modprm  16736  modprm0  16738  modprmn0modprm0  16740  pythagtriplem1  16749  pythagtriplem4  16752  pythagtriplem8  16756  pythagtriplem9  16757  pythagtriplem12  16759  pythagtriplem14  16761  pythagtriplem16  16763  pcexp  16792  pc2dvds  16812  pcz  16814  fldivp1  16830  pcfac  16832  oddprmdvds  16836  pockthg  16839  infpnlem1  16843  prmreclem1  16849  prmreclem2  16850  1arith  16860  4sqlem11  16888  vdwlem2  16915  vdwlem8  16921  vdwnnlem2  16929  prmgaplem7  16990  prmgaplem8  16991  cshwshashlem2  17030  cshwshashlem3  17031  pwsval  17432  isacs1i  17601  funcsetcestrclem9  18115  ismgmid  18584  mhmpropd  18678  smndex1gid  18784  smndex1id  18792  grpsubid1  18908  mulgnnp1  18962  mulgsubcl  18968  mulgnn0z  18981  mulgnndir  18983  mulgneg2  18988  lagsubg  19072  ghmco  19112  symg2bas  19260  symgextfv  19286  pgpfi2  19474  efgsfo  19607  frgpupf  19641  frgpup1  19643  gsummptshft  19804  telgsumfzslem  19856  telgsums  19861  ablfac1eu  19943  pgpfac1lem2  19945  ablfaclem3  19957  dvdsrid  20181  dvdsrneg  20184  dvr1  20221  abv1  20441  lmodfopne  20510  lbsexg  20777  xrsds  20988  znf1o  21107  lindfmm  21382  gsummoncoe1  21828  matecl  21927  mavmul0g  22055  gsummatr01  22161  mp2pm2mplem4  22311  chfacfisf  22356  chfacfisfcpmat  22357  chfacfpmmulgsum2  22367  cpmadugsumlemF  22378  isclo  22591  resttopon  22665  restcld  22676  restcls  22685  iscn  22739  iscnp  22741  cnco  22770  cndis  22795  cnindis  22796  cmpsub  22904  hauscmplem  22910  cmpfii  22913  ptcnplem  23125  txtube  23144  txcmplem1  23145  xkoptsub  23158  qtoptop  23204  kqfval  23227  hmeoco  23276  fileln0  23354  trfil1  23390  trfil2  23391  trufil  23414  elfm3  23454  hausflf2  23502  isucn  23783  bl2in  23906  metss2lem  24020  metss2  24021  stdbdxmet  24024  metrest  24033  nmval2  24101  nmoix  24246  ioo2bl  24309  xrsxmet  24325  expcn  24388  elcncf  24405  icccvx  24466  cphsscph  24768  iscmet3  24810  causs  24815  metcld2  24824  metsscmetcld  24832  cncmet  24839  bcth3  24848  ovolgelb  24997  ovolfi  25011  shft2rab  25025  uniioombllem3  25102  dyadmax  25115  dyadmbl  25117  subopnmbl  25121  volcn  25123  mbfid  25152  mbfeqalem2  25159  mbfres  25161  cnmbf  25176  i1fmulc  25221  mbfi1fseqlem3  25235  mbfi1fseqlem4  25236  itg2seq  25260  itg2gt0  25278  itgss3  25332  dvexp  25470  plypow  25719  plyeq0lem  25724  coeidlem  25751  dgrlt  25780  dgrcolem2  25788  elqaalem2  25833  aacjcl  25840  aaliou3lem1  25855  aaliou3lem2  25856  pserdvlem2  25940  abelthlem8  25951  cosord  26040  sinord  26043  resinf1o  26045  relogexp  26104  logdivlt  26129  advlogexp  26163  logcxp  26177  cxpcl  26182  rpcxpcl  26184  cxpne0  26185  logbchbase  26276  logbgt0b  26298  birthdaylem2  26457  cxplim  26476  divsqrtsumo1  26488  zetacvg  26519  wilthlem1  26572  ftalem7  26583  basellem1  26585  issqf  26640  sqf11  26643  sgmf  26649  sgmnncl  26651  sqff1o  26686  dvdsflsumcom  26692  dvdsmulf1o  26698  sgmppw  26700  chtublem  26714  chtub  26715  logexprlim  26728  bposlem3  26789  bposlem5  26791  bposlem6  26792  lgsdirnn0  26847  gausslemma2dlem1a  26868  gausslemma2dlem5a  26873  lgsquad2  26889  lgsquad3  26890  2sqreulem1  26949  2sqreunnlem1  26952  dchrisumlem1  26992  dchrisumlem2  26993  dchrisumlem3  26994  mulogsumlem  27034  noextenddif  27171  addsrid  27448  sltneg  27519  sleneg  27520  brbtwn  28157  uspgrupgrushgr  28437  usgrumgruspgr  28440  cusgrfilem2  28713  finsumvtxdg2ssteplem2  28803  crctcshwlkn0lem4  29067  crctcshwlkn0lem6  29069  crctcshwlkn0lem7  29070  crctcshwlkn0  29075  elwspths2spth  29221  rusgrnumwwlk  29229  clwlkclwwlklem2fv2  29249  erclwwlknref  29322  1to2vfriswmgr  29532  4cycl2v2nb  29542  frgr2wwlkeqm  29584  nvo00  30014  nmorepnf  30021  ubthlem1  30123  normpyc  30399  occon3  30550  pjpreeq  30651  idcnop  31234  riesz3i  31315  cnlnssadj  31333  rnbra  31360  strlem3a  31505  cvcon3  31537  ssdmd1  31566  ssdmd2  31567  relfi  31833  fzsplit3  32005  prmsimpcyc  32373  esumcst  33061  dmvlsiga  33127  ballotlemimin  33504  bnj545  33906  bnj929  33947  bnj953  33950  pthhashvtx  34118  derangsn  34161  iscvm  34250  cvmsval  34257  cvmliftlem7  34282  cvmlift2lem12  34305  mclsssvlem  34553  supfz  34698  faclimlem3  34715  gg-expcn  35164  opnrebl2  35206  nn0prpwlem  35207  tailval  35258  nndivlub  35343  ctbssinf  36287  finixpnum  36473  ltflcei  36476  lindsdom  36482  lindsenlbs  36483  matunitlindflem2  36485  poimirlem4  36492  poimirlem14  36502  poimirlem15  36503  poimirlem19  36507  poimirlem20  36508  poimirlem22  36510  poimirlem24  36512  poimirlem28  36516  poimirlem30  36518  poimirlem31  36519  mblfinlem2  36526  mblfinlem3  36527  mblfinlem4  36528  ftc1anclem1  36561  ftc1anclem4  36564  ftc1anclem5  36565  ftc1anclem7  36567  ftc1anclem8  36568  ftc1anc  36569  caushft  36629  ismtyval  36668  heiborlem7  36685  heiborlem10  36688  heibor  36689  lcmineqlem8  40901  f1o2d2  41055  oexpreposd  41212  elrfirn  41433  ismrc  41439  nacsfix  41450  mzpcompact2lem  41489  eldiophb  41495  ellz1  41505  rexrabdioph  41532  congrep  41712  jm2.26a  41739  rngunsnply  41915  mendring  41934  iocmbl  41962  oeord2lim  42059  cantnfresb  42074  omabs2  42082  ofoafg  42104  dfno2  42179  rp-isfinite5  42268  enrelmap  42748  expgrowthi  43092  cnfex  43712  xlimclim2lem  44555  climxlim2  44562  icccncfext  44603  itgsinexp  44671  iblspltprt  44689  itgspltprt  44695  fourierdlem50  44872  fourierswlem  44946  etransclem35  44985  zm1nn  46010  subsubelfzo0  46034  iccpartres  46086  iccelpart  46101  iccpartiun  46102  iccpartnel  46106  goldbachthlem1  46213  goldbachth  46215  odz2prm2pw  46231  2pwp1prm  46257  evenltle  46385  fpprwpprb  46408  sbgoldbaltlem2  46448  bgoldbachlt  46481  isomushgr  46494  isomuspgrlem1  46495  isomgrtr  46507  upgrwlkupwlk  46518  mgmhmpropd  46555  2zrngamgm  46837  lincresunit3  47162  lincreslvec3  47163  isldepslvec2  47166  m1modmmod  47207  blengt1fldiv2p1  47279  dignn0flhalf  47304  nn0sumshdiglemA  47305  rrx2pnedifcoorneor  47402  aacllem  47848