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  7223  fimaproj  8071  frxp3  8087  oaabs  8569  oaabs2  8570  omabs  8572  cofon1  8593  sbthlem8  9014  cantnfle  9568  cantnfp1  9578  cantnflem1c  9584  sornom  10175  enfin2i  10219  ttukeylem6  10412  fpwwe2lem12  10540  fpwwe2  10541  winalim2  10594  wuncval2  10645  negf1o  11554  xlemul1a  13189  difreicc  13386  flflp1  13713  faclbnd  14199  swrdswrd  14614  swrdccatin1  14634  pfxccatin12lem3  14641  swrdccat3blem  14648  ello12  15425  lo1bdd2  15433  elo12  15436  rlimclim1  15454  rlimcld2  15487  o1co  15495  o1of2  15522  o1rlimmul  15528  rlimsqzlem  15558  isercoll  15577  o1fsum  15722  supcvg  15765  dvds2ln  16202  lcmgcdlem  16519  cncongr2  16581  isprm5  16620  prmdvdsncoprmbd  16640  pcadd  16803  vdwlem2  16896  vdwlem11  16905  sbcie3s  17075  prdsval  17361  mreexexlem4d  17555  isacs2  17561  catcocl  17593  catass  17594  subccocl  17754  fullsubc  17759  funcco  17780  funcpropd  17811  fullpropd  17831  ffthiso  17840  isnat  17859  natpropd  17888  fucpropd  17889  xpcval  18085  evlf2  18126  curfpropd  18141  curfuncf  18146  uncfcurf  18147  curf2ndf  18155  hofcl  18167  hofpropd  18175  yonffthlem  18190  isacs3lem  18450  acsfiindd  18461  chnind  18529  gsumpropd2lem  18589  resmgmhm2b  18623  resmhm2b  18732  mhmid  18978  mhmmnd  18979  ghmgrp  18981  conjnmzb  19167  ghmqusnsg  19196  ghmquskerlem3  19200  ghmqusker  19201  pgpfi  19519  sylow3lem2  19542  efgredlem  19661  frgpnabllem1  19787  imasabl  19790  dprdfcntz  19931  ablfac1b  19986  pgpfac1lem3  19993  pgpfac1lem5  19995  pgpfaclem3  19999  omndmul2  20047  gsumle  20059  ringinvnzdiv  20221  rnghmsubcsetclem2  20549  rhmsubcsetclem2  20578  srhmsubc  20597  rhmsubclem4  20605  imadrhmcl  20714  cntzsdrg  20719  suborng  20793  islmhm2  20974  lspsneleq  21054  rhmpreimaidl  21216  znunit  21502  psgndiflemB  21539  uvcff  21730  uvcf1  21731  lindfmm  21766  sraassab  21807  psrval  21854  psrass1  21902  resspsrmul  21914  mplbas2  21978  mhpmulcl  22065  psdmul  22082  coe1tmmul  22192  gsummoncoe1  22224  evls1fpws  22285  dmatsubcl  22414  scmatscm  22429  smatvscl  22440  marrepval  22478  mdetdiaglem  22514  mdetunilem8  22535  mdetunilem9  22536  pmatcoe1fsupp  22617  decpmatmulsumfsupp  22689  pmatcollpw2lem  22693  mp2pm2mplem4  22725  pm2mpmhmlem1  22734  pm2mpmhmlem2  22735  pm2mp  22741  fvmptnn04if  22765  cpmadugsumfi  22793  cpmidg2sum  22796  cpmadumatpoly  22799  cayhamlem4  22804  neiptoptop  23047  neitr  23096  ordtrest2lem  23119  cnpnei  23180  iscncl  23185  cncls  23190  cnntr  23191  cncnp  23196  lmcnp  23220  isreg2  23293  hauscmplem  23322  cmpfi  23324  1stcfb  23361  1stcrest  23369  2ndcctbss  23371  2ndcomap  23374  islly2  23400  cldllycmp  23411  lly1stc  23412  locfincmp  23442  llycmpkgen2  23466  1stckgenlem  23469  kgencn2  23473  kgencn3  23474  ptbasfi  23497  ptpjopn  23528  txdis1cn  23551  txlly  23552  txnlly  23553  txtube  23556  txcmplem2  23558  tx1stc  23566  txkgen  23568  xkopt  23571  xkoco2cn  23574  xkococnlem  23575  xkococn  23576  xkoinjcn  23603  tgqtop  23628  regr1lem  23655  kqreglem1  23657  nrmhmph  23710  rnelfmlem  23868  rnelfm  23869  fmfnfmlem4  23873  fmfnfm  23874  ufldom  23878  flimopn  23891  hauspwpwf1  23903  fclsopn  23930  fclsnei  23935  fclsrest  23940  alexsublem  23960  alexsubALTlem3  23965  ptcmplem2  23969  ptcmplem3  23970  cnextfun  23980  cnextcn  23983  symgtgp  24022  tgpt0  24035  qustgpopn  24036  tsmsxplem1  24069  trust  24145  utopsnneiplem  24163  utop3cls  24167  utopreg  24168  isucn2  24194  cstucnd  24199  ucncn  24200  fmucnd  24207  cfilufg  24208  neipcfilu  24211  met2ndci  24438  prdsxmslem2  24445  metcnp3  24456  metustid  24470  metustexhalf  24472  metust  24474  psmetutop  24483  nmoleub  24647  reconnlem2  24744  xrge0tsms  24751  cncfco  24828  lebnumlem3  24890  lebnum  24891  nmoleub2lem2  25044  nmoleub3  25047  iscfil2  25194  iscau4  25207  iscmet3lem2  25220  equivcfil  25227  equivcau  25228  caubl  25236  rrxdstprj1  25337  ovolshftlem2  25439  ovolicc2lem4  25449  uniioombl  25518  i1fmulclem  25631  mbfi1fseqlem6  25649  itg2const2  25670  itg2split  25678  bddiblnc  25771  ellimc2  25806  ellimc3  25808  limcflf  25810  dvmptfsum  25907  dvferm1  25917  dvferm2  25919  dvlip2  25928  c1lip1  25930  lhop1  25947  ftc1a  25972  ply1divex  26070  plyeq0lem  26143  plymullem1  26147  coemullem  26183  coemulc  26188  ulmshftlem  26326  ulmcaulem  26331  ulmbdd  26335  ulmcn  26336  ulmdvlem3  26339  mtestbdd  26342  pserulm  26359  pserdvlem2  26366  abelthlem8  26377  xrlimcnp  26906  jensen  26927  lgamucov  26976  logfac2  27156  dchrelbas3  27177  dchrpt  27206  gausslemma2dlem1a  27304  lgsquad3  27326  2sqb  27371  rpvmasumlem  27426  dchrisumlem1  27428  dchrisumlem3  27430  dchrmusum2  27433  dchrvmasumlem2  27437  dchrisum0flblem1  27447  dchrisum0lem1b  27454  dchrisum0lem1  27455  dchrisum0  27459  mulog2sumlem2  27474  pntlem3  27548  ostth3  27577  slerec  27761  cofcutr  27869  remulscllem2  28404  istrkgcb  28435  tgbtwndiff  28485  iscgrglt  28493  tgcgrxfr  28497  motcgrg  28523  lnext  28546  tgbtwnconn1  28554  tgbtwnconn3  28556  legval  28563  legtrid  28570  legso  28578  hlcgreu  28597  tglnne  28607  tglineeltr  28610  tglnne0  28619  colline  28628  tglowdim2l  28629  tglowdim2ln  28630  mirreu3  28633  mirbtwnhl  28659  krippenlem  28669  midexlem  28671  perpcom  28692  perpneq  28693  footexALT  28697  footex  28700  colperpexlem3  28711  colperpex  28712  opphllem  28714  midex  28716  oppne3  28722  opptgdim2  28724  oppnid  28725  opphllem2  28727  opphllem5  28730  opphllem6  28731  oppperpex  28732  outpasch  28734  hlpasch  28735  lnopp2hpgb  28742  hpgerlem  28744  colopp  28748  colhp  28749  lmieu  28763  lnperpex  28782  trgcopy  28783  trgcopyeulem  28784  iscgra1  28789  cgrane1  28791  cgrane2  28792  cgrane3  28793  cgrane4  28794  cgrahl1  28795  cgrahl2  28796  cgracgr  28797  cgraswap  28799  cgracom  28801  cgratr  28802  flatcgra  28803  cgrabtwn  28805  cgrahl  28806  sacgr  28810  acopyeu  28813  cgrg3col4  28832  tgasa1  28837  f1otrg  28850  f1otrge  28851  axeuclidlem  28942  axcontlem2  28945  umgrvad2edg  29193  usgredg2vlem2  29206  pthdepisspth  29715  clwwlkccatlem  29971  clwlkclwwlklem2  29982  3cycld  30160  eupth2lems  30220  eucrctshift  30225  frgr3vlem2  30256  n4cyclfrgr  30273  numclwwlk1lem2f1  30339  numclwwlk2lem1  30358  ubthlem3  30854  chirredlem1  32372  chirredlem3  32374  cdj1i  32415  fnpreimac  32655  xrge0infss  32747  nn0xmulclb  32758  hashxpe  32794  sgnmul  32823  2exple2exp  32833  ccatf1  32937  ccatws1f1o  32939  swrdf1  32944  dfmgc2lem  32983  mgcf1o  32991  mndlactf1  33014  mndlactfo  33015  mndractf1  33016  mndractfo  33017  gsumfs2d  33042  gsumhashmul  33048  xrge0tsmsd  33049  gsumwun  33052  psgnfzto1stlem  33076  cycpmco2  33109  cycpmrn  33119  tocyccntz  33120  cycpmconjslem2  33131  cyc3conja  33133  conjga  33146  submarchi  33162  isarchiofld  33175  elrgspnlem1  33216  elrgspnlem2  33217  elrgspnlem3  33218  elrgspnlem4  33219  elrgspnsubrunlem1  33221  elrgspnsubrunlem2  33222  elrgspnsubrun  33223  erlval  33232  erler  33239  rloccring  33244  rlocf1  33247  domnprodn0  33249  subrdom  33258  imaslmod  33325  znfermltl  33338  lindfpropd  33354  unitprodclb  33361  nsgmgc  33384  nsgqusf1olem1  33385  unitpidl1  33396  elrspunidl  33400  elrspunsn  33401  rhmimaidl  33404  drngidl  33405  qsidomlem1  33424  mxidlprm  33442  mxidlirredi  33443  drngmxidlr  33450  qsdrngilem  33466  qsdrngi  33467  rsprprmprmidl  33494  rsprprmprmidlb  33495  rprmasso2  33498  rprmirred  33503  rprmirredb  33504  rprmdvdspow  33505  1arithidom  33509  pidufd  33515  1arithufdlem3  33518  dfufd2  33522  ply1dg3rt0irred  33553  extvfvcl  33587  mplvrpmga  33593  mplvrpmmhm  33594  mplvrpmrhm  33595  esplymhp  33608  esplyfval3  33612  esplyind  33613  exsslsb  33630  lbslelsp  33631  ply1degltdimlem  33656  lindsunlem  33658  lindsun  33659  lbsdiflsp0  33660  dimkerim  33661  fedgmul  33665  dimlssid  33666  assalactf1o  33669  extdg1id  33700  evls1fldgencl  33704  fldextrspunlsplem  33707  fldextrspunlsp  33708  extdgfialglem1  33726  minplyirred  33745  fldext2chn  33762  cos9thpiminplylem2  33817  smatrcl  33830  1smat1  33838  submateq  33843  mdetpmtr1  33857  madjusmdetlem2  33862  locfinreflem  33874  cmppcmp  33892  rhmpreimacn  33919  ordtrest2NEWlem  33956  ordtconnlem1  33958  lmdvg  33987  zrhcntr  34013  esumpcvgval  34112  esum2d  34127  sigapildsys  34196  ldgenpisyslem1  34197  fiunelros  34208  volmeas  34265  imambfm  34296  omssubadd  34334  carsggect  34352  carsgclctunlem3  34354  signsply0  34585  signstres  34609  actfunsnf1o  34638  actfunsnrndisj  34639  reprsuc  34649  reprinfz1  34656  breprexplema  34664  breprexplemc  34666  breprexp  34667  breprexpnat  34668  circlemeth  34674  hgt750lemb  34690  tgoldbachgtd  34696  erdszelem8  35263  pconnconn  35296  cvmlift2lem12  35379  cvmlift3lem5  35388  cvmlift3lem7  35390  cvmlift3lem8  35391  fmla1  35452  mrsubrn  35578  msrval  35603  msubff1  35621  btwnconn1lem13  36164  elicc3  36382  neibastop2lem  36425  weiunfr  36532  unbdqndv2  36576  irrdifflemf  37390  ltflcei  37668  lindsenlbs  37675  matunitlindflem1  37676  matunitlindflem2  37677  poimirlem4  37684  poimirlem13  37693  poimirlem14  37694  poimirlem22  37702  poimirlem26  37706  poimirlem27  37707  heicant  37715  mblfinlem2  37718  mblfinlem3  37719  mblfinlem4  37720  cnambfre  37728  itg2addnclem  37731  itg2addnclem2  37732  itg2gt0cn  37735  ftc1cnnc  37752  ftc1anclem5  37757  ftc1anclem7  37759  ftc1anc  37761  equivtotbnd  37838  isbndx  37842  ssbnd  37848  heibor1lem  37869  rrncmslem  37892  islshpat  39136  lfl1dim  39240  lfl1dim2N  39241  lkrpssN  39282  glbconN  39496  hlhgt2  39508  3dim2  39587  3dim3  39588  islln3  39629  islvol5  39698  2lplnja  39738  dalem19  39801  isline4N  39896  2polssN  40034  lhpmatb  40150  4atex  40195  trlatn0  40291  cdlemf2  40681  dialss  41165  diaglbN  41174  diaintclN  41177  dibglbN  41285  dibintclN  41286  dihlsscpre  41353  dihglblem5aN  41411  dihglblem2aN  41412  dihglblem4  41416  dihatexv  41457  dihjat1lem  41547  lcfl6  41619  mapdval2N  41749  aks4d1p8  42200  fldhmf1  42203  primrootscoprmpow  42212  primrootscoprbij2  42216  primrootspoweq0  42219  evl1gprodd  42230  hashscontpow  42235  aks6d1c2lem4  42240  idomnnzgmulnz  42246  deg1gprod  42253  sticksstones8  42266  sticksstones12a  42270  aks6d1c6lem3  42285  aks6d1c6lem5  42290  aks6d1c7  42297  aks5lem5a  42304  unitscyglem2  42309  sn-0tie0  42569  imacrhmcl  42632  fiabv  42654  evlsvvval  42681  evlselv  42705  fsuppind  42708  prjspertr  42723  prjspreln0  42727  prjspner1  42744  elrfi  42811  eldioph2  42879  diophin  42889  irrapxlem2  42940  irrapxlem3  42941  irrapxlem4  42942  irrapxlem5  42943  pell1234qrne0  42970  pell1234qrreccl  42971  pell1234qrmulcl  42972  pell14qrgt0  42976  pell14qrdich  42986  pell1qrge1  42987  pellfundex  43003  congabseq  43091  jm2.27b  43123  jm2.27  43125  fnwe2lem2  43168  kelac1  43180  lnrfg  43236  hbt  43247  omabs2  43449  nadd1suc  43509  rfovcnvf1od  44121  ntrneiiso  44208  ntrneikb  44211  ntrneixb  44212  ntrneik3  44213  ntrneix3  44214  ntrneik13  44215  ntrneix13  44216  cvgdvgrat  44430  binomcxplemnotnn0  44473  sineq0ALT  45053  fnchoice  45150  disjf1  45304  supxrgere  45456  supxrgelem  45460  supxrge  45461  suplesup  45462  xralrple2  45477  infxr  45489  infleinflem2  45493  infleinf  45494  uzub  45553  mccl  45722  limcrecl  45753  lptioo2  45755  lptioo1  45756  lptre2pt  45762  addlimc  45770  limsupmnflem  45842  climxrre  45872  liminflimsupclim  45929  climxlim2lem  45967  xlimliminflimsup  45984  icccncfext  46009  cncfiooicclem1  46015  cncfiooiccre  46017  dvbdfbdioolem2  46051  ioodvbdlimc1lem1  46053  dvnxpaek  46064  dvmptfprodlem  46066  dvmptfprod  46067  dvnprodlem3  46070  itgioocnicc  46099  itgspltprt  46101  stoweidlem31  46153  fourierdlem39  46268  fourierdlem42  46271  fourierdlem48  46276  fourierdlem49  46277  fourierdlem50  46278  fourierdlem51  46279  fourierdlem64  46292  fourierdlem65  46293  fourierdlem74  46302  fourierdlem75  46303  fourierdlem81  46309  fourierdlem82  46310  fourierdlem101  46329  etransclem23  46379  etransclem27  46383  etransclem32  46388  etransclem33  46389  etransclem35  46391  etransclem38  46394  sge0tsms  46502  sge0cl  46503  sge0f1o  46504  sge0split  46531  sge0rpcpnf  46543  sge0seq  46568  nnfoctbdjlem  46577  iundjiun  46582  meaiuninc3v  46606  meaiininclem  46608  omeiunltfirp  46641  carageniuncllem2  46644  carageniuncl  46645  hoidmv1lelem1  46713  hoidmvlelem3  46719  hoidmvlelem5  46721  hoidmvle  46722  hoiqssbllem3  46746  iunhoiioolem  46797  pimdecfgtioo  46839  pimincfltioo  46840  preimageiingt  46842  preimaleiinlt  46843  smflimlem4  46896  chnerlem1  47004  iccpartigtl  47547  iccpartgt  47551  sprsymrelf1lem  47615  paireqne  47635  proththd  47738  requad2  47747  sbgoldbst  47902  bgoldbtbndlem4  47932  isuspgrim0lem  48017  isuspgrim0  48018  isuspgrimlem  48019  gricushgr  48041  grimedg  48059  grimgrtri  48073  isubgr3stgrlem7  48096  gpgusgralem  48180  pgn4cyclex  48250  2zrngmmgm  48376  cznrng  48385  rhmsubcALTVlem4  48408  srhmsubcALTV  48449  lincsum  48554  lcoss  48561  snlindsntor  48596  islindeps2  48608  line2x  48879  line2y  48880  itscnhlinecirc02p  48910  discsubc  49189  imasubc3  49281  uppropd  49306  swapfval  49387  fucofvalg  49443  fuco21  49461  precofvalALT  49493  2arwcat  49725  lanup  49766  ranup  49767