Theorem ad3antrrr 730

Description: Deduction adding three conjuncts to antecedent. (Contributed by NM, 28-Jul-2012.)

Hypothesis

Ref	Expression
ad2ant.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ad3antrrr	⊢ ((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Proof of Theorem ad3antrrr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad2antrr 726	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:  ad4antr  732  ad4antlr  733  simplll  774  fsnex  7229  fimaproj  8077  frxp3  8093  oaabs  8576  oaabs2  8577  omabs  8579  cofon1  8600  sbthlem8  9022  cantnfle  9580  cantnfp1  9590  cantnflem1c  9596  sornom  10187  enfin2i  10231  ttukeylem6  10424  fpwwe2lem12  10553  fpwwe2  10554  winalim2  10607  wuncval2  10658  negf1o  11567  xlemul1a  13203  difreicc  13400  flflp1  13727  faclbnd  14213  swrdswrd  14628  swrdccatin1  14648  pfxccatin12lem3  14655  swrdccat3blem  14662  ello12  15439  lo1bdd2  15447  elo12  15450  rlimclim1  15468  rlimcld2  15501  o1co  15509  o1of2  15536  o1rlimmul  15542  rlimsqzlem  15572  isercoll  15591  o1fsum  15736  supcvg  15779  dvds2ln  16216  lcmgcdlem  16533  cncongr2  16595  isprm5  16634  prmdvdsncoprmbd  16654  pcadd  16817  vdwlem2  16910  vdwlem11  16919  sbcie3s  17089  prdsval  17375  mreexexlem4d  17570  isacs2  17576  catcocl  17608  catass  17609  subccocl  17769  fullsubc  17774  funcco  17795  funcpropd  17826  fullpropd  17846  ffthiso  17855  isnat  17874  natpropd  17903  fucpropd  17904  xpcval  18100  evlf2  18141  curfpropd  18156  curfuncf  18161  uncfcurf  18162  curf2ndf  18170  hofcl  18182  hofpropd  18190  yonffthlem  18205  isacs3lem  18465  acsfiindd  18476  chnind  18544  gsumpropd2lem  18604  resmgmhm2b  18638  resmhm2b  18747  mhmid  18993  mhmmnd  18994  ghmgrp  18996  conjnmzb  19182  ghmqusnsg  19211  ghmquskerlem3  19215  ghmqusker  19216  pgpfi  19534  sylow3lem2  19557  efgredlem  19676  frgpnabllem1  19802  imasabl  19805  dprdfcntz  19946  ablfac1b  20001  pgpfac1lem3  20008  pgpfac1lem5  20010  pgpfaclem3  20014  omndmul2  20062  gsumle  20074  ringinvnzdiv  20236  rnghmsubcsetclem2  20565  rhmsubcsetclem2  20594  srhmsubc  20613  rhmsubclem4  20621  imadrhmcl  20730  cntzsdrg  20735  suborng  20809  islmhm2  20990  lspsneleq  21070  rhmpreimaidl  21232  znunit  21518  psgndiflemB  21555  uvcff  21746  uvcf1  21747  lindfmm  21782  sraassab  21823  psrval  21871  psrass1  21919  resspsrmul  21931  mplbas2  21997  evlsvvval  22048  mhpmulcl  22092  psdmul  22109  coe1tmmul  22219  gsummoncoe1  22252  evls1fpws  22313  dmatsubcl  22442  scmatscm  22457  smatvscl  22468  marrepval  22506  mdetdiaglem  22542  mdetunilem8  22563  mdetunilem9  22564  pmatcoe1fsupp  22645  decpmatmulsumfsupp  22717  pmatcollpw2lem  22721  mp2pm2mplem4  22753  pm2mpmhmlem1  22762  pm2mpmhmlem2  22763  pm2mp  22769  fvmptnn04if  22793  cpmadugsumfi  22821  cpmidg2sum  22824  cpmadumatpoly  22827  cayhamlem4  22832  neiptoptop  23075  neitr  23124  ordtrest2lem  23147  cnpnei  23208  iscncl  23213  cncls  23218  cnntr  23219  cncnp  23224  lmcnp  23248  isreg2  23321  hauscmplem  23350  cmpfi  23352  1stcfb  23389  1stcrest  23397  2ndcctbss  23399  2ndcomap  23402  islly2  23428  cldllycmp  23439  lly1stc  23440  locfincmp  23470  llycmpkgen2  23494  1stckgenlem  23497  kgencn2  23501  kgencn3  23502  ptbasfi  23525  ptpjopn  23556  txdis1cn  23579  txlly  23580  txnlly  23581  txtube  23584  txcmplem2  23586  tx1stc  23594  txkgen  23596  xkopt  23599  xkoco2cn  23602  xkococnlem  23603  xkococn  23604  xkoinjcn  23631  tgqtop  23656  regr1lem  23683  kqreglem1  23685  nrmhmph  23738  rnelfmlem  23896  rnelfm  23897  fmfnfmlem4  23901  fmfnfm  23902  ufldom  23906  flimopn  23919  hauspwpwf1  23931  fclsopn  23958  fclsnei  23963  fclsrest  23968  alexsublem  23988  alexsubALTlem3  23993  ptcmplem2  23997  ptcmplem3  23998  cnextfun  24008  cnextcn  24011  symgtgp  24050  tgpt0  24063  qustgpopn  24064  tsmsxplem1  24097  trust  24173  utopsnneiplem  24191  utop3cls  24195  utopreg  24196  isucn2  24222  cstucnd  24227  ucncn  24228  fmucnd  24235  cfilufg  24236  neipcfilu  24239  met2ndci  24466  prdsxmslem2  24473  metcnp3  24484  metustid  24498  metustexhalf  24500  metust  24502  psmetutop  24511  nmoleub  24675  reconnlem2  24772  xrge0tsms  24779  cncfco  24856  lebnumlem3  24918  lebnum  24919  nmoleub2lem2  25072  nmoleub3  25075  iscfil2  25222  iscau4  25235  iscmet3lem2  25248  equivcfil  25255  equivcau  25256  caubl  25264  rrxdstprj1  25365  ovolshftlem2  25467  ovolicc2lem4  25477  uniioombl  25546  i1fmulclem  25659  mbfi1fseqlem6  25677  itg2const2  25698  itg2split  25706  bddiblnc  25799  ellimc2  25834  ellimc3  25836  limcflf  25838  dvmptfsum  25935  dvferm1  25945  dvferm2  25947  dvlip2  25956  c1lip1  25958  lhop1  25975  ftc1a  26000  ply1divex  26098  plyeq0lem  26171  plymullem1  26175  coemullem  26211  coemulc  26216  ulmshftlem  26354  ulmcaulem  26359  ulmbdd  26363  ulmcn  26364  ulmdvlem3  26367  mtestbdd  26370  pserulm  26387  pserdvlem2  26394  abelthlem8  26405  xrlimcnp  26934  jensen  26955  lgamucov  27004  logfac2  27184  dchrelbas3  27205  dchrpt  27234  gausslemma2dlem1a  27332  lgsquad3  27354  2sqb  27399  rpvmasumlem  27454  dchrisumlem1  27456  dchrisumlem3  27458  dchrmusum2  27461  dchrvmasumlem2  27465  dchrisum0flblem1  27475  dchrisum0lem1b  27482  dchrisum0lem1  27483  dchrisum0  27487  mulog2sumlem2  27502  pntlem3  27576  ostth3  27605  lesrec  27795  cofcutr  27920  remulscllem2  28497  istrkgcb  28528  tgbtwndiff  28578  iscgrglt  28586  tgcgrxfr  28590  motcgrg  28616  lnext  28639  tgbtwnconn1  28647  tgbtwnconn3  28649  legval  28656  legtrid  28663  legso  28671  hlcgreu  28690  tglnne  28700  tglineeltr  28703  tglnne0  28712  colline  28721  tglowdim2l  28722  tglowdim2ln  28723  mirreu3  28726  mirbtwnhl  28752  krippenlem  28762  midexlem  28764  perpcom  28785  perpneq  28786  footexALT  28790  footex  28793  colperpexlem3  28804  colperpex  28805  opphllem  28807  midex  28809  oppne3  28815  opptgdim2  28817  oppnid  28818  opphllem2  28820  opphllem5  28823  opphllem6  28824  oppperpex  28825  outpasch  28827  hlpasch  28828  lnopp2hpgb  28835  hpgerlem  28837  colopp  28841  colhp  28842  lmieu  28856  lnperpex  28875  trgcopy  28876  trgcopyeulem  28877  iscgra1  28882  cgrane1  28884  cgrane2  28885  cgrane3  28886  cgrane4  28887  cgrahl1  28888  cgrahl2  28889  cgracgr  28890  cgraswap  28892  cgracom  28894  cgratr  28895  flatcgra  28896  cgrabtwn  28898  cgrahl  28899  sacgr  28903  acopyeu  28906  cgrg3col4  28925  tgasa1  28930  f1otrg  28943  f1otrge  28944  axeuclidlem  29035  axcontlem2  29038  umgrvad2edg  29286  usgredg2vlem2  29299  pthdepisspth  29808  clwwlkccatlem  30064  clwlkclwwlklem2  30075  3cycld  30253  eupth2lems  30313  eucrctshift  30318  frgr3vlem2  30349  n4cyclfrgr  30366  numclwwlk1lem2f1  30432  numclwwlk2lem1  30451  ubthlem3  30947  chirredlem1  32465  chirredlem3  32467  cdj1i  32508  fnpreimac  32749  xrge0infss  32840  nn0xmulclb  32851  hashxpe  32887  sgnmul  32916  2exple2exp  32926  ccatf1  33031  ccatws1f1o  33033  swrdf1  33038  dfmgc2lem  33077  mgcf1o  33085  mndlactf1  33108  mndlactfo  33109  mndractf1  33110  mndractfo  33111  gsumfs2d  33144  gsumhashmul  33150  xrge0tsmsd  33155  gsumwun  33158  psgnfzto1stlem  33182  cycpmco2  33215  cycpmrn  33225  tocyccntz  33226  cycpmconjslem2  33237  cyc3conja  33239  conjga  33252  submarchi  33268  isarchiofld  33281  elrgspnlem1  33324  elrgspnlem2  33325  elrgspnlem3  33326  elrgspnlem4  33327  elrgspnsubrunlem1  33329  elrgspnsubrunlem2  33330  elrgspnsubrun  33331  erlval  33340  erler  33347  rloccring  33352  rlocf1  33355  domnprodn0  33357  domnprodeq0  33358  subrdom  33367  imaslmod  33434  znfermltl  33447  lindfpropd  33463  unitprodclb  33470  nsgmgc  33493  nsgqusf1olem1  33494  unitpidl1  33505  elrspunidl  33509  elrspunsn  33510  rhmimaidl  33513  drngidl  33514  qsidomlem1  33533  mxidlprm  33551  mxidlirredi  33552  drngmxidlr  33559  qsdrngilem  33575  qsdrngi  33576  rsprprmprmidl  33603  rsprprmprmidlb  33604  rprmasso2  33607  rprmirred  33612  rprmirredb  33613  rprmdvdspow  33614  1arithidom  33618  pidufd  33624  1arithufdlem3  33627  dfufd2  33631  deg1prod  33664  ply1dg3rt0irred  33665  extvfvcl  33701  mplvrpmga  33710  mplvrpmmhm  33711  mplvrpmrhm  33712  esplymhp  33726  esplyfval3  33730  esplyind  33731  exsslsb  33753  lbslelsp  33754  ply1degltdimlem  33779  lindsunlem  33781  lindsun  33782  lbsdiflsp0  33783  dimkerim  33784  fedgmul  33788  dimlssid  33789  assalactf1o  33792  extdg1id  33823  evls1fldgencl  33827  fldextrspunlsplem  33830  fldextrspunlsp  33831  extdgfialglem1  33849  minplyirred  33868  fldext2chn  33885  cos9thpiminplylem2  33940  smatrcl  33953  1smat1  33961  submateq  33966  mdetpmtr1  33980  madjusmdetlem2  33985  locfinreflem  33997  cmppcmp  34015  rhmpreimacn  34042  ordtrest2NEWlem  34079  ordtconnlem1  34081  lmdvg  34110  zrhcntr  34136  esumpcvgval  34235  esum2d  34250  sigapildsys  34319  ldgenpisyslem1  34320  fiunelros  34331  volmeas  34388  imambfm  34419  omssubadd  34457  carsggect  34475  carsgclctunlem3  34477  signsply0  34708  signstres  34732  actfunsnf1o  34761  actfunsnrndisj  34762  reprsuc  34772  reprinfz1  34779  breprexplema  34787  breprexplemc  34789  breprexp  34790  breprexpnat  34791  circlemeth  34797  hgt750lemb  34813  tgoldbachgtd  34819  erdszelem8  35392  pconnconn  35425  cvmlift2lem12  35508  cvmlift3lem5  35517  cvmlift3lem7  35519  cvmlift3lem8  35520  fmla1  35581  mrsubrn  35707  msrval  35732  msubff1  35750  btwnconn1lem13  36293  elicc3  36511  neibastop2lem  36554  weiunfr  36661  unbdqndv2  36711  irrdifflemf  37526  ltflcei  37805  lindsenlbs  37812  matunitlindflem1  37813  matunitlindflem2  37814  poimirlem4  37821  poimirlem13  37830  poimirlem14  37831  poimirlem22  37839  poimirlem26  37843  poimirlem27  37844  heicant  37852  mblfinlem2  37855  mblfinlem3  37856  mblfinlem4  37857  cnambfre  37865  itg2addnclem  37868  itg2addnclem2  37869  itg2gt0cn  37872  ftc1cnnc  37889  ftc1anclem5  37894  ftc1anclem7  37896  ftc1anc  37898  equivtotbnd  37975  isbndx  37979  ssbnd  37985  heibor1lem  38006  rrncmslem  38029  islshpat  39273  lfl1dim  39377  lfl1dim2N  39378  lkrpssN  39419  glbconN  39633  hlhgt2  39645  3dim2  39724  3dim3  39725  islln3  39766  islvol5  39835  2lplnja  39875  dalem19  39938  isline4N  40033  2polssN  40171  lhpmatb  40287  4atex  40332  trlatn0  40428  cdlemf2  40818  dialss  41302  diaglbN  41311  diaintclN  41314  dibglbN  41422  dibintclN  41423  dihlsscpre  41490  dihglblem5aN  41548  dihglblem2aN  41549  dihglblem4  41553  dihatexv  41594  dihjat1lem  41684  lcfl6  41756  mapdval2N  41886  aks4d1p8  42337  fldhmf1  42340  primrootscoprmpow  42349  primrootscoprbij2  42353  primrootspoweq0  42356  evl1gprodd  42367  hashscontpow  42372  aks6d1c2lem4  42377  idomnnzgmulnz  42383  deg1gprod  42390  sticksstones8  42403  sticksstones12a  42407  aks6d1c6lem3  42422  aks6d1c6lem5  42427  aks6d1c7  42434  aks5lem5a  42441  unitscyglem2  42446  sn-0tie0  42702  imacrhmcl  42765  fiabv  42787  evlselv  42826  fsuppind  42829  prjspertr  42844  prjspreln0  42848  prjspner1  42865  elrfi  42932  eldioph2  43000  diophin  43010  irrapxlem2  43061  irrapxlem3  43062  irrapxlem4  43063  irrapxlem5  43064  pell1234qrne0  43091  pell1234qrreccl  43092  pell1234qrmulcl  43093  pell14qrgt0  43097  pell14qrdich  43107  pell1qrge1  43108  pellfundex  43124  congabseq  43212  jm2.27b  43244  jm2.27  43246  fnwe2lem2  43289  kelac1  43301  lnrfg  43357  hbt  43368  omabs2  43570  nadd1suc  43630  rfovcnvf1od  44241  ntrneiiso  44328  ntrneikb  44331  ntrneixb  44332  ntrneik3  44333  ntrneix3  44334  ntrneik13  44335  ntrneix13  44336  cvgdvgrat  44550  binomcxplemnotnn0  44593  sineq0ALT  45173  fnchoice  45270  disjf1  45423  supxrgere  45574  supxrgelem  45578  supxrge  45579  suplesup  45580  xralrple2  45595  infxr  45607  infleinflem2  45611  infleinf  45612  uzub  45671  mccl  45840  limcrecl  45871  lptioo2  45873  lptioo1  45874  lptre2pt  45880  addlimc  45888  limsupmnflem  45960  climxrre  45990  liminflimsupclim  46047  climxlim2lem  46085  xlimliminflimsup  46102  icccncfext  46127  cncfiooicclem1  46133  cncfiooiccre  46135  dvbdfbdioolem2  46169  ioodvbdlimc1lem1  46171  dvnxpaek  46182  dvmptfprodlem  46184  dvmptfprod  46185  dvnprodlem3  46188  itgioocnicc  46217  itgspltprt  46219  stoweidlem31  46271  fourierdlem39  46386  fourierdlem42  46389  fourierdlem48  46394  fourierdlem49  46395  fourierdlem50  46396  fourierdlem51  46397  fourierdlem64  46410  fourierdlem65  46411  fourierdlem74  46420  fourierdlem75  46421  fourierdlem81  46427  fourierdlem82  46428  fourierdlem101  46447  etransclem23  46497  etransclem27  46501  etransclem32  46506  etransclem33  46507  etransclem35  46509  etransclem38  46512  sge0tsms  46620  sge0cl  46621  sge0f1o  46622  sge0split  46649  sge0rpcpnf  46661  sge0seq  46686  nnfoctbdjlem  46695  iundjiun  46700  meaiuninc3v  46724  meaiininclem  46726  omeiunltfirp  46759  carageniuncllem2  46762  carageniuncl  46763  hoidmv1lelem1  46831  hoidmvlelem3  46837  hoidmvlelem5  46839  hoidmvle  46840  hoiqssbllem3  46864  iunhoiioolem  46915  pimdecfgtioo  46957  pimincfltioo  46958  preimageiingt  46960  preimaleiinlt  46961  smflimlem4  47014  chnerlem1  47122  iccpartigtl  47665  iccpartgt  47669  sprsymrelf1lem  47733  paireqne  47753  proththd  47856  requad2  47865  sbgoldbst  48020  bgoldbtbndlem4  48050  isuspgrim0lem  48135  isuspgrim0  48136  isuspgrimlem  48137  gricushgr  48159  grimedg  48177  grimgrtri  48191  isubgr3stgrlem7  48214  gpgusgralem  48298  pgn4cyclex  48368  2zrngmmgm  48494  cznrng  48503  rhmsubcALTVlem4  48526  srhmsubcALTV  48567  lincsum  48671  lcoss  48678  snlindsntor  48713  islindeps2  48725  line2x  48996  line2y  48997  itscnhlinecirc02p  49027  discsubc  49305  imasubc3  49397  uppropd  49422  swapfval  49503  fucofvalg  49559  fuco21  49577  precofvalALT  49609  2arwcat  49841  lanup  49882  ranup  49883