Theorem syl2anr 595

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

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  swopo  5607  ordintdif  6428  funco  6601  resdif  6866  fvcofneq  7109  fnprb  7227  fntpb  7228  isotr  7350  weisoeq  7369  brrpssg  7738  findsg  7912  coexg  7944  xpexgALT  7997  fnsuppres  8207  wfrlem10OLD  8350  oaass  8593  oeword  8622  oeworde  8625  mapsnd  8917  ixpssmapg  8959  enrefnn  9087  pw2f1olem  9116  domsdomtr  9152  xpen  9180  mapen  9181  mapdom1  9182  phplem2  9244  mapfienlem1  9450  elfir  9460  wdomen2  9622  carden2b  10012  harcard  10023  isinffi  10037  acnlem  10093  acndom  10096  alephdom  10126  fin23lem21  10384  fin23lem39  10395  isf32lem5  10402  fin1a2lem12  10456  axdc3lem2  10496  ttukeylem1  10554  pwcfsdom  10628  canthp1  10699  nqereu  10974  addpqf  10989  axmulf  11191  axmulass  11202  axdistr  11203  ltaddnegr  11482  negeu  11502  fimaxre3  12214  nnsub  12310  nn0sub  12576  ltsubnn0  12577  elz2  12630  uzaddcl  12942  qaddcl  13003  xltneg  13252  xleneg  13253  supxrbnd1  13356  infxrgelb  13370  iccneg  13505  uzsubsubfz  13579  fzsplit2  13582  fzadd2  13592  fzss1  13596  uzsplit  13629  fz0fzdiffz0  13666  difelfzle  13670  difelfznle  13671  fvffz0  13675  preduz  13679  predfz  13682  fzonlt0  13711  fzouzsplit  13723  fzo0addelr  13743  eluzgtdifelfzo  13750  elfzodifsumelfzo  13754  ssfzo12  13781  elfznelfzob  13795  fllt  13828  flflp1  13829  uzsup  13885  negmod  13938  modifeq2int  13955  modfzo0difsn  13965  modsumfzodifsn  13966  om2uzlt2i  13973  nn0ennn  14001  suppssfz  14016  seqfveq2  14046  sermono  14056  seqf1o  14065  ser1const  14080  rpexpmord  14189  mulsubdivbinom2  14281  faclbnd  14309  bcval4  14326  bcpasc  14340  hashkf  14351  hashunx  14405  hashfacenOLD  14474  fz1isolem  14482  ishashinf  14484  seqcoll  14485  ccatval1  14587  ccatval21sw  14595  ccatrn  14599  ccatalpha  14603  swrdnd0  14667  swrd0  14668  swrdfv2  14671  swrdspsleq  14675  addlenpfx  14701  ccatpfx  14711  swrdswrd  14715  pfxccatin12lem2  14741  pfxccat3  14744  swrdccat  14745  revccat  14776  repswswrd  14794  cshwmodn  14805  cshwidxmod  14813  repswcshw  14822  2cshwid  14824  2cshwcom  14826  2cshwcshw  14836  cshwcshid  14838  cshwcsh2id  14839  s1co  14844  cshco  14847  trclub  15005  shftfval  15077  seqshft  15092  crim  15122  caubnd  15365  limsuplt  15483  isercolllem2  15672  fsumcvg  15718  fsumcvg2  15733  fsumshftm  15787  fsumo1  15818  isumshft  15845  harmonic  15865  cvgrat  15889  mertenslem1  15890  zprod  15941  fprodmodd  16001  bpolylem  16052  bpolysum  16057  bpolydiflem  16058  fsumkthpow  16060  rpnnen2lem12  16229  dvdsval3  16262  negdvdsb  16277  dvdsnegb  16278  dvdsmul1  16282  dvdsabseq  16317  dvdsssfz1  16322  odd2np1  16345  divalglem8  16404  ndvdsadd  16414  dfgcd2  16549  dvdssqim  16557  nn0seqcvgd  16573  seq1st  16574  algcvgblem  16580  lcmf  16636  lcmfunsnlem2  16643  cncongr2  16671  prmdvdsfz  16708  isprm7  16711  prmndvdsfaclt  16729  powm2modprm  16807  modprm0  16809  modprmn0modprm0  16811  pythagtriplem1  16820  pythagtriplem4  16823  pythagtriplem8  16827  pythagtriplem9  16828  pythagtriplem12  16830  pythagtriplem14  16832  pythagtriplem16  16834  pcexp  16863  pc2dvds  16883  pcz  16885  fldivp1  16901  pcfac  16903  oddprmdvds  16907  pockthg  16910  infpnlem1  16914  prmreclem1  16920  prmreclem2  16921  1arith  16931  4sqlem11  16959  vdwlem2  16986  vdwlem8  16992  vdwnnlem2  17000  prmgaplem7  17061  prmgaplem8  17062  cshwshashlem2  17101  cshwshashlem3  17102  pwsval  17503  isacs1i  17672  funcsetcestrclem9  18189  ismgmid  18660  mgmhmpropd  18693  mhmpropd  18784  smndex1gid  18895  smndex1id  18903  grpsubid1  19021  mulgnnp1  19078  mulgsubcl  19084  mulgnn0z  19097  mulgnndir  19099  mulgneg2  19104  lagsubg  19191  ghmco  19232  symg2bas  19392  symgextfv  19418  pgpfi2  19606  efgsfo  19739  frgpupf  19773  frgpup1  19775  gsummptshft  19936  telgsumfzslem  19988  telgsums  19993  ablfac1eu  20075  pgpfac1lem2  20077  ablfaclem3  20089  dvdsrid  20351  dvdsrneg  20354  dvr1  20391  abv1  20806  lmodfopne  20878  lbsexg  21147  xrsds  21408  znf1o  21551  lindfmm  21827  gsummoncoe1  22302  matecl  22421  mavmul0g  22549  gsummatr01  22655  mp2pm2mplem4  22805  chfacfisf  22850  chfacfisfcpmat  22851  chfacfpmmulgsum2  22861  cpmadugsumlemF  22872  isclo  23085  resttopon  23159  restcld  23170  restcls  23179  iscn  23233  iscnp  23235  cnco  23264  cndis  23289  cnindis  23290  cmpsub  23398  hauscmplem  23404  cmpfii  23407  ptcnplem  23619  txtube  23638  txcmplem1  23639  xkoptsub  23652  qtoptop  23698  kqfval  23721  hmeoco  23770  fileln0  23848  trfil1  23884  trfil2  23885  trufil  23908  elfm3  23948  hausflf2  23996  isucn  24277  bl2in  24400  metss2lem  24514  metss2  24515  stdbdxmet  24518  metrest  24527  nmval2  24595  nmoix  24740  ioo2bl  24803  xrsxmet  24819  expcn  24884  expcnOLD  24886  elcncf  24903  icccvx  24969  cphsscph  25273  iscmet3  25315  causs  25320  metcld2  25329  metsscmetcld  25337  cncmet  25344  bcth3  25353  ovolgelb  25503  ovolfi  25517  shft2rab  25531  uniioombllem3  25608  dyadmax  25621  dyadmbl  25623  subopnmbl  25627  volcn  25629  mbfid  25658  mbfeqalem2  25665  mbfres  25667  cnmbf  25682  i1fmulc  25727  mbfi1fseqlem3  25741  mbfi1fseqlem4  25742  itg2seq  25766  itg2gt0  25784  itgss3  25838  dvexp  25979  plypow  26235  plyeq0lem  26240  coeidlem  26267  dgrlt  26297  dgrcolem2  26305  elqaalem2  26351  aacjcl  26358  aaliou3lem1  26373  aaliou3lem2  26374  pserdvlem2  26461  abelthlem8  26472  cosord  26561  sinord  26564  resinf1o  26566  relogexp  26626  logdivlt  26651  advlogexp  26685  logcxp  26699  cxpcl  26704  rpcxpcl  26706  cxpne0  26707  logbchbase  26802  logbgt0b  26824  birthdaylem2  26983  cxplim  27003  divsqrtsumo1  27015  zetacvg  27046  wilthlem1  27099  ftalem7  27110  basellem1  27112  issqf  27167  sqf11  27170  sgmf  27176  sgmnncl  27178  sqff1o  27213  dvdsflsumcom  27219  mpodvdsmulf1o  27225  dvdsmulf1o  27227  sgmppw  27229  chtublem  27243  chtub  27244  logexprlim  27257  bposlem3  27318  bposlem5  27320  bposlem6  27321  lgsdirnn0  27376  gausslemma2dlem1a  27397  gausslemma2dlem5a  27402  lgsquad2  27418  lgsquad3  27419  2sqreulem1  27478  2sqreunnlem1  27481  dchrisumlem1  27521  dchrisumlem2  27522  dchrisumlem3  27523  mulogsumlem  27563  noextenddif  27701  addsrid  27981  sltneg  28057  sleneg  28058  om2noseqlt2  28277  elzn0s  28345  brbtwn  28836  uspgrupgrushgr  29118  usgrumgruspgr  29121  cusgrfilem2  29396  finsumvtxdg2ssteplem2  29486  crctcshwlkn0lem4  29750  crctcshwlkn0lem6  29752  crctcshwlkn0lem7  29753  crctcshwlkn0  29758  elwspths2spth  29904  rusgrnumwwlk  29912  clwlkclwwlklem2fv2  29932  erclwwlknref  30005  1to2vfriswmgr  30215  4cycl2v2nb  30225  frgr2wwlkeqm  30267  nvo00  30697  nmorepnf  30704  ubthlem1  30806  normpyc  31082  occon3  31233  pjpreeq  31334  idcnop  31917  riesz3i  31998  cnlnssadj  32016  rnbra  32043  strlem3a  32188  cvcon3  32220  ssdmd1  32249  ssdmd2  32250  relfi  32524  fzsplit3  32698  prmsimpcyc  33094  esumcst  33898  dmvlsiga  33964  ballotlemimin  34341  bnj545  34742  bnj929  34783  bnj953  34786  pthhashvtx  34957  derangsn  35000  iscvm  35089  cvmsval  35096  cvmliftlem7  35121  cvmlift2lem12  35144  mclsssvlem  35392  supfz  35553  faclimlem3  35569  opnrebl2  36035  nn0prpwlem  36036  tailval  36087  nndivlub  36172  ctbssinf  37115  finixpnum  37308  ltflcei  37311  lindsdom  37317  lindsenlbs  37318  matunitlindflem2  37320  poimirlem4  37327  poimirlem14  37337  poimirlem15  37338  poimirlem19  37342  poimirlem20  37343  poimirlem22  37345  poimirlem24  37347  poimirlem28  37351  poimirlem30  37353  poimirlem31  37354  mblfinlem2  37361  mblfinlem3  37362  mblfinlem4  37363  ftc1anclem1  37396  ftc1anclem4  37399  ftc1anclem5  37400  ftc1anclem7  37402  ftc1anclem8  37403  ftc1anc  37404  caushft  37464  ismtyval  37503  heiborlem7  37520  heiborlem10  37523  heibor  37524  lcmineqlem8  41737  deg1gprod  41840  f1o2d2  41959  oexpreposd  42028  elrfirn  42370  ismrc  42376  nacsfix  42387  mzpcompact2lem  42426  eldiophb  42432  ellz1  42442  rexrabdioph  42469  congrep  42649  jm2.26a  42676  rngunsnply  42852  mendring  42871  iocmbl  42896  oeord2lim  42993  cantnfresb  43008  omabs2  43016  ofoafg  43038  dfno2  43113  rp-isfinite5  43202  enrelmap  43682  expgrowthi  44025  cnfex  44645  xlimclim2lem  45478  climxlim2  45485  icccncfext  45526  itgsinexp  45594  iblspltprt  45612  itgspltprt  45618  fourierdlem50  45795  fourierswlem  45869  etransclem35  45908  zm1nn  46933  subsubelfzo0  46957  iccpartres  47008  iccelpart  47023  iccpartiun  47024  iccpartnel  47028  goldbachthlem1  47135  goldbachth  47137  odz2prm2pw  47153  2pwp1prm  47179  evenltle  47307  fpprwpprb  47330  sbgoldbaltlem2  47370  bgoldbachlt  47403  gricushgr  47483  uhgrimisgrgriclem  47495  upgrwlkupwlk  47535  2zrngamgm  47640  lincresunit3  47882  lincreslvec3  47883  isldepslvec2  47886  m1modmmod  47927  blengt1fldiv2p1  47999  dignn0flhalf  48024  nn0sumshdiglemA  48025  rrx2pnedifcoorneor  48122  aacllem  48567