Theorem ad3antrrr 726

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 722	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 206  df-an 396

This theorem is referenced by:  ad4antr  728  ad4antlr  729  ad5ant12  752  simplll  771  fsnex  7135  fimaproj  7947  oaabs  8438  oaabs2  8439  omabs  8441  undom  8800  sbthlem8  8830  findcard3  8987  cantnfle  9359  cantnfp1  9369  cantnflem1c  9375  sornom  9964  enfin2i  10008  ttukeylem6  10201  fpwwe2lem12  10329  winalim2  10383  wuncval2  10434  negf1o  11335  xlemul1a  12951  difreicc  13145  flflp1  13455  faclbnd  13932  swrdswrd  14346  pfxccatin12lem3  14373  swrdccat3blem  14380  ello12  15153  elo12  15164  rlimclim1  15182  rlimcld2  15215  o1co  15223  o1of2  15250  o1rlimmul  15256  rlimsqzlem  15288  isercoll  15307  o1fsum  15453  supcvg  15496  dvds2ln  15926  lcmgcdlem  16239  cncongr2  16301  isprm5  16340  prmdvdsncoprmbd  16359  pcadd  16518  vdwlem2  16611  vdwlem11  16620  sbcie3s  16791  prdsval  17083  mreexexlem4d  17273  isacs2  17279  catcocl  17311  catass  17312  subccocl  17476  fullsubc  17481  funcco  17502  fullpropd  17552  ffthiso  17561  isnat  17579  natpropd  17610  fucpropd  17611  xpcval  17810  evlf2  17852  curfpropd  17867  curfuncf  17872  uncfcurf  17873  hofcl  17893  hofpropd  17901  yonffthlem  17916  isacs3lem  18175  acsfiindd  18186  gsumpropd2lem  18278  resmhm2b  18376  mhmid  18611  mhmmnd  18612  ghmgrp  18614  conjnmzb  18784  pgpfi  19125  sylow3lem2  19148  efgredlem  19268  frgpnabllem1  19389  dprdfcntz  19533  ablfac1b  19588  pgpfac1lem3  19595  pgpfac1lem5  19597  pgpfaclem3  19601  ringinvnzdiv  19747  cntzsdrg  19985  islmhm2  20215  lspsneleq  20292  znunit  20683  psgndiflemB  20717  uvcff  20908  uvcf1  20909  lindfmm  20944  psrval  21028  psrass1  21084  resspsrmul  21096  mplbas2  21153  mhpmulcl  21249  coe1tmmul  21358  gsummoncoe1  21385  dmatsubcl  21555  scmatscm  21570  smatvscl  21581  marrepval  21619  mdetdiaglem  21655  mdetunilem8  21676  mdetunilem9  21677  pmatcoe1fsupp  21758  decpmatmulsumfsupp  21830  pmatcollpw2lem  21834  mp2pm2mplem4  21866  pm2mpmhmlem1  21875  pm2mpmhmlem2  21876  pm2mp  21882  fvmptnn04if  21906  cpmadugsumfi  21934  cpmidg2sum  21937  cpmadumatpoly  21940  cayhamlem4  21945  neiptoptop  22190  neitr  22239  ordtrest2lem  22262  cnpnei  22323  iscncl  22328  cncls  22333  cnntr  22334  cncnp  22339  lmcnp  22363  isreg2  22436  hauscmplem  22465  cmpfi  22467  1stcfb  22504  1stcrest  22512  2ndcctbss  22514  2ndcomap  22517  islly2  22543  cldllycmp  22554  lly1stc  22555  locfincmp  22585  llycmpkgen2  22609  1stckgenlem  22612  kgencn2  22616  kgencn3  22617  ptbasfi  22640  ptpjopn  22671  txdis1cn  22694  txlly  22695  txnlly  22696  txtube  22699  txcmplem2  22701  tx1stc  22709  txkgen  22711  xkopt  22714  xkoco2cn  22717  xkococnlem  22718  xkococn  22719  xkoinjcn  22746  tgqtop  22771  regr1lem  22798  kqreglem1  22800  nrmhmph  22853  rnelfmlem  23011  rnelfm  23012  fmfnfmlem4  23016  fmfnfm  23017  ufldom  23021  flimopn  23034  hauspwpwf1  23046  fclsopn  23073  fclsnei  23078  fclsrest  23083  alexsublem  23103  alexsubALTlem3  23108  ptcmplem2  23112  ptcmplem3  23113  cnextfun  23123  cnextcn  23126  symgtgp  23165  tgpt0  23178  qustgpopn  23179  tsmsxplem1  23212  trust  23289  utopsnneiplem  23307  utop3cls  23311  utopreg  23312  isucn2  23339  cstucnd  23344  ucncn  23345  fmucnd  23352  cfilufg  23353  neipcfilu  23356  met2ndci  23584  prdsxmslem2  23591  metustid  23616  metustexhalf  23618  metust  23620  psmetutop  23629  nmoleub  23801  reconnlem2  23896  xrge0tsms  23903  cncfco  23976  lebnumlem3  24032  lebnum  24033  nmoleub2lem2  24185  nmoleub3  24188  iscfil2  24335  iscau4  24348  iscmet3lem2  24361  equivcfil  24368  equivcau  24369  caubl  24377  rrxdstprj1  24478  ovolshftlem2  24579  ovolicc2lem4  24589  uniioombl  24658  i1fmulclem  24772  mbfi1fseqlem6  24790  itg2const2  24811  itg2split  24819  bddiblnc  24911  ellimc2  24946  ellimc3  24948  limcflf  24950  dvmptfsum  25044  dvferm1  25054  dvferm2  25056  dvlip2  25064  c1lip1  25066  lhop1  25083  ftc1a  25106  ply1divex  25206  plyeq0lem  25276  plymullem1  25280  coemullem  25316  coemulc  25321  ulmshftlem  25453  ulmcaulem  25458  ulmbdd  25462  ulmcn  25463  ulmdvlem3  25466  mtestbdd  25469  pserulm  25486  pserdvlem2  25492  abelthlem8  25503  xrlimcnp  26023  jensen  26043  lgamucov  26092  logfac2  26270  dchrelbas3  26291  dchrpt  26320  gausslemma2dlem1a  26418  lgsquad3  26440  2sqb  26485  rpvmasumlem  26540  dchrisumlem1  26542  dchrisumlem3  26544  dchrmusum2  26547  dchrvmasumlem2  26551  dchrisum0flblem1  26561  dchrisum0lem1b  26568  dchrisum0lem1  26569  dchrisum0  26573  mulog2sumlem2  26588  pntlem3  26662  ostth3  26691  istrkgcb  26721  tgbtwndiff  26771  iscgrglt  26779  tgcgrxfr  26783  motcgrg  26809  lnext  26832  tgbtwnconn1  26840  tgbtwnconn3  26842  legval  26849  legtrid  26856  legso  26864  hlcgreu  26883  tglnne  26893  tglineeltr  26896  tglnne0  26905  colline  26914  tglowdim2l  26915  tglowdim2ln  26916  mirreu3  26919  mirbtwnhl  26945  krippenlem  26955  midexlem  26957  perpcom  26978  footexALT  26983  footex  26986  colperpexlem3  26997  colperpex  26998  opphllem  27000  midex  27002  oppne3  27008  opptgdim2  27010  oppnid  27011  opphllem2  27013  opphllem5  27016  opphllem6  27017  oppperpex  27018  outpasch  27020  hlpasch  27021  lnopp2hpgb  27028  hpgerlem  27030  colopp  27034  colhp  27035  lmieu  27049  lnperpex  27068  trgcopy  27069  trgcopyeulem  27070  iscgra1  27075  cgrane1  27077  cgrane2  27078  cgrane3  27079  cgrane4  27080  cgrahl1  27081  cgrahl2  27082  cgracgr  27083  cgraswap  27085  cgracom  27087  cgratr  27088  flatcgra  27089  cgrabtwn  27091  cgrahl  27092  sacgr  27096  acopyeu  27099  cgrg3col4  27118  tgasa1  27123  f1otrg  27136  f1otrge  27137  axeuclidlem  27233  axcontlem2  27236  umgrvad2edg  27483  usgredg2vlem2  27496  pthdepisspth  28004  clwwlkccatlem  28254  clwlkclwwlklem2  28265  3cycld  28443  eupth2lems  28503  eucrctshift  28508  frgr3vlem2  28539  n4cyclfrgr  28556  numclwwlk1lem2f1  28622  numclwwlk2lem1  28641  ubthlem3  29135  chirredlem1  30653  chirredlem3  30655  cdj1i  30696  fnpreimac  30910  xrge0infss  30985  nn0xmulclb  30996  hashxpe  31029  ccatf1  31125  swrdf1  31130  dfmgc2lem  31175  mgcf1o  31183  gsumhashmul  31218  xrge0tsmsd  31219  omndmul2  31240  gsumle  31252  psgnfzto1stlem  31269  cycpmco2  31302  cycpmrn  31312  tocyccntz  31313  cycpmconjslem2  31324  cyc3conja  31326  submarchi  31342  suborng  31416  isarchiofld  31418  imaslmod  31455  znfermltl  31464  lindfpropd  31478  nsgqusf1olem1  31500  rhmpreimaidl  31505  elrspunidl  31508  rhmimaidl  31511  qsidomlem1  31530  mxidlprm  31542  lindsunlem  31607  lindsun  31608  lbsdiflsp0  31609  dimkerim  31610  fedgmul  31614  extdg1id  31640  smatrcl  31648  1smat1  31656  submateq  31661  mdetpmtr1  31675  madjusmdetlem2  31680  locfinreflem  31692  cmppcmp  31710  rhmpreimacn  31737  ordtrest2NEWlem  31774  ordtconnlem1  31776  lmdvg  31805  esumpcvgval  31946  esum2d  31961  sigapildsys  32030  ldgenpisyslem1  32031  fiunelros  32042  volmeas  32099  imambfm  32129  omssubadd  32167  carsggect  32185  carsgclctunlem3  32187  sgnmul  32409  signsply0  32430  signstres  32454  actfunsnf1o  32484  actfunsnrndisj  32485  reprsuc  32495  reprinfz1  32502  breprexplema  32510  breprexplemc  32512  breprexp  32513  breprexpnat  32514  circlemeth  32520  hgt750lemb  32536  tgoldbachgtd  32542  erdszelem8  33060  pconnconn  33093  cvmlift2lem12  33176  cvmlift3lem5  33185  cvmlift3lem7  33187  cvmlift3lem8  33188  mrsubrn  33375  msrval  33400  msubff1  33418  frxp3  33724  slerec  33940  cofcutr  34019  btwnconn1lem13  34328  elicc3  34433  neibastop2lem  34476  unbdqndv2  34618  irrdifflemf  35423  ltflcei  35692  lindsenlbs  35699  matunitlindflem1  35700  matunitlindflem2  35701  poimirlem4  35708  poimirlem13  35717  poimirlem14  35718  poimirlem22  35726  poimirlem26  35730  poimirlem27  35731  heicant  35739  mblfinlem2  35742  mblfinlem3  35743  mblfinlem4  35744  cnambfre  35752  itg2addnclem  35755  itg2addnclem2  35756  itg2gt0cn  35759  ftc1cnnc  35776  ftc1anclem5  35781  ftc1anclem7  35783  ftc1anc  35785  equivtotbnd  35863  isbndx  35867  ssbnd  35873  heibor1lem  35894  rrncmslem  35917  islshpat  36958  lfl1dim  37062  lfl1dim2N  37063  lkrpssN  37104  glbconN  37318  hlhgt2  37330  3dim2  37409  3dim3  37410  islln3  37451  islvol5  37520  2lplnja  37560  dalem19  37623  isline4N  37718  2polssN  37856  lhpmatb  37972  4atex  38017  trlatn0  38113  cdlemf2  38503  dialss  38987  diaglbN  38996  diaintclN  38999  dibglbN  39107  dibintclN  39108  dihlsscpre  39175  dihglblem5aN  39233  dihglblem2aN  39234  dihglblem4  39238  dihatexv  39279  dihjat1lem  39369  lcfl6  39441  mapdval2N  39571  aks4d1p8  40023  sticksstones8  40037  sticksstones12a  40041  fsuppind  40202  sn-0tie0  40342  prjspertr  40365  prjspreln0  40369  prjspner1  40384  elrfi  40432  eldioph2  40500  diophin  40510  irrapxlem2  40561  irrapxlem3  40562  irrapxlem4  40563  irrapxlem5  40564  pell1234qrne0  40591  pell1234qrreccl  40592  pell1234qrmulcl  40593  pell14qrgt0  40597  pell14qrdich  40607  pell1qrge1  40608  pellfundex  40624  congabseq  40712  jm2.27b  40744  jm2.27  40746  fnwe2lem2  40792  kelac1  40804  lnrfg  40860  hbt  40871  rfovcnvf1od  41501  ntrneiiso  41590  ntrneikb  41593  ntrneixb  41594  ntrneik3  41595  ntrneix3  41596  ntrneik13  41597  ntrneix13  41598  cvgdvgrat  41820  binomcxplemnotnn0  41863  sineq0ALT  42446  disjf1  42609  supxrgere  42762  supxrgelem  42766  supxrge  42767  suplesup  42768  xralrple2  42783  infxr  42796  infleinflem2  42800  infleinf  42801  uzub  42861  mccl  43029  limcrecl  43060  lptioo2  43062  lptioo1  43063  lptre2pt  43071  addlimc  43079  limsupmnflem  43151  climxrre  43181  liminflimsupclim  43238  climxlim2lem  43276  xlimliminflimsup  43293  icccncfext  43318  cncfiooicclem1  43324  cncfiooiccre  43326  dvbdfbdioolem2  43360  ioodvbdlimc1lem1  43362  dvnxpaek  43373  dvmptfprodlem  43375  dvmptfprod  43376  dvnprodlem3  43379  itgioocnicc  43408  itgspltprt  43410  stoweidlem31  43462  fourierdlem39  43577  fourierdlem42  43580  fourierdlem48  43585  fourierdlem49  43586  fourierdlem50  43587  fourierdlem51  43588  fourierdlem64  43601  fourierdlem65  43602  fourierdlem74  43611  fourierdlem75  43612  fourierdlem81  43618  fourierdlem82  43619  fourierdlem101  43638  etransclem23  43688  etransclem27  43692  etransclem32  43697  etransclem33  43698  etransclem35  43700  etransclem38  43703  sge0tsms  43808  sge0cl  43809  sge0f1o  43810  sge0split  43837  sge0rpcpnf  43849  sge0seq  43874  nnfoctbdjlem  43883  iundjiun  43888  meaiuninc3v  43912  meaiininclem  43914  omeiunltfirp  43947  carageniuncllem2  43950  carageniuncl  43951  hoidmv1lelem1  44019  hoidmvlelem3  44025  hoidmvlelem5  44027  hoidmvle  44028  hoiqssbllem3  44052  iunhoiioolem  44103  pimdecfgtioo  44141  pimincfltioo  44142  preimageiingt  44144  preimaleiinlt  44145  smflimlem4  44196  iccpartigtl  44763  iccpartgt  44767  sprsymrelf1lem  44831  paireqne  44851  proththd  44954  requad2  44963  sbgoldbst  45118  bgoldbtbndlem4  45148  isomushgr  45166  isomuspgrlem2d  45171  resmgmhm2b  45242  2zrngmmgm  45392  cznrng  45401  rnghmsubcsetclem2  45422  rhmsubcsetclem2  45468  srhmsubc  45522  rhmsubclem4  45535  srhmsubcALTV  45540  rhmsubcALTVlem4  45553  lincsum  45658  lcoss  45665  snlindsntor  45700  islindeps2  45712  line2x  45988  line2y  45989  itscnhlinecirc02p  46019