Theorem ad3antrrr 766

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 481	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad2antrr 762	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:  ad4antr  768  ad5ant12  1300  fsnex  6538  oaabs  7724  oaabs2  7725  omabs  7727  undom  8048  sbthlem8  8077  findcard3  8203  cantnfle  8568  cantnfp1  8578  cantnflem1c  8584  sornom  9099  enfin2i  9143  ttukeylem6  9336  fpwwe2lem13  9464  fpwwe2  9465  winalim2  9518  wuncval2  9569  negf1o  10460  xlemul1a  12118  difreicc  12304  flflp1  12608  faclbnd  13077  swrdswrd  13460  swrdccatin12lem3  13490  swrdccat3blem  13495  ello12  14247  lo1bdd2  14255  elo12  14258  rlimclim1  14276  rlimcld2  14309  o1co  14317  o1of2  14343  o1rlimmul  14349  rlimsqzlem  14379  isercoll  14398  o1fsum  14545  supcvg  14588  dvds2ln  15014  lcmgcdlem  15319  cncongr2  15382  isprm5  15419  pcadd  15593  vdwlem2  15686  vdwlem11  15695  sbcie3s  15917  prdsval  16115  mreexexlem4d  16307  isacs2  16314  catcocl  16346  catass  16347  subccocl  16505  fullsubc  16510  funcco  16531  funcpropd  16560  fullpropd  16580  ffthiso  16589  isnat  16607  natpropd  16636  fucpropd  16637  xpcval  16817  evlf2  16858  curfpropd  16873  curfuncf  16878  uncfcurf  16879  curf2ndf  16887  hofcl  16899  hofpropd  16907  yonffthlem  16922  isacs3lem  17166  acsfiindd  17177  gsumpropd2lem  17273  resmhm2b  17361  mhmid  17536  mhmmnd  17537  ghmgrp  17539  conjnmzb  17695  pgpfi  18020  sylow3lem2  18043  efgredlem  18160  frgpnabllem1  18276  dprdfcntz  18414  ablfac1b  18469  pgpfac1lem3  18476  pgpfac1lem5  18478  pgpfaclem3  18482  ringinvnzdiv  18593  islmhm2  19038  lspsneleq  19115  psrval  19362  psrass1  19405  resspsrmul  19417  mplbas2  19470  coe1tmmul  19647  gsummoncoe1  19674  znunit  19912  psgndiflemB  19946  uvcff  20130  uvcf1  20131  lindfmm  20166  dmatsubcl  20304  scmatscm  20319  smatvscl  20330  marrepval  20368  mdetdiaglem  20404  mdetunilem8  20425  mdetunilem9  20426  pmatcoe1fsupp  20506  decpmatmulsumfsupp  20578  pmatcollpw2lem  20582  mp2pm2mplem4  20614  pm2mpmhmlem1  20623  pm2mpmhmlem2  20624  pm2mp  20630  fvmptnn04if  20654  cpmadugsumfi  20682  cpmidg2sum  20685  cpmadumatpoly  20688  cayhamlem4  20693  neiptoptop  20935  neitr  20984  ordtrest2lem  21007  cnpnei  21068  iscncl  21073  cncls  21078  cnntr  21079  cncnp  21084  lmcnp  21108  isreg2  21181  hauscmplem  21209  cmpfi  21211  1stcfb  21248  1stcrest  21256  2ndcctbss  21258  2ndcomap  21261  islly2  21287  cldllycmp  21298  lly1stc  21299  locfincmp  21329  llycmpkgen2  21353  1stckgenlem  21356  kgencn2  21360  kgencn3  21361  ptbasfi  21384  ptpjopn  21415  txdis1cn  21438  txlly  21439  txnlly  21440  txtube  21443  txcmplem2  21445  tx1stc  21453  txkgen  21455  xkopt  21458  xkoco2cn  21461  xkococnlem  21462  xkococn  21463  xkoinjcn  21490  tgqtop  21515  regr1lem  21542  kqreglem1  21544  nrmhmph  21597  rnelfmlem  21756  rnelfm  21757  fmfnfmlem4  21761  fmfnfm  21762  ufldom  21766  flimopn  21779  hauspwpwf1  21791  fclsopn  21818  fclsnei  21823  fclsrest  21828  alexsublem  21848  alexsubALTlem3  21853  ptcmplem2  21857  ptcmplem3  21858  cnextfun  21868  cnextcn  21871  symgtgp  21905  tgpt0  21922  qustgpopn  21923  tsmsxplem1  21956  trust  22033  utopsnneiplem  22051  utop3cls  22055  utopreg  22056  isucn2  22083  cstucnd  22088  ucncn  22089  fmucnd  22096  cfilufg  22097  neipcfilu  22100  met2ndci  22327  prdsxmslem2  22334  metcnp3  22345  metustid  22359  metustexhalf  22361  metust  22363  psmetutop  22372  nmoleub  22535  reconnlem2  22630  xrge0tsms  22637  cncfco  22710  lebnumlem3  22762  lebnum  22763  nmoleub2lem2  22916  nmoleub3  22919  iscfil2  23064  iscau4  23077  iscmet3lem2  23090  equivcfil  23097  equivcau  23098  caubl  23106  rrxdstprj1  23192  ovolshftlem2  23278  ovolicc2lem4  23288  uniioombl  23357  i1fmulclem  23469  mbfi1fseqlem6  23487  itg2const2  23508  itg2split  23516  ellimc2  23641  ellimc3  23643  limcflf  23645  dvmptfsum  23738  dvferm1  23748  dvferm2  23750  dvlip2  23758  c1lip1  23760  lhop1  23777  ftc1a  23800  ply1divex  23896  plyeq0lem  23966  plymullem1  23970  coemullem  24006  coemulc  24011  ulmshftlem  24143  ulmcaulem  24148  ulmbdd  24152  ulmcn  24153  ulmdvlem3  24156  mtestbdd  24159  pserulm  24176  pserdvlem2  24182  abelthlem8  24193  xrlimcnp  24695  jensen  24715  lgamucov  24764  logfac2  24942  dchrelbas3  24963  dchrpt  24992  gausslemma2dlem1a  25090  lgsquad3  25112  2sqb  25157  rpvmasumlem  25176  dchrisumlem1  25178  dchrisumlem3  25180  dchrmusum2  25183  dchrvmasumlem2  25187  dchrisum0flblem1  25197  dchrisum0lem1b  25204  dchrisum0lem1  25205  dchrisum0  25209  mulog2sumlem2  25224  pntlem3  25298  ostth3  25327  istrkgcb  25355  tgbtwndiff  25401  iscgrglt  25409  tgcgrxfr  25413  motcgrg  25439  lnext  25462  tgbtwnconn1  25470  tgbtwnconn3  25472  legval  25479  legtrid  25486  legso  25494  hlcgreu  25513  tglnne  25523  tglineeltr  25526  tglnne0  25535  colline  25544  tglowdim2l  25545  tglowdim2ln  25546  mirreu3  25549  mirbtwnhl  25575  krippenlem  25585  midexlem  25587  perpcom  25608  perpneq  25609  footex  25613  colperpexlem3  25624  colperpex  25625  opphllem  25627  midex  25629  oppne3  25635  opptgdim2  25637  oppnid  25638  opphllem2  25640  opphllem5  25643  opphllem6  25644  oppperpex  25645  outpasch  25647  hlpasch  25648  lnopp2hpgb  25655  hpgerlem  25657  colopp  25661  colhp  25662  lmieu  25676  lnperpex  25695  trgcopy  25696  trgcopyeulem  25697  iscgra1  25702  cgrane1  25704  cgrane2  25705  cgrane3  25706  cgrane4  25707  cgrahl1  25708  cgrahl2  25709  cgracgr  25710  cgraswap  25712  cgracom  25714  cgratr  25715  cgrabtwn  25717  cgrahl  25718  sacgr  25722  acopyeu  25725  cgrg3col4  25734  tgasa1  25739  f1otrg  25751  f1otrge  25752  axeuclidlem  25842  axcontlem2  25845  umgrvad2edg  26105  usgredg2vlem2  26118  nbgr2vtx1edg  26246  nbuhgr2vtx1edgb  26248  pthdepisspth  26631  wwlksnwwlksnon  26810  clwlkclwwlklem2  26901  wwlksext2clwwlk  26924  clwlksf1clwwlk  26969  3cycld  27038  eupth2lems  27098  eucrctshift  27103  frgr3vlem2  27138  n4cyclfrgr  27155  numclwwlk2lem1  27235  ubthlem3  27728  chirredlem1  29249  chirredlem3  29251  cdj1i  29292  xrge0infss  29525  omndmul2  29712  submarchi  29740  gsumle  29779  xrge0tsmsd  29785  suborng  29815  isarchiofld  29817  psgnfzto1stlem  29850  fzto1st1  29852  smatrcl  29862  1smat1  29870  submateq  29875  mdetpmtr1  29889  madjusmdetlem2  29894  fimaproj  29900  locfinreflem  29907  cmppcmp  29925  ordtrest2NEWlem  29968  ordtconnlem1  29970  lmdvg  29999  esumpcvgval  30140  esum2d  30155  sigapildsys  30225  ldgenpisyslem1  30226  fiunelros  30237  volmeas  30294  imambfm  30324  omssubadd  30362  carsggect  30380  carsgclctunlem3  30382  sgnmul  30604  signsply0  30628  signstres  30652  actfunsnf1o  30682  actfunsnrndisj  30683  reprsuc  30693  reprinfz1  30700  breprexplema  30708  breprexplemc  30710  breprexp  30711  breprexpnat  30712  circlemeth  30718  hgt750lemb  30734  tgoldbachgtd  30740  erdszelem8  31180  pconnconn  31213  cvmlift2lem12  31296  cvmlift3lem5  31305  cvmlift3lem7  31307  cvmlift3lem8  31308  mrsubrn  31410  msrval  31435  msubff1  31453  slerec  31923  btwnconn1lem13  32206  elicc3  32311  neibastop2lem  32355  unbdqndv2  32502  ltflcei  33397  lindsenlbs  33404  matunitlindflem1  33405  matunitlindflem2  33406  poimirlem4  33413  poimirlem13  33422  poimirlem14  33423  poimirlem22  33431  poimirlem26  33435  poimirlem27  33436  heicant  33444  mblfinlem2  33447  mblfinlem3  33448  mblfinlem4  33449  cnambfre  33458  itg2addnclem  33461  itg2addnclem2  33462  itg2gt0cn  33465  bddiblnc  33480  ftc1cnnc  33484  ftc1anclem5  33489  ftc1anclem7  33491  ftc1anc  33493  equivtotbnd  33577  isbndx  33581  ssbnd  33587  heibor1lem  33608  rrncmslem  33631  islshpat  34304  lfl1dim  34408  lfl1dim2N  34409  lkrpssN  34450  glbconN  34663  hlhgt2  34675  3dim2  34754  3dim3  34755  islln3  34796  islvol5  34865  2lplnja  34905  dalem19  34968  isline4N  35063  2polssN  35201  lhpmatb  35317  4atex  35362  trlatn0  35459  cdlemf2  35850  dialss  36335  diaglbN  36344  diaintclN  36347  dibglbN  36455  dibintclN  36456  dihlsscpre  36523  dihglblem5aN  36581  dihglblem2aN  36582  dihglblem4  36586  dihatexv  36627  dihjat1lem  36717  lcfl6  36789  mapdval2N  36919  elrfi  37257  eldioph2  37325  diophin  37336  irrapxlem2  37387  irrapxlem3  37388  irrapxlem4  37389  irrapxlem5  37390  pell1234qrne0  37417  pell1234qrreccl  37418  pell1234qrmulcl  37419  pell14qrgt0  37423  pell14qrdich  37433  pell1qrge1  37434  pellfundex  37450  congabseq  37541  jm2.27b  37573  jm2.27  37575  fnwe2lem2  37621  kelac1  37633  lnrfg  37689  hbt  37700  cntzsdrg  37772  rfovcnvf1od  38298  ntrneiiso  38389  ntrneikb  38392  ntrneixb  38393  ntrneik3  38394  ntrneix3  38395  ntrneik13  38396  ntrneix13  38397  cvgdvgrat  38512  binomcxplemnotnn0  38555  sineq0ALT  39173  disjf1  39369  supxrgere  39549  supxrgelem  39553  supxrge  39554  suplesup  39555  xralrple2  39570  infxr  39583  infleinflem2  39587  infleinf  39588  uzub  39658  mccl  39830  limcrecl  39861  lptioo2  39863  lptioo1  39864  lptre2pt  39872  addlimc  39880  limsupmnflem  39952  climxrre  39982  liminflimsupclim  40039  climxlim2lem  40071  icccncfext  40100  cncfiooicclem1  40106  cncfiooiccre  40108  dvbdfbdioolem2  40144  ioodvbdlimc1lem1  40146  dvnxpaek  40157  dvmptfprodlem  40159  dvmptfprod  40160  dvnprodlem3  40163  itgioocnicc  40193  itgspltprt  40195  stoweidlem31  40248  fourierdlem39  40363  fourierdlem42  40366  fourierdlem48  40371  fourierdlem49  40372  fourierdlem50  40373  fourierdlem51  40374  fourierdlem64  40387  fourierdlem65  40388  fourierdlem74  40397  fourierdlem75  40398  fourierdlem81  40404  fourierdlem82  40405  fourierdlem101  40424  etransclem23  40474  etransclem27  40478  etransclem32  40483  etransclem33  40484  etransclem35  40486  etransclem38  40489  sge0tsms  40597  sge0cl  40598  sge0f1o  40599  sge0split  40626  sge0rpcpnf  40638  sge0seq  40663  nnfoctbdjlem  40672  iundjiun  40677  meaiininclem  40700  omeiunltfirp  40733  carageniuncllem2  40736  carageniuncl  40737  hoidmv1lelem1  40805  hoidmvlelem3  40811  hoidmvlelem5  40813  hoidmvle  40814  hoiqssbllem3  40838  iunhoiioolem  40889  pimdecfgtioo  40927  pimincfltioo  40928  preimageiingt  40930  preimaleiinlt  40931  smflimlem4  40982  iccpartigtl  41359  iccpartgt  41363  proththd  41531  sbgoldbst  41666  bgoldbtbndlem4  41696  sprsymrelf1lem  41741  resmgmhm2b  41800  2zrngmmgm  41946  cznrng  41955  rnghmsubcsetclem2  41976  rhmsubcsetclem2  42022  srhmsubc  42076  rhmsubclem4  42089  srhmsubcALTV  42094  rhmsubcALTVlem4  42107  lincsum  42218  lcoss  42225  snlindsntor  42260  islindeps2  42272