Theorem ad3antrrr 762

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 758	1 ⊢ ((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  ad4antr  764  ad5ant12  1292  fsnex  6438  oaabs  7611  oaabs2  7612  omabs  7614  undom  7933  sbthlem8  7962  findcard3  8088  cantnfle  8451  cantnfp1  8461  cantnflem1c  8467  sornom  8982  enfin2i  9026  ttukeylem6  9219  fpwwe2lem13  9343  fpwwe2  9344  winalim2  9397  wuncval2  9448  negf1o  10339  xlemul1a  11990  difreicc  12175  flflp1  12470  faclbnd  12939  swrdswrd  13312  swrdccatin12lem3  13341  swrdccat3blem  13346  ello12  14095  lo1bdd2  14103  elo12  14106  rlimclim1  14124  rlimcld2  14157  o1co  14165  o1of2  14191  o1rlimmul  14197  rlimsqzlem  14227  isercoll  14246  o1fsum  14386  supcvg  14427  dvds2ln  14852  lcmgcdlem  15157  cncongr2  15220  isprm5  15257  pcadd  15431  vdwlem2  15524  vdwlem11  15533  sbcie3s  15745  prdsval  15938  mreexexlem4d  16130  isacs2  16137  catcocl  16169  catass  16170  subccocl  16328  fullsubc  16333  funcco  16354  funcpropd  16383  fullpropd  16403  ffthiso  16412  isnat  16430  natpropd  16459  fucpropd  16460  xpcval  16640  evlf2  16681  curfpropd  16696  curfuncf  16701  uncfcurf  16702  curf2ndf  16710  hofcl  16722  hofpropd  16730  yonffthlem  16745  isacs3lem  16989  acsfiindd  17000  gsumpropd2lem  17096  resmhm2b  17184  mhmid  17359  mhmmnd  17360  ghmgrp  17362  conjnmzb  17518  pgpfi  17843  sylow3lem2  17866  efgredlem  17983  frgpnabllem1  18099  dprdfcntz  18237  ablfac1b  18292  pgpfac1lem3  18299  pgpfac1lem5  18301  pgpfaclem3  18305  ringinvnzdiv  18416  islmhm2  18859  lspsneleq  18936  psrval  19183  psrass1  19226  resspsrmul  19238  mplbas2  19291  coe1tmmul  19468  gsummoncoe1  19495  znunit  19731  psgndiflemB  19765  uvcff  19949  uvcf1  19950  lindfmm  19985  dmatsubcl  20123  scmatscm  20138  smatvscl  20149  marrepval  20187  mdetdiaglem  20223  mdetunilem8  20244  mdetunilem9  20245  pmatcoe1fsupp  20325  decpmatmulsumfsupp  20397  pmatcollpw2lem  20401  mp2pm2mplem4  20433  pm2mpmhmlem1  20442  pm2mpmhmlem2  20443  pm2mp  20449  fvmptnn04if  20473  cpmadugsumfi  20501  cpmidg2sum  20504  cpmadumatpoly  20507  cayhamlem4  20512  neiptoptop  20745  neitr  20794  ordtrest2lem  20817  cnpnei  20878  iscncl  20883  cncls  20888  cnntr  20889  cncnp  20894  lmcnp  20918  isreg2  20991  hauscmplem  21019  cmpfi  21021  1stcfb  21058  1stcrest  21066  2ndcctbss  21068  2ndcomap  21071  islly2  21097  cldllycmp  21108  lly1stc  21109  locfincmp  21139  llycmpkgen2  21163  1stckgenlem  21166  kgencn2  21170  kgencn3  21171  ptbasfi  21194  ptpjopn  21225  txdis1cn  21248  txlly  21249  txnlly  21250  txtube  21253  txcmplem2  21255  tx1stc  21263  txkgen  21265  xkopt  21268  xkoco2cn  21271  xkococnlem  21272  xkococn  21273  xkoinjcn  21300  tgqtop  21325  regr1lem  21352  kqreglem1  21354  nrmhmph  21407  rnelfmlem  21566  rnelfm  21567  fmfnfmlem4  21571  fmfnfm  21572  ufldom  21576  flimopn  21589  hauspwpwf1  21601  fclsopn  21628  fclsnei  21633  fclsrest  21638  alexsublem  21658  alexsubALTlem3  21663  ptcmplem2  21667  ptcmplem3  21668  cnextfun  21678  cnextcn  21681  symgtgp  21715  tgpt0  21732  qustgpopn  21733  tsmsxplem1  21766  trust  21843  utopsnneiplem  21861  utop3cls  21865  utopreg  21866  isucn2  21893  cstucnd  21898  ucncn  21899  fmucnd  21906  cfilufg  21907  neipcfilu  21910  met2ndci  22137  prdsxmslem2  22144  metcnp3  22155  metustid  22169  metustexhalf  22171  metust  22173  psmetutop  22182  nmoleub  22345  reconnlem2  22438  xrge0tsms  22445  cncfco  22518  lebnumlem3  22570  lebnum  22571  nmoleub2lem2  22724  nmoleub3  22727  iscfil2  22872  iscau4  22885  iscmet3lem2  22898  equivcfil  22905  equivcau  22906  caubl  22914  rrxdstprj1  23000  ovolshftlem2  23085  ovolicc2lem4  23095  uniioombl  23163  i1fmulclem  23275  mbfi1fseqlem6  23293  itg2const2  23314  itg2split  23322  ellimc2  23447  ellimc3  23449  limcflf  23451  dvmptfsum  23542  dvferm1  23552  dvferm2  23554  dvlip2  23562  c1lip1  23564  lhop1  23581  ftc1a  23604  ply1divex  23700  plyeq0lem  23770  plymullem1  23774  coemullem  23810  coemulc  23815  ulmshftlem  23947  ulmcaulem  23952  ulmbdd  23956  ulmcn  23957  ulmdvlem3  23960  mtestbdd  23963  pserulm  23980  pserdvlem2  23986  abelthlem8  23997  xrlimcnp  24495  jensen  24515  lgamucov  24564  logfac2  24742  dchrelbas3  24763  dchrpt  24792  gausslemma2dlem1a  24890  lgsquad3  24912  2sqb  24957  rpvmasumlem  24976  dchrisumlem1  24978  dchrisumlem3  24980  dchrmusum2  24983  dchrvmasumlem2  24987  dchrisum0flblem1  24997  dchrisum0lem1b  25004  dchrisum0lem1  25005  dchrisum0  25009  mulog2sumlem2  25024  pntlem3  25098  ostth3  25127  istrkgcb  25155  tgbtwndiff  25201  iscgrglt  25209  tgcgrxfr  25213  motcgrg  25239  lnext  25262  tgbtwnconn1  25270  tgbtwnconn3  25272  legval  25279  legtrid  25286  legso  25294  hlcgreu  25313  tglnne  25323  tglineeltr  25326  tglnne0  25335  colline  25344  tglowdim2l  25345  tglowdim2ln  25346  mirreu3  25349  mirbtwnhl  25375  krippenlem  25385  midexlem  25387  perpcom  25408  perpneq  25409  footex  25413  colperpexlem3  25424  colperpex  25425  opphllem  25427  midex  25429  oppne3  25435  opptgdim2  25437  oppnid  25438  opphllem2  25440  opphllem5  25443  opphllem6  25444  oppperpex  25445  outpasch  25447  hlpasch  25448  lnopp2hpgb  25455  hpgerlem  25457  colopp  25461  colhp  25462  lmieu  25476  lnperpex  25495  trgcopy  25496  trgcopyeulem  25497  iscgra1  25502  cgrane1  25504  cgrane2  25505  cgrane3  25506  cgrane4  25507  cgrahl1  25508  cgrahl2  25509  cgracgr  25510  cgraswap  25512  cgracom  25514  cgratr  25515  cgrabtwn  25517  cgrahl  25518  sacgr  25522  acopyeu  25525  cgrg3col4  25534  tgasa1  25539  f1otrg  25551  f1otrge  25552  axeuclidlem  25642  axcontlem2  25645  usgraidx2vlem2  25921  usgrares1  25939  nbgraf1olem5  25974  usgra2wlkspth  26149  constr3cycl  26189  clwlkisclwwlklem1  26315  wwlkext2clwwlk  26331  eupath2  26507  frisusgranb  26524  frgra2v  26526  frgra3vlem2  26528  2pthfrgrarn2  26537  2spotiundisj  26589  usg2spot2nb  26592  usgreghash2spotv  26593  numclwwlk2lem1  26629  ubthlem3  27112  chirredlem1  28633  chirredlem3  28635  cdj1i  28676  xrge0infss  28915  omndmul2  29043  submarchi  29071  gsumle  29110  xrge0tsmsd  29116  suborng  29146  isarchiofld  29148  psgnfzto1stlem  29181  fzto1st1  29183  smatrcl  29190  1smat1  29198  submateq  29203  mdetpmtr1  29217  madjusmdetlem2  29222  fimaproj  29228  locfinreflem  29235  cmppcmp  29253  ordtrest2NEWlem  29296  ordtconlem1  29298  lmdvg  29327  esumpcvgval  29467  esum2d  29482  sigapildsys  29552  ldgenpisyslem1  29553  fiunelros  29564  volmeas  29621  imambfm  29651  omssubadd  29689  carsggect  29707  carsgclctunlem3  29709  sgnmul  29931  signsply0  29954  signstres  29978  erdszelem8  30434  pconcon  30467  cvmlift2lem12  30550  cvmlift3lem5  30559  cvmlift3lem7  30561  cvmlift3lem8  30562  mrsubrn  30664  msrval  30689  msubff1  30707  nodenselem5  31084  btwnconn1lem13  31376  elicc3  31481  neibastop2lem  31525  unbdqndv2  31672  ltflcei  32567  lindsenlbs  32574  matunitlindflem1  32575  matunitlindflem2  32576  poimirlem4  32583  poimirlem13  32592  poimirlem14  32593  poimirlem22  32601  poimirlem26  32605  poimirlem27  32606  heicant  32614  mblfinlem2  32617  mblfinlem3  32618  mblfinlem4  32619  cnambfre  32628  itg2addnclem  32631  itg2addnclem2  32632  itg2gt0cn  32635  bddiblnc  32650  ftc1cnnc  32654  ftc1anclem5  32659  ftc1anclem7  32661  ftc1anc  32663  equivtotbnd  32747  isbndx  32751  ssbnd  32757  heibor1lem  32778  rrncmslem  32801  islshpat  33322  lfl1dim  33426  lfl1dim2N  33427  lkrpssN  33468  glbconN  33681  hlhgt2  33693  3dim2  33772  3dim3  33773  islln3  33814  islvol5  33883  2lplnja  33923  dalem19  33986  isline4N  34081  2polssN  34219  lhpmatb  34335  4atex  34380  trlatn0  34477  cdlemf2  34868  dialss  35353  diaglbN  35362  diaintclN  35365  dibglbN  35473  dibintclN  35474  dihlsscpre  35541  dihglblem5aN  35599  dihglblem2aN  35600  dihglblem4  35604  dihatexv  35645  dihjat1lem  35735  lcfl6  35807  mapdval2N  35937  elrfi  36275  eldioph2  36343  diophin  36354  irrapxlem2  36405  irrapxlem3  36406  irrapxlem4  36407  irrapxlem5  36408  pell1234qrne0  36435  pell1234qrreccl  36436  pell1234qrmulcl  36437  pell14qrgt0  36441  pell14qrdich  36451  pell1qrge1  36452  pellfundex  36468  congabseq  36559  jm2.27b  36591  jm2.27  36593  fnwe2lem2  36639  kelac1  36651  lnrfg  36708  hbt  36719  cntzsdrg  36791  rfovcnvf1od  37318  ntrneiiso  37409  ntrneikb  37412  ntrneixb  37413  ntrneik3  37414  ntrneix3  37415  ntrneik13  37416  ntrneix13  37417  cvgdvgrat  37534  binomcxplemnotnn0  37577  sineq0ALT  38195  disjf1  38364  supxrgere  38490  supxrgelem  38494  supxrge  38495  suplesup  38496  xralrple2  38511  infxr  38524  infleinflem2  38528  infleinf  38529  mccl  38665  limcrecl  38696  lptioo2  38698  lptioo1  38699  lptre2pt  38707  addlimc  38715  icccncfext  38773  cncfiooicclem1  38779  cncfiooiccre  38781  dvbdfbdioolem2  38819  ioodvbdlimc1lem1  38821  dvnxpaek  38832  dvmptfprodlem  38834  dvmptfprod  38835  dvnprodlem3  38838  itgioocnicc  38869  itgspltprt  38871  stoweidlem31  38924  fourierdlem39  39039  fourierdlem42  39042  fourierdlem48  39047  fourierdlem49  39048  fourierdlem50  39049  fourierdlem51  39050  fourierdlem64  39063  fourierdlem65  39064  fourierdlem74  39073  fourierdlem75  39074  fourierdlem81  39080  fourierdlem82  39081  fourierdlem101  39100  etransclem23  39150  etransclem27  39154  etransclem32  39159  etransclem33  39160  etransclem35  39162  etransclem38  39165  sge0tsms  39273  sge0cl  39274  sge0f1o  39275  sge0split  39302  sge0rpcpnf  39314  sge0seq  39339  nnfoctbdjlem  39348  iundjiun  39353  meaiininclem  39376  omeiunltfirp  39409  carageniuncllem2  39412  carageniuncl  39413  hoidmv1lelem1  39481  hoidmvlelem3  39487  hoidmvlelem5  39489  hoidmvle  39490  hoiqssbllem3  39514  iunhoiioolem  39566  pimdecfgtioo  39604  pimincfltioo  39605  preimageiingt  39607  preimaleiinlt  39608  smflimlem4  39660  iccpartigtl  39961  iccpartgt  39965  proththd  40069  bgoldbst  40200  bgoldbtbndlem4  40224  umgrvad2edg  40440  usgredg2vlem2  40453  nbgr2vtx1edg  40572  nbuhgr2vtx1edgb  40574  pthdepissPth  40941  wwlksnwwlksnon  41121  clwlkclwwlklem2  41209  wwlksext2clwwlk  41231  clwlksf1clwwlk  41276  3cycld  41345  eupth2lems  41406  eucrctshift  41411  frgr3vlem2  41444  n4cyclfrgr  41461  av-numclwwlk2lem1  41532  resmgmhm2b  41590  2zrngmmgm  41736  cznrng  41747  rnghmsubcsetclem2  41768  rhmsubcsetclem2  41814  srhmsubc  41868  rhmsubclem4  41881  srhmsubcALTV  41887  rhmsubcALTVlem4  41900  lincsum  42012  lcoss  42019  snlindsntor  42054  islindeps2  42066