Theorem ad3antrrr 743

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 486	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad2antrr 739	1 ⊢ ((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ad4antr  745  ad4antlr  746  simplll  787  fsnex  7288  fimaproj  8137  frxp3  8153  oaabs  8640  oaabs2  8641  omabs  8643  cofon1  8664  sbthlem8  9096  cantnfle  9654  cantnfp1  9664  cantnflem1c  9670  sornom  10283  enfin2i  10327  ttukeylem6  10520  fpwwe2lem12  10655  fpwwe2  10656  winalim2  10709  wuncval2  10760  negf1o  11672  xlemul1a  13344  difreicc  13541  flflp1  13872  faclbnd  14358  ccatf1  14660  swrdf1  14723  swrdswrd  14778  swrdccatin1  14798  pfxccatin12lem3  14805  swrdccat3blem  14812  sgnmul  15184  ello12  15607  lo1bdd2  15615  elo12  15618  rlimclim1  15636  rlimcld2  15669  o1co  15677  o1of2  15704  o1rlimmul  15710  rlimsqzlem  15740  isercoll  15759  o1fsum  15904  supcvg  15949  dvds2ln  16385  lcmgcdlem  16702  cncongr2  16764  isprm5  16804  prmdvdsncoprmbd  16824  pcadd  16987  vdwlem2  17080  vdwlem11  17089  sbcie3s  17260  prdsval  17546  mreexexlem4d  17741  isacs2  17747  catcocl  17779  catass  17780  subccocl  17940  fullsubc  17945  funcco  17966  funcpropd  17997  fullpropd  18017  ffthiso  18026  isnat  18045  natpropd  18074  fucpropd  18075  xpcval  18271  evlf2  18312  curfpropd  18327  curfuncf  18332  uncfcurf  18333  curf2ndf  18341  hofcl  18353  hofpropd  18361  yonffthlem  18376  isacs3lem  18636  acsfiindd  18647  chnind  18715  gsumpropd2lem  18787  resmgmhm2b  18821  resmhm2b  18937  mhmid  19192  mhmmnd  19193  ghmgrp  19195  conjnmzb  19386  ghmqusnsg  19415  ghmquskerlem3  19419  ghmqusker  19420  pgpfi  19738  sylow3lem2  19761  efgredlem  19880  frgpnabllem1  20006  imasabl  20009  dprdfcntz  20150  ablfac1b  20205  pgpfac1lem3  20212  pgpfac1lem5  20214  pgpfaclem3  20218  omndmul2  20266  gsumle  20278  ringinvnzdiv  20449  rnghmsubcsetclem2  20800  rhmsubcsetclem2  20829  srhmsubc  20848  rhmsubclem4  20856  imadrhmcl  20969  cntzsdrg  20974  suborng  21048  islmhm2  21228  lspsneleq  21308  drngidl  21454  rhmpreimaidl  21485  qsidomlem1  21549  prmidlsubm  21556  znunit  21782  psgndiflemB  21819  uvcff  22010  uvcf1  22011  lindfmm  22046  lindsenlbs  22070  sraassab  22089  psrval  22136  psrass1  22184  resspsrmul  22196  mplbas2  22264  evlsvvval  22315  mhpmulcl  22383  psdmul  22400  coe1tmmul  22509  gsummoncoe1  22539  evls1fpws  22600  dmatsubcl  22726  scmatscm  22741  smatvscl  22752  marrepval  22790  mdetdiaglem  22826  mdetunilem8  22847  mdetunilem9  22848  matunitlindflem1  22907  matunitlindflem2  22908  pmatcoe1fsupp  22932  decpmatmulsumfsupp  23004  pmatcollpw2lem  23008  mp2pm2mplem4  23040  pm2mpmhmlem1  23049  pm2mpmhmlem2  23050  pm2mp  23056  fvmptnn04if  23080  cpmadugsumfi  23108  cpmidg2sum  23111  cpmadumatpoly  23114  cayhamlem4  23119  neiptoptop  23362  neitr  23411  ordtrest2lem  23434  cnpnei  23495  iscncl  23500  cncls  23505  cnntr  23506  cncnp  23511  lmcnp  23535  isreg2  23608  hauscmplem  23637  cmpfi  23639  1stcfb  23676  1stcrest  23684  2ndcctbss  23687  2ndcomap  23690  islly2  23716  cldllycmp  23727  lly1stc  23728  locfincmp  23758  llycmpkgen2  23782  1stckgenlem  23785  kgencn2  23789  kgencn3  23790  ptbasfi  23813  ptpjopn  23844  txdis1cn  23867  txlly  23868  txnlly  23869  txtube  23872  txcmplem2  23874  tx1stc  23882  txkgen  23884  xkopt  23887  xkoco2cn  23890  xkococnlem  23891  xkococn  23892  xkoinjcn  23919  tgqtop  23944  regr1lem  23971  kqreglem1  23973  nrmhmph  24026  rnelfmlem  24184  rnelfm  24185  fmfnfmlem4  24189  fmfnfm  24190  ufldom  24194  flimopn  24207  hauspwpwf1  24219  fclsopn  24246  fclsnei  24251  fclsrest  24256  alexsublem  24276  alexsubALTlem3  24281  ptcmplem2  24285  ptcmplem3  24286  cnextfun  24296  cnextcn  24299  symgtgp  24338  tgpt0  24351  qustgpopn  24352  tsmsxplem1  24385  trust  24461  utopsnneiplem  24479  utop3cls  24483  utopreg  24484  isucn2  24510  cstucnd  24515  ucncn  24516  fmucnd  24523  cfilufg  24524  neipcfilu  24527  met2ndci  24754  prdsxmslem2  24761  metcnp3  24772  metustid  24786  metustexhalf  24788  metust  24790  psmetutop  24799  nmoleub  24963  reconnlem2  25060  xrge0tsms  25067  cncfco  25141  lebnumlem3  25197  lebnum  25198  nmoleub2lem2  25350  nmoleub3  25353  iscfil2  25500  iscau4  25513  iscmet3lem2  25526  equivcfil  25533  equivcau  25534  caubl  25542  rrxdstprj1  25643  ovolshftlem2  25744  ovolicc2lem4  25754  uniioombl  25823  i1fmulclem  25936  mbfi1fseqlem6  25954  itg2const2  25975  itg2split  25983  bddiblnc  26076  ellimc2  26111  ellimc3  26113  limcflf  26115  dvmptfsum  26209  dvferm1  26219  dvferm2  26221  dvlip2  26229  c1lip1  26231  lhop1  26248  ftc1a  26271  ply1divex  26369  plyeq0lem  26443  plymullem1  26447  coemullem  26483  coemulc  26488  ulmshftlem  26632  ulmcaulem  26637  ulmbdd  26641  ulmcn  26642  ulmdvlem3  26645  mtestbdd  26648  pserulm  26665  pserdvlem2  26671  abelthlem8  26682  xrlimcnp  27213  jensen  27233  lgamucov  27282  logfac2  27461  dchrelbas3  27482  dchrpt  27511  gausslemma2dlem1a  27609  lgsquad3  27631  2sqb  27676  rpvmasumlem  27731  dchrisumlem1  27733  dchrisumlem3  27735  dchrmusum2  27738  dchrvmasumlem2  27742  dchrisum0flblem1  27752  dchrisum0lem1b  27759  dchrisum0lem1  27760  dchrisum0  27764  mulog2sumlem2  27779  pntlem3  27853  ostth3  27882  lesrec  28072  cofcutr  28197  remulscllem2  28774  istrkgcb  28805  tgbtwndiff  28856  iscgrglt  28864  tgcgrxfr  28868  motcgrg  28894  lnext  28917  tgbtwnconn1  28925  tgbtwnconn3  28927  legval  28934  legtrid  28941  legso  28949  hlcgreu  28971  tglnne  28983  tglineeltr  28986  tglnne0  28996  colline  29005  tglowdim2l  29006  tglowdim2ln  29007  mirreu3  29013  mirbtwnhl  29039  krippenlem  29049  midexlem  29051  perpcom  29075  perpneq  29076  footexALT  29080  footex  29083  colperpexlem3  29095  colperpex  29096  opphllem  29098  midex  29100  oppne3  29106  opptgdim2  29108  oppnid  29109  opphllem2  29111  opphllem5  29114  opphllem6  29115  oppperpex  29116  outpasch  29120  hlpasch  29121  lnopp2hpgb  29128  hpgerlem  29130  colopp  29134  colhp  29135  plngrnssp  29144  lnincplng  29149  plngrotlem1  29152  plngrotlem2  29153  plngrotlem3  29154  lnssplnglem  29156  lmieu  29176  lnperpex  29196  trgcopy  29198  trgcopyeulem  29199  iscgra1  29204  cgrane1  29206  cgrane2  29207  cgrane3  29208  cgrane4  29209  cgrahl1  29210  cgrahl2  29211  cgracgr  29212  cgraswap  29214  cgracom  29216  cgratr  29217  zerocgra  29218  flatcgra  29219  cgrabtwn  29221  cgrahl  29222  sacgr  29226  acopyeu  29229  ragcgra  29230  tgaaddcpbllem1  29236  tgaaddcpbllem3  29238  tgaaddcpbl  29239  cgrg3col4  29259  angmgmaddeu1  29266  angmgmaddeu2  29267  angmgmaddeu3  29268  angmgmaddeu4  29269  angmgmaddeu5  29270  angmgmaddeu6  29271  angmgmaddeu7  29272  angmgmaddov2lem  29274  angmgmaddcpbl  29277  angmgmaddrid  29280  angmgm  29284  tgasa1  29290  prlnghpg  29311  dfprlng2  29312  perpprlng  29315  prlngex  29316  prlngmolem1  29317  prlngmolem2  29318  prlngplngtr  29324  prlngmid2  29326  quadcgrprlng  29331  f1otrg  29335  f1otrge  29336  axeuclidlem  29427  axcontlem2  29430  umgrvad2edg  29681  usgredg2vlem2  29694  pthdepisspth  30208  clwwlkccatlem  30467  clwlkclwwlklem2  30478  3cycld  30666  eupth2lems  30726  eucrctshift  30731  frgr3vlem2  30762  n4cyclfrgr  30779  numclwwlk1lem2f1  30845  numclwwlk2lem1  30864  ubthlem3  31361  chirredlem1  32879  chirredlem3  32881  cdj1i  32922  fnpreimac  33151  xrge0infss  33239  nn0xmulclb  33250  hashxpe  33286  2exple2exp  33312  ccatws1f1o  33401  dfmgc2lem  33443  mgcf1o  33451  mndlactf1  33474  mndlactfo  33475  mndractf1  33476  mndractfo  33477  gsumfs2d  33509  gsumhashmul  33515  suppgsumssiun  33520  xrge0tsmsd  33521  gsumwun  33524  psgnfzto1stlem  33548  cycpmco2  33581  cycpmrn  33591  tocyccntz  33592  cycpmconjslem2  33603  cyc3conja  33605  conjga  33618  submarchi  33634  isarchiofld  33647  elrgspnlem1  33690  elrgspnlem2  33691  elrgspnlem3  33692  elrgspnlem4  33693  elrgspnsubrunlem1  33695  elrgspnsubrunlem2  33696  elrgspnsubrun  33697  erlval  33706  erler  33713  rloccring  33719  rlocf1  33722  rlocisunit  33724  domnprodn0  33726  domnprodeq0  33727  subrdom  33733  imaslmod  33801  znfermltl  33809  lindfpropd  33823  unitprodclb  33830  nsgmgc  33849  nsgqusf1olem1  33850  unitpidl1  33860  elrspunidl  33864  elrspunsn  33865  rhmimaidl  33868  mxidlprm  33881  mxidlirredi  33882  drngmxidlr  33888  qsdrngilem  33904  qsdrngi  33905  drnglring  33910  dflringlem2  33913  dflring3  33915  dflring4  33916  rsprprmprmidl  33940  rsprprmprmidlb  33941  rprmasso2  33944  rprmirred  33949  rprmirredb  33950  rprmdvdspow  33951  1arithidom  33955  pidufd  33961  1arithufdlem3  33964  dfufd2  33968  deg1prod  34001  ply1dg3rt0irred  34002  0mplrim  34032  mplidomlem  34045  extvfvcl  34054  mplvrpmga  34063  mplvrpmmhm  34064  mplvrpmrhm  34065  psrgsum  34066  psrmonprod  34070  esplymhp  34086  esplyfval3  34090  esplyfval1  34091  esplyfvaln  34092  esplyind  34093  exsslsb  34115  lbslelsp  34116  ply1degltdimlem  34140  lindsunlem  34142  lindsun  34143  lbsdiflsp0  34144  dimkerim  34145  fedgmul  34149  dimlssid  34150  assalactf1o  34153  extdg1id  34184  evls1fldgencl  34188  fldextrspunlsplem  34191  fldextrspunlsp  34192  extdgfialglem1  34210  minplyirred  34229  fldext2chn  34246  cos9thpiminplylem2  34301  smatrcl  34314  1smat1  34322  submateq  34327  mdetpmtr1  34341  madjusmdetlem2  34346  locfinreflem  34358  cmppcmp  34376  rhmpreimacn  34403  ordtrest2NEWlem  34440  ordtconnlem1  34442  lmdvg  34471  zrhcntr  34497  esumpcvgval  34596  esum2d  34611  sigapildsys  34681  ldgenpisyslem1  34682  fiunelros  34693  volmeas  34750  imambfm  34781  omssubadd  34819  carsggect  34837  carsgclctunlem3  34839  signsply0  35067  signstres  35091  actfunsnf1o  35120  actfunsnrndisj  35121  reprsuc  35131  reprinfz1  35138  breprexplema  35146  breprexplemc  35148  breprexp  35149  breprexpnat  35150  circlemeth  35156  hgt750lemb  35172  tgoldbachgtd  35178  erdszelem8  35785  pconnconn  35818  cvmlift2lem12  35901  cvmlift3lem5  35910  cvmlift3lem7  35912  cvmlift3lem8  35913  fmla1  35974  mrsubrn  36100  msrval  36125  msubff1  36143  btwnconn1lem13  36687  elicc3  36944  neibastop2lem  36987  weiunfr  37094  unbdqndv2  37216  irrdifflemf  38085  ltflcei  38370  poimirlem4  38381  poimirlem13  38390  poimirlem14  38391  poimirlem22  38399  poimirlem26  38403  poimirlem27  38404  heicant  38412  mblfinlem2  38415  mblfinlem3  38416  mblfinlem4  38417  cnambfre  38425  itg2addnclem  38428  itg2addnclem2  38429  itg2gt0cn  38432  ftc1cnnc  38449  ftc1anclem5  38454  ftc1anclem7  38456  ftc1anc  38458  equivtotbnd  38536  isbndx  38540  ssbnd  38546  heibor1lem  38567  rrncmslem  38590  islshpat  39898  lfl1dim  40002  lfl1dim2N  40003  lkrpssN  40044  glbconN  40258  hlhgt2  40270  3dim2  40349  3dim3  40350  islln3  40391  islvol5  40460  2lplnja  40500  dalem19  40563  isline4N  40658  2polssN  40796  lhpmatb  40912  4atex  40957  trlatn0  41053  cdlemf2  41443  dialss  41927  diaglbN  41936  diaintclN  41939  dibglbN  42047  dibintclN  42048  dihlsscpre  42115  dihglblem5aN  42173  dihglblem2aN  42174  dihglblem4  42178  dihatexv  42219  dihjat1lem  42309  lcfl6  42381  mapdval2N  42511  aks4d1p8  42961  fldhmf1  42964  primrootscoprmpow  42973  primrootscoprbij2  42977  primrootspoweq0  42980  evl1gprodd  42991  hashscontpow  42996  aks6d1c2lem4  43001  idomnnzgmulnz  43007  deg1gprod  43014  sticksstones8  43027  sticksstones12a  43031  aks6d1c6lem3  43046  aks6d1c6lem5  43051  aks6d1c7  43058  aks5lem5a  43065  unitscyglem2  43070  sn-0tie0  43347  imacrhmcl  43410  fiabv  43426  evlselv  43443  fsuppind  43444  prjspertr  43459  prjspreln0  43463  prjspner1  43480  elrfi  43547  eldioph2  43615  diophin  43625  irrapxlem2  43672  irrapxlem3  43673  irrapxlem4  43674  irrapxlem5  43675  pell1234qrne0  43702  pell1234qrreccl  43703  pell1234qrmulcl  43704  pell14qrgt0  43708  pell14qrdich  43718  pell1qrge1  43719  pellfundex  43735  congabseq  43823  jm2.27b  43855  jm2.27  43857  fnwe2lem2  43900  kelac1  43912  lnrfg  43968  hbt  43979  omabs2  44181  nadd1suc  44241  rfovcnvf1od  44852  ntrneiiso  44939  ntrneikb  44942  ntrneixb  44943  ntrneik3  44944  ntrneix3  44945  ntrneik13  44946  ntrneix13  44947  cvgdvgrat  45145  binomcxplemnotnn0  45188  sineq0ALT  45767  fnchoice  45871  disjf1  46023  supxrgere  46171  supxrgelem  46175  supxrge  46176  suplesup  46177  xralrple2  46192  infxr  46204  infleinflem2  46208  infleinf  46209  uzub  46267  mccl  46436  limcrecl  46467  lptioo2  46469  lptioo1  46470  lptre2pt  46476  addlimc  46484  limsupmnflem  46556  climxrre  46586  liminflimsupclim  46643  climxlim2lem  46681  xlimliminflimsup  46698  icccncfext  46723  cncfiooicclem1  46729  cncfiooiccre  46731  dvbdfbdioolem2  46765  ioodvbdlimc1lem1  46767  dvnxpaek  46778  dvmptfprodlem  46780  dvmptfprod  46781  dvnprodlem3  46784  itgioocnicc  46813  itgspltprt  46815  stoweidlem31  46867  fourierdlem39  46982  fourierdlem42  46985  fourierdlem48  46990  fourierdlem49  46991  fourierdlem50  46992  fourierdlem51  46993  fourierdlem64  47006  fourierdlem65  47007  fourierdlem74  47016  fourierdlem75  47017  fourierdlem81  47023  fourierdlem82  47024  fourierdlem101  47043  etransclem23  47093  etransclem27  47097  etransclem32  47102  etransclem33  47103  etransclem35  47105  etransclem38  47108  sge0tsms  47216  sge0cl  47217  sge0f1o  47218  sge0split  47245  sge0rpcpnf  47257  sge0seq  47282  nnfoctbdjlem  47291  iundjiun  47296  meaiuninc3v  47320  meaiininclem  47322  omeiunltfirp  47355  carageniuncllem2  47358  carageniuncl  47359  hoicvr  47384  hoidmv1lelem1  47427  hoidmvlelem3  47433  hoidmvlelem5  47435  hoidmvle  47436  hoiqssbllem3  47460  iunhoiioolem  47511  pimdecfgtioo  47553  pimincfltioo  47554  preimageiingt  47556  preimaleiinlt  47557  smflimlem4  47610  iccpartigtl  48331  iccpartgt  48335  sprsymrelf1lem  48399  paireqne  48419  proththd  48525  requad2  48547  sbgoldbst  48702  bgoldbtbndlem4  48732  isuspgrim0lem  48817  isuspgrim0  48818  isuspgrimlem  48819  gricushgr  48841  grimedg  48859  grimgrtri  48873  isubgr3stgrlem7  48896  gpgusgralem  48980  pgn4cyclex  49050  2zrngmmgm  49175  cznrng  49184  rhmsubcALTVlem4  49207  srhmsubcALTV  49248  lincsum  49367  lcoss  49374  snlindsntor  49409  islindeps2  49421  line2x  49692  line2y  49693  itscnhlinecirc02p  49723  discsubc  49998  imasubc3  50090  uppropd  50115  swapfval  50196  fucofvalg  50252  fuco21  50270  precofvalALT  50302  2arwcat  50534  lanup  50575  ranup  50576