Theorem ad3antrrr 731

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 727	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  733  ad4antlr  734  simplll  775  fsnex  7238  fimaproj  8085  frxp3  8101  oaabs  8584  oaabs2  8585  omabs  8587  cofon1  8608  sbthlem8  9032  cantnfle  9592  cantnfp1  9602  cantnflem1c  9608  sornom  10199  enfin2i  10243  ttukeylem6  10436  fpwwe2lem12  10565  fpwwe2  10566  winalim2  10619  wuncval2  10670  negf1o  11580  xlemul1a  13240  difreicc  13437  flflp1  13766  faclbnd  14252  swrdswrd  14667  swrdccatin1  14687  pfxccatin12lem3  14694  swrdccat3blem  14701  ello12  15478  lo1bdd2  15486  elo12  15489  rlimclim1  15507  rlimcld2  15540  o1co  15548  o1of2  15575  o1rlimmul  15581  rlimsqzlem  15611  isercoll  15630  o1fsum  15776  supcvg  15821  dvds2ln  16258  lcmgcdlem  16575  cncongr2  16637  isprm5  16677  prmdvdsncoprmbd  16697  pcadd  16860  vdwlem2  16953  vdwlem11  16962  sbcie3s  17132  prdsval  17418  mreexexlem4d  17613  isacs2  17619  catcocl  17651  catass  17652  subccocl  17812  fullsubc  17817  funcco  17838  funcpropd  17869  fullpropd  17889  ffthiso  17898  isnat  17917  natpropd  17946  fucpropd  17947  xpcval  18143  evlf2  18184  curfpropd  18199  curfuncf  18204  uncfcurf  18205  curf2ndf  18213  hofcl  18225  hofpropd  18233  yonffthlem  18248  isacs3lem  18508  acsfiindd  18519  chnind  18587  gsumpropd2lem  18647  resmgmhm2b  18681  resmhm2b  18790  mhmid  19039  mhmmnd  19040  ghmgrp  19042  conjnmzb  19228  ghmqusnsg  19257  ghmquskerlem3  19261  ghmqusker  19262  pgpfi  19580  sylow3lem2  19603  efgredlem  19722  frgpnabllem1  19848  imasabl  19851  dprdfcntz  19992  ablfac1b  20047  pgpfac1lem3  20054  pgpfac1lem5  20056  pgpfaclem3  20060  omndmul2  20108  gsumle  20120  ringinvnzdiv  20282  rnghmsubcsetclem2  20609  rhmsubcsetclem2  20638  srhmsubc  20657  rhmsubclem4  20665  imadrhmcl  20774  cntzsdrg  20779  suborng  20853  islmhm2  21033  lspsneleq  21113  rhmpreimaidl  21275  znunit  21543  psgndiflemB  21580  uvcff  21771  uvcf1  21772  lindfmm  21807  sraassab  21848  psrval  21895  psrass1  21942  resspsrmul  21954  mplbas2  22020  evlsvvval  22071  mhpmulcl  22115  psdmul  22132  coe1tmmul  22242  gsummoncoe1  22273  evls1fpws  22334  dmatsubcl  22463  scmatscm  22478  smatvscl  22489  marrepval  22527  mdetdiaglem  22563  mdetunilem8  22584  mdetunilem9  22585  pmatcoe1fsupp  22666  decpmatmulsumfsupp  22738  pmatcollpw2lem  22742  mp2pm2mplem4  22774  pm2mpmhmlem1  22783  pm2mpmhmlem2  22784  pm2mp  22790  fvmptnn04if  22814  cpmadugsumfi  22842  cpmidg2sum  22845  cpmadumatpoly  22848  cayhamlem4  22853  neiptoptop  23096  neitr  23145  ordtrest2lem  23168  cnpnei  23229  iscncl  23234  cncls  23239  cnntr  23240  cncnp  23245  lmcnp  23269  isreg2  23342  hauscmplem  23371  cmpfi  23373  1stcfb  23410  1stcrest  23418  2ndcctbss  23420  2ndcomap  23423  islly2  23449  cldllycmp  23460  lly1stc  23461  locfincmp  23491  llycmpkgen2  23515  1stckgenlem  23518  kgencn2  23522  kgencn3  23523  ptbasfi  23546  ptpjopn  23577  txdis1cn  23600  txlly  23601  txnlly  23602  txtube  23605  txcmplem2  23607  tx1stc  23615  txkgen  23617  xkopt  23620  xkoco2cn  23623  xkococnlem  23624  xkococn  23625  xkoinjcn  23652  tgqtop  23677  regr1lem  23704  kqreglem1  23706  nrmhmph  23759  rnelfmlem  23917  rnelfm  23918  fmfnfmlem4  23922  fmfnfm  23923  ufldom  23927  flimopn  23940  hauspwpwf1  23952  fclsopn  23979  fclsnei  23984  fclsrest  23989  alexsublem  24009  alexsubALTlem3  24014  ptcmplem2  24018  ptcmplem3  24019  cnextfun  24029  cnextcn  24032  symgtgp  24071  tgpt0  24084  qustgpopn  24085  tsmsxplem1  24118  trust  24194  utopsnneiplem  24212  utop3cls  24216  utopreg  24217  isucn2  24243  cstucnd  24248  ucncn  24249  fmucnd  24256  cfilufg  24257  neipcfilu  24260  met2ndci  24487  prdsxmslem2  24494  metcnp3  24505  metustid  24519  metustexhalf  24521  metust  24523  psmetutop  24532  nmoleub  24696  reconnlem2  24793  xrge0tsms  24800  cncfco  24874  lebnumlem3  24930  lebnum  24931  nmoleub2lem2  25083  nmoleub3  25086  iscfil2  25233  iscau4  25246  iscmet3lem2  25259  equivcfil  25266  equivcau  25267  caubl  25275  rrxdstprj1  25376  ovolshftlem2  25477  ovolicc2lem4  25487  uniioombl  25556  i1fmulclem  25669  mbfi1fseqlem6  25687  itg2const2  25708  itg2split  25716  bddiblnc  25809  ellimc2  25844  ellimc3  25846  limcflf  25848  dvmptfsum  25942  dvferm1  25952  dvferm2  25954  dvlip2  25962  c1lip1  25964  lhop1  25981  ftc1a  26004  ply1divex  26102  plyeq0lem  26175  plymullem1  26179  coemullem  26215  coemulc  26220  ulmshftlem  26354  ulmcaulem  26359  ulmbdd  26363  ulmcn  26364  ulmdvlem3  26367  mtestbdd  26370  pserulm  26387  pserdvlem2  26393  abelthlem8  26404  xrlimcnp  26932  jensen  26952  lgamucov  27001  logfac2  27180  dchrelbas3  27201  dchrpt  27230  gausslemma2dlem1a  27328  lgsquad3  27350  2sqb  27395  rpvmasumlem  27450  dchrisumlem1  27452  dchrisumlem3  27454  dchrmusum2  27457  dchrvmasumlem2  27461  dchrisum0flblem1  27471  dchrisum0lem1b  27478  dchrisum0lem1  27479  dchrisum0  27483  mulog2sumlem2  27498  pntlem3  27572  ostth3  27601  lesrec  27791  cofcutr  27916  remulscllem2  28493  istrkgcb  28524  tgbtwndiff  28574  iscgrglt  28582  tgcgrxfr  28586  motcgrg  28612  lnext  28635  tgbtwnconn1  28643  tgbtwnconn3  28645  legval  28652  legtrid  28659  legso  28667  hlcgreu  28686  tglnne  28696  tglineeltr  28699  tglnne0  28708  colline  28717  tglowdim2l  28718  tglowdim2ln  28719  mirreu3  28722  mirbtwnhl  28748  krippenlem  28758  midexlem  28760  perpcom  28781  perpneq  28782  footexALT  28786  footex  28789  colperpexlem3  28800  colperpex  28801  opphllem  28803  midex  28805  oppne3  28811  opptgdim2  28813  oppnid  28814  opphllem2  28816  opphllem5  28819  opphllem6  28820  oppperpex  28821  outpasch  28823  hlpasch  28824  lnopp2hpgb  28831  hpgerlem  28833  colopp  28837  colhp  28838  lmieu  28852  lnperpex  28871  trgcopy  28872  trgcopyeulem  28873  iscgra1  28878  cgrane1  28880  cgrane2  28881  cgrane3  28882  cgrane4  28883  cgrahl1  28884  cgrahl2  28885  cgracgr  28886  cgraswap  28888  cgracom  28890  cgratr  28891  flatcgra  28892  cgrabtwn  28894  cgrahl  28895  sacgr  28899  acopyeu  28902  cgrg3col4  28921  tgasa1  28926  f1otrg  28939  f1otrge  28940  axeuclidlem  29031  axcontlem2  29034  umgrvad2edg  29282  usgredg2vlem2  29295  pthdepisspth  29803  clwwlkccatlem  30059  clwlkclwwlklem2  30070  3cycld  30248  eupth2lems  30308  eucrctshift  30313  frgr3vlem2  30344  n4cyclfrgr  30361  numclwwlk1lem2f1  30427  numclwwlk2lem1  30446  ubthlem3  30943  chirredlem1  32461  chirredlem3  32463  cdj1i  32504  fnpreimac  32743  xrge0infss  32833  nn0xmulclb  32844  hashxpe  32880  sgnmul  32908  2exple2exp  32918  ccatf1  33009  ccatws1f1o  33011  swrdf1  33016  dfmgc2lem  33055  mgcf1o  33063  mndlactf1  33086  mndlactfo  33087  mndractf1  33088  mndractfo  33089  gsumfs2d  33122  gsumhashmul  33128  suppgsumssiun  33133  xrge0tsmsd  33134  gsumwun  33137  psgnfzto1stlem  33161  cycpmco2  33194  cycpmrn  33204  tocyccntz  33205  cycpmconjslem2  33216  cyc3conja  33218  conjga  33231  submarchi  33247  isarchiofld  33260  elrgspnlem1  33303  elrgspnlem2  33304  elrgspnlem3  33305  elrgspnlem4  33306  elrgspnsubrunlem1  33308  elrgspnsubrunlem2  33309  elrgspnsubrun  33310  erlval  33319  erler  33326  rloccring  33331  rlocf1  33334  domnprodn0  33336  domnprodeq0  33337  subrdom  33346  imaslmod  33413  znfermltl  33426  lindfpropd  33442  unitprodclb  33449  nsgmgc  33472  nsgqusf1olem1  33473  unitpidl1  33484  elrspunidl  33488  elrspunsn  33489  rhmimaidl  33492  drngidl  33493  qsidomlem1  33512  mxidlprm  33530  mxidlirredi  33531  drngmxidlr  33538  qsdrngilem  33554  qsdrngi  33555  rsprprmprmidl  33582  rsprprmprmidlb  33583  rprmasso2  33586  rprmirred  33591  rprmirredb  33592  rprmdvdspow  33593  1arithidom  33597  pidufd  33603  1arithufdlem3  33606  dfufd2  33610  deg1prod  33643  ply1dg3rt0irred  33644  extvfvcl  33680  mplvrpmga  33689  mplvrpmmhm  33690  mplvrpmrhm  33691  psrgsum  33692  psrmonprod  33696  esplymhp  33712  esplyfval3  33716  esplyfval1  33717  esplyfvaln  33718  esplyind  33719  exsslsb  33741  lbslelsp  33742  ply1degltdimlem  33766  lindsunlem  33768  lindsun  33769  lbsdiflsp0  33770  dimkerim  33771  fedgmul  33775  dimlssid  33776  assalactf1o  33779  extdg1id  33810  evls1fldgencl  33814  fldextrspunlsplem  33817  fldextrspunlsp  33818  extdgfialglem1  33836  minplyirred  33855  fldext2chn  33872  cos9thpiminplylem2  33927  smatrcl  33940  1smat1  33948  submateq  33953  mdetpmtr1  33967  madjusmdetlem2  33972  locfinreflem  33984  cmppcmp  34002  rhmpreimacn  34029  ordtrest2NEWlem  34066  ordtconnlem1  34068  lmdvg  34097  zrhcntr  34123  esumpcvgval  34222  esum2d  34237  sigapildsys  34306  ldgenpisyslem1  34307  fiunelros  34318  volmeas  34375  imambfm  34406  omssubadd  34444  carsggect  34462  carsgclctunlem3  34464  signsply0  34695  signstres  34719  actfunsnf1o  34748  actfunsnrndisj  34749  reprsuc  34759  reprinfz1  34766  breprexplema  34774  breprexplemc  34776  breprexp  34777  breprexpnat  34778  circlemeth  34784  hgt750lemb  34800  tgoldbachgtd  34806  erdszelem8  35380  pconnconn  35413  cvmlift2lem12  35496  cvmlift3lem5  35505  cvmlift3lem7  35507  cvmlift3lem8  35508  fmla1  35569  mrsubrn  35695  msrval  35720  msubff1  35738  btwnconn1lem13  36281  elicc3  36499  neibastop2lem  36542  weiunfr  36649  unbdqndv2  36771  irrdifflemf  37639  ltflcei  37929  lindsenlbs  37936  matunitlindflem1  37937  matunitlindflem2  37938  poimirlem4  37945  poimirlem13  37954  poimirlem14  37955  poimirlem22  37963  poimirlem26  37967  poimirlem27  37968  heicant  37976  mblfinlem2  37979  mblfinlem3  37980  mblfinlem4  37981  cnambfre  37989  itg2addnclem  37992  itg2addnclem2  37993  itg2gt0cn  37996  ftc1cnnc  38013  ftc1anclem5  38018  ftc1anclem7  38020  ftc1anc  38022  equivtotbnd  38099  isbndx  38103  ssbnd  38109  heibor1lem  38130  rrncmslem  38153  islshpat  39463  lfl1dim  39567  lfl1dim2N  39568  lkrpssN  39609  glbconN  39823  hlhgt2  39835  3dim2  39914  3dim3  39915  islln3  39956  islvol5  40025  2lplnja  40065  dalem19  40128  isline4N  40223  2polssN  40361  lhpmatb  40477  4atex  40522  trlatn0  40618  cdlemf2  41008  dialss  41492  diaglbN  41501  diaintclN  41504  dibglbN  41612  dibintclN  41613  dihlsscpre  41680  dihglblem5aN  41738  dihglblem2aN  41739  dihglblem4  41743  dihatexv  41784  dihjat1lem  41874  lcfl6  41946  mapdval2N  42076  aks4d1p8  42526  fldhmf1  42529  primrootscoprmpow  42538  primrootscoprbij2  42542  primrootspoweq0  42545  evl1gprodd  42556  hashscontpow  42561  aks6d1c2lem4  42566  idomnnzgmulnz  42572  deg1gprod  42579  sticksstones8  42592  sticksstones12a  42596  aks6d1c6lem3  42611  aks6d1c6lem5  42616  aks6d1c7  42623  aks5lem5a  42630  unitscyglem2  42635  sn-0tie0  42896  imacrhmcl  42959  fiabv  42981  evlselv  43020  fsuppind  43023  prjspertr  43038  prjspreln0  43042  prjspner1  43059  elrfi  43126  eldioph2  43194  diophin  43204  irrapxlem2  43251  irrapxlem3  43252  irrapxlem4  43253  irrapxlem5  43254  pell1234qrne0  43281  pell1234qrreccl  43282  pell1234qrmulcl  43283  pell14qrgt0  43287  pell14qrdich  43297  pell1qrge1  43298  pellfundex  43314  congabseq  43402  jm2.27b  43434  jm2.27  43436  fnwe2lem2  43479  kelac1  43491  lnrfg  43547  hbt  43558  omabs2  43760  nadd1suc  43820  rfovcnvf1od  44431  ntrneiiso  44518  ntrneikb  44521  ntrneixb  44522  ntrneik3  44523  ntrneix3  44524  ntrneik13  44525  ntrneix13  44526  cvgdvgrat  44740  binomcxplemnotnn0  44783  sineq0ALT  45363  fnchoice  45460  disjf1  45613  supxrgere  45763  supxrgelem  45767  supxrge  45768  suplesup  45769  xralrple2  45784  infxr  45796  infleinflem2  45800  infleinf  45801  uzub  45859  mccl  46028  limcrecl  46059  lptioo2  46061  lptioo1  46062  lptre2pt  46068  addlimc  46076  limsupmnflem  46148  climxrre  46178  liminflimsupclim  46235  climxlim2lem  46273  xlimliminflimsup  46290  icccncfext  46315  cncfiooicclem1  46321  cncfiooiccre  46323  dvbdfbdioolem2  46357  ioodvbdlimc1lem1  46359  dvnxpaek  46370  dvmptfprodlem  46372  dvmptfprod  46373  dvnprodlem3  46376  itgioocnicc  46405  itgspltprt  46407  stoweidlem31  46459  fourierdlem39  46574  fourierdlem42  46577  fourierdlem48  46582  fourierdlem49  46583  fourierdlem50  46584  fourierdlem51  46585  fourierdlem64  46598  fourierdlem65  46599  fourierdlem74  46608  fourierdlem75  46609  fourierdlem81  46615  fourierdlem82  46616  fourierdlem101  46635  etransclem23  46685  etransclem27  46689  etransclem32  46694  etransclem33  46695  etransclem35  46697  etransclem38  46700  sge0tsms  46808  sge0cl  46809  sge0f1o  46810  sge0split  46837  sge0rpcpnf  46849  sge0seq  46874  nnfoctbdjlem  46883  iundjiun  46888  meaiuninc3v  46912  meaiininclem  46914  omeiunltfirp  46947  carageniuncllem2  46950  carageniuncl  46951  hoicvr  46976  hoidmv1lelem1  47019  hoidmvlelem3  47025  hoidmvlelem5  47027  hoidmvle  47028  hoiqssbllem3  47052  iunhoiioolem  47103  pimdecfgtioo  47145  pimincfltioo  47146  preimageiingt  47148  preimaleiinlt  47149  smflimlem4  47202  chnerlem1  47312  iccpartigtl  47883  iccpartgt  47887  sprsymrelf1lem  47951  paireqne  47971  proththd  48077  requad2  48099  sbgoldbst  48254  bgoldbtbndlem4  48284  isuspgrim0lem  48369  isuspgrim0  48370  isuspgrimlem  48371  gricushgr  48393  grimedg  48411  grimgrtri  48425  isubgr3stgrlem7  48448  gpgusgralem  48532  pgn4cyclex  48602  2zrngmmgm  48728  cznrng  48737  rhmsubcALTVlem4  48760  srhmsubcALTV  48801  lincsum  48905  lcoss  48912  snlindsntor  48947  islindeps2  48959  line2x  49230  line2y  49231  itscnhlinecirc02p  49261  discsubc  49539  imasubc3  49631  uppropd  49656  swapfval  49737  fucofvalg  49793  fuco21  49811  precofvalALT  49843  2arwcat  50075  lanup  50116  ranup  50117