Theorem syl2anr 495

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  swopo  5045  ordintdif  5774  funco  5928  resdif  6157  fvcofneq  6367  fnprb  6472  fntpb  6473  isotr  6586  weisoeq  6605  brrpssg  6939  findsg  7093  coexg  7117  xpexgALT  7161  fnsuppres  7322  wfrlem10  7424  oaass  7641  oeword  7670  oeworde  7673  ixpssmapg  7938  pw2f1olem  8064  domsdomtr  8095  xpen  8123  mapen  8124  mapdom1  8125  mapfienlem1  8310  elfir  8321  wdomen2  8482  carden2b  8793  harcard  8804  isinffi  8818  acnlem  8871  acndom  8874  alephdom  8904  fin23lem21  9161  fin23lem39  9172  isf32lem5  9179  fin1a2lem12  9233  axdc3lem2  9273  ttukeylem1  9331  pwcfsdom  9405  canthp1  9476  nqereu  9751  addpqf  9766  axmulf  9967  axmulass  9978  axdistr  9979  ltaddnegr  10252  negeu  10271  fimaxre3  10970  nnsub  11059  nn0sub  11343  ltsubnn0  11344  elz2  11394  uzaddcl  11744  qaddcl  11804  xltneg  12048  xleneg  12049  supxrbnd1  12151  infxrgelb  12165  iccneg  12293  uzsubsubfz  12363  fzsplit2  12366  fzadd2  12376  fzss1  12380  uzsplit  12412  fz0fzdiffz0  12448  difelfzle  12452  difelfznle  12453  fvffz0  12457  preduz  12461  predfz  12464  fzonlt0  12491  fzouzsplit  12503  fzo0addelr  12522  eluzgtdifelfzo  12529  elfzodifsumelfzo  12533  ssfzo12  12561  elfznelfzob  12574  fllt  12607  flflp1  12608  uzsup  12662  negmod  12715  modifeq2int  12732  modfzo0difsn  12742  modsumfzodifsn  12743  om2uzlt2i  12750  nn0ennn  12778  suppssfz  12794  seqfveq2  12823  sermono  12833  seqf1o  12842  ser1const  12857  mulsubdivbinom2  13046  faclbnd  13077  bcval4  13094  bcpasc  13108  hashkf  13119  hashunx  13175  hashfacen  13238  fz1isolem  13245  ishashinf  13247  seqcoll  13248  ccatalpha  13375  swrd0  13434  swrdfv2  13446  swrdspsleq  13449  swrdswrd  13460  swrdccatin12lem2  13489  swrdccat3  13492  revccat  13515  repswswrd  13531  cshwmodn  13541  cshwidxmod  13549  repswcshw  13558  2cshwid  13560  2cshwcom  13562  2cshwcshw  13571  cshwcshid  13573  cshwcsh2id  13574  s1co  13579  cshco  13582  trclub  13739  shftfval  13810  seqshft  13825  crim  13855  caubnd  14098  limsuplt  14210  isercolllem2  14396  fsumcvg  14443  fsumcvg2  14458  fsumshftm  14513  fsumo1  14544  isumshft  14571  harmonic  14591  cvgrat  14615  mertenslem1  14616  zprod  14667  fprodmodd  14728  bpolylem  14779  bpolysum  14784  bpolydiflem  14785  fsumkthpow  14787  rpnnen2lem12  14954  dvdsval3  14987  negdvdsb  14998  dvdsnegb  14999  dvdsmul1  15003  dvdsabseq  15035  dvdsssfz1  15040  odd2np1  15065  divalglem8  15123  ndvdsadd  15134  dfgcd2  15263  dvdssqim  15273  nn0seqcvgd  15283  seq1st  15284  algcvgblem  15290  lcmf  15346  lcmfunsnlem2  15353  cncongr2  15382  prmdvdsfz  15417  isprm7  15420  prmndvdsfaclt  15435  powm2modprm  15508  modprm0  15510  modprmn0modprm0  15512  pythagtriplem1  15521  pythagtriplem4  15524  pythagtriplem8  15528  pythagtriplem9  15529  pythagtriplem12  15531  pythagtriplem14  15533  pythagtriplem16  15535  pcexp  15564  pc2dvds  15583  pcz  15585  fldivp1  15601  pcfac  15603  oddprmdvds  15607  pockthg  15610  infpnlem1  15614  prmreclem1  15620  prmreclem2  15621  1arith  15631  4sqlem11  15659  vdwlem2  15686  vdwlem8  15692  vdwnnlem2  15700  prmgaplem7  15761  prmgaplem8  15762  cshwshashlem2  15803  cshwshashlem3  15804  pwsval  16146  isacs1i  16318  funcsetcestrclem9  16803  ismgmid  17264  mhmpropd  17341  grpsubid1  17500  mulgnnp1  17549  mulgsubcl  17555  mulgnn0z  17567  mulgnndir  17569  mulgnndirOLD  17570  mulgneg2  17575  lagsubg  17656  ghmco  17680  symg2bas  17818  symgextfv  17838  pgpfi2  18021  efgsfo  18152  frgpupf  18186  frgpup1  18188  gsummptshft  18336  telgsumfzslem  18385  telgsums  18390  ablfac1eu  18472  pgpfac1lem2  18474  ablfaclem3  18486  dvdsrid  18651  dvdsrneg  18654  dvr1  18689  abv1  18833  lmodfopne  18901  lbsexg  19164  gsummoncoe1  19674  xrsds  19789  znf1o  19900  lindfmm  20166  matecl  20231  mavmul0g  20359  gsummatr01  20465  mp2pm2mplem4  20614  chfacfisf  20659  chfacfisfcpmat  20660  chfacfpmmulgsum2  20670  cpmadugsumlemF  20681  isclo  20891  resttopon  20965  restcld  20976  restcls  20985  iscn  21039  iscnp  21041  cnco  21070  cndis  21095  cnindis  21096  cmpsub  21203  hauscmplem  21209  cmpfii  21212  ptcnplem  21424  txtube  21443  txcmplem1  21444  xkoptsub  21457  qtoptop  21503  kqfval  21526  hmeoco  21575  fileln0  21654  trfil1  21690  trfil2  21691  trufil  21714  elfm3  21754  hausflf2  21802  isucn  22082  bl2in  22205  metss2lem  22316  metss2  22317  stdbdxmet  22320  metrest  22329  nmfval2  22395  nmval2  22396  nmoix  22533  ioo2bl  22596  xrsxmet  22612  expcn  22675  elcncf  22692  icccvx  22749  iscmet3  23091  causs  23096  metcld2  23105  cmetss  23113  cncmet  23119  bcth3  23128  ovolgelb  23248  ovolfi  23262  shft2rab  23276  uniioombllem3  23353  dyadmax  23366  dyadmbl  23368  subopnmbl  23372  volcn  23374  mbfid  23403  mbfeqalem  23409  mbfres  23411  cnmbf  23426  i1fmulc  23470  mbfi1fseqlem3  23484  mbfi1fseqlem4  23485  itg2seq  23509  itg2gt0  23527  itgss3  23581  dvexp  23716  plypow  23961  plyeq0lem  23966  coeidlem  23993  dgrlt  24022  dgrcolem2  24030  elqaalem2  24075  aacjcl  24082  aaliou3lem1  24097  aaliou3lem2  24098  pserdvlem2  24182  abelthlem8  24193  cosord  24278  sinord  24280  resinf1o  24282  relogexp  24342  logdivlt  24367  advlogexp  24401  logcxp  24415  cxpcl  24420  rpcxpcl  24422  cxpne0  24423  logbchbase  24509  birthdaylem2  24679  cxplim  24698  divsqrtsumo1  24710  zetacvg  24741  wilthlem1  24794  ftalem7  24805  basellem1  24807  issqf  24862  sqf11  24865  sgmf  24871  sgmnncl  24873  sqff1o  24908  dvdsflsumcom  24914  dvdsmulf1o  24920  sgmppw  24922  chtublem  24936  chtub  24937  logexprlim  24950  bposlem3  25011  bposlem5  25013  bposlem6  25014  lgsdirnn0  25069  gausslemma2dlem1a  25090  gausslemma2dlem5a  25095  lgsquad2  25111  lgsquad3  25112  dchrisumlem1  25178  dchrisumlem2  25179  dchrisumlem3  25180  mulogsumlem  25220  brbtwn  25779  uspgrupgrushgr  26072  usgrumgruspgr  26075  cusgrfilem2  26352  finsumvtxdg2ssteplem2  26442  crctcshwlkn0lem4  26705  crctcshwlkn0lem6  26707  crctcshwlkn0lem7  26708  crctcshwlkn0  26713  elwspths2spth  26862  rusgrnumwwlk  26870  clwlkclwwlklem2fv2  26897  1to2vfriswmgr  27143  4cycl2v2nb  27153  frgr2wwlkeqm  27195  numclwwlk8  27250  nvo00  27616  nmorepnf  27623  ubthlem1  27726  normpyc  28003  occon3  28156  pjpreeq  28257  idcnop  28840  riesz3i  28921  cnlnssadj  28939  rnbra  28966  strlem3a  29111  cvcon3  29143  ssdmd1  29172  ssdmd2  29173  relfi  29415  fzsplit3  29553  esumcst  30125  dmvlsiga  30192  ballotlemimin  30567  bnj545  30965  bnj929  31006  bnj953  31009  derangsn  31152  iscvm  31241  cvmsval  31248  cvmliftlem7  31273  cvmlift2lem12  31296  mclsssvlem  31459  supfz  31613  faclimlem3  31631  noextenddif  31821  opnrebl2  32316  nn0prpwlem  32317  tailval  32368  nndivlub  32457  finixpnum  33394  ltflcei  33397  lindsdom  33403  lindsenlbs  33404  matunitlindflem2  33406  poimirlem4  33413  poimirlem14  33423  poimirlem15  33424  poimirlem19  33428  poimirlem20  33429  poimirlem22  33431  poimirlem24  33433  poimirlem28  33437  poimirlem30  33439  poimirlem31  33440  mblfinlem2  33447  mblfinlem3  33448  mblfinlem4  33449  ftc1anclem1  33485  ftc1anclem4  33488  ftc1anclem5  33489  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  caushft  33557  ismtyval  33599  heiborlem7  33616  heiborlem10  33619  heibor  33620  elrfirn  37258  ismrc  37264  nacsfix  37275  mzpcompact2lem  37314  eldiophb  37320  ellz1  37330  rexrabdioph  37358  rpexpmord  37513  congrep  37540  jm2.26a  37567  rngunsnply  37743  mendring  37762  iocmbl  37798  rp-isfinite5  37863  enrelmap  38291  expgrowthi  38532  cnfex  39187  xlimclim2lem  40065  climxlim2  40072  icccncfext  40100  itgsinexp  40170  iblspltprt  40189  itgspltprt  40195  fourierdlem50  40373  fourierswlem  40447  etransclem35  40486  zm1nn  41316  subsubelfzo0  41336  iccpartres  41354  iccelpart  41369  iccpartiun  41370  iccpartnel  41374  addlenpfx  41398  pfxccatin12lem2  41424  pfxccat3  41426  goldbachthlem1  41457  goldbachth  41459  odz2prm2pw  41475  fmtnoprmfac1lem  41476  2pwp1prm  41503  evenltle  41626  sbgoldbaltlem2  41668  bgoldbachlt  41701  bgoldbachltOLD  41707  upgrwlkupwlk  41721  mgmhmpropd  41785  2zrngamgm  41939  lincresunit3  42270  lincreslvec3  42271  isldepslvec2  42274  m1modmmod  42316  blengt1fldiv2p1  42387  dignn0flhalf  42412  nn0sumshdiglemA  42413  aacllem  42547