Theorem ad3antrrr 742

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  ad4antr  744  ad4antlr  745  simplll  786  fsnex  7271  fimaproj  8119  frxp3  8135  oaabs  8622  oaabs2  8623  omabs  8625  cofon1  8646  sbthlem8  9070  cantnfle  9628  cantnfp1  9638  cantnflem1c  9644  sornom  10249  enfin2i  10293  ttukeylem6  10486  fpwwe2lem12  10615  fpwwe2  10616  winalim2  10669  wuncval2  10720  negf1o  11632  xlemul1a  13305  difreicc  13502  flflp1  13831  faclbnd  14317  swrdswrd  14732  swrdccatin1  14752  pfxccatin12lem3  14759  swrdccat3blem  14766  sgnmul  15134  ello12  15557  lo1bdd2  15565  elo12  15568  rlimclim1  15586  rlimcld2  15619  o1co  15627  o1of2  15654  o1rlimmul  15660  rlimsqzlem  15690  isercoll  15709  o1fsum  15855  supcvg  15900  dvds2ln  16337  lcmgcdlem  16654  cncongr2  16716  isprm5  16756  prmdvdsncoprmbd  16776  pcadd  16939  vdwlem2  17032  vdwlem11  17041  sbcie3s  17212  prdsval  17498  mreexexlem4d  17693  isacs2  17699  catcocl  17731  catass  17732  subccocl  17892  fullsubc  17897  funcco  17918  funcpropd  17949  fullpropd  17969  ffthiso  17978  isnat  17997  natpropd  18026  fucpropd  18027  xpcval  18223  evlf2  18264  curfpropd  18279  curfuncf  18284  uncfcurf  18285  curf2ndf  18293  hofcl  18305  hofpropd  18313  yonffthlem  18328  isacs3lem  18588  acsfiindd  18599  chnind  18667  gsumpropd2lem  18727  resmgmhm2b  18761  resmhm2b  18871  mhmid  19120  mhmmnd  19121  ghmgrp  19123  conjnmzb  19314  ghmqusnsg  19343  ghmquskerlem3  19347  ghmqusker  19348  pgpfi  19666  sylow3lem2  19689  efgredlem  19808  frgpnabllem1  19934  imasabl  19937  dprdfcntz  20078  ablfac1b  20133  pgpfac1lem3  20140  pgpfac1lem5  20142  pgpfaclem3  20146  omndmul2  20194  gsumle  20206  ringinvnzdiv  20375  rnghmsubcsetclem2  20708  rhmsubcsetclem2  20737  srhmsubc  20756  rhmsubclem4  20764  imadrhmcl  20869  cntzsdrg  20874  suborng  20948  islmhm2  21128  lspsneleq  21208  rhmpreimaidl  21378  qsidomlem1  21440  prmidlsubm  21447  znunit  21673  psgndiflemB  21710  uvcff  21901  uvcf1  21902  lindfmm  21937  sraassab  21978  psrval  22025  psrass1  22073  resspsrmul  22085  mplbas2  22153  evlsvvval  22204  mhpmulcl  22272  psdmul  22289  coe1tmmul  22398  gsummoncoe1  22429  evls1fpws  22490  dmatsubcl  22616  scmatscm  22631  smatvscl  22642  marrepval  22680  mdetdiaglem  22716  mdetunilem8  22737  mdetunilem9  22738  pmatcoe1fsupp  22819  decpmatmulsumfsupp  22891  pmatcollpw2lem  22895  mp2pm2mplem4  22927  pm2mpmhmlem1  22936  pm2mpmhmlem2  22937  pm2mp  22943  fvmptnn04if  22967  cpmadugsumfi  22995  cpmidg2sum  22998  cpmadumatpoly  23001  cayhamlem4  23006  neiptoptop  23249  neitr  23298  ordtrest2lem  23321  cnpnei  23382  iscncl  23387  cncls  23392  cnntr  23393  cncnp  23398  lmcnp  23422  isreg2  23495  hauscmplem  23524  cmpfi  23526  1stcfb  23563  1stcrest  23571  2ndcctbss  23573  2ndcomap  23576  islly2  23602  cldllycmp  23613  lly1stc  23614  locfincmp  23644  llycmpkgen2  23668  1stckgenlem  23671  kgencn2  23675  kgencn3  23676  ptbasfi  23699  ptpjopn  23730  txdis1cn  23753  txlly  23754  txnlly  23755  txtube  23758  txcmplem2  23760  tx1stc  23768  txkgen  23770  xkopt  23773  xkoco2cn  23776  xkococnlem  23777  xkococn  23778  xkoinjcn  23805  tgqtop  23830  regr1lem  23857  kqreglem1  23859  nrmhmph  23912  rnelfmlem  24070  rnelfm  24071  fmfnfmlem4  24075  fmfnfm  24076  ufldom  24080  flimopn  24093  hauspwpwf1  24105  fclsopn  24132  fclsnei  24137  fclsrest  24142  alexsublem  24162  alexsubALTlem3  24167  ptcmplem2  24171  ptcmplem3  24172  cnextfun  24182  cnextcn  24185  symgtgp  24224  tgpt0  24237  qustgpopn  24238  tsmsxplem1  24271  trust  24347  utopsnneiplem  24365  utop3cls  24369  utopreg  24370  isucn2  24396  cstucnd  24401  ucncn  24402  fmucnd  24409  cfilufg  24410  neipcfilu  24413  met2ndci  24640  prdsxmslem2  24647  metcnp3  24658  metustid  24672  metustexhalf  24674  metust  24676  psmetutop  24685  nmoleub  24849  reconnlem2  24946  xrge0tsms  24953  cncfco  25027  lebnumlem3  25083  lebnum  25084  nmoleub2lem2  25236  nmoleub3  25239  iscfil2  25386  iscau4  25399  iscmet3lem2  25412  equivcfil  25419  equivcau  25420  caubl  25428  rrxdstprj1  25529  ovolshftlem2  25630  ovolicc2lem4  25640  uniioombl  25709  i1fmulclem  25822  mbfi1fseqlem6  25840  itg2const2  25861  itg2split  25869  bddiblnc  25962  ellimc2  25997  ellimc3  25999  limcflf  26001  dvmptfsum  26095  dvferm1  26105  dvferm2  26107  dvlip2  26115  c1lip1  26117  lhop1  26134  ftc1a  26157  ply1divex  26255  plyeq0lem  26328  plymullem1  26332  coemullem  26368  coemulc  26373  ulmshftlem  26510  ulmcaulem  26515  ulmbdd  26519  ulmcn  26520  ulmdvlem3  26523  mtestbdd  26526  pserulm  26543  pserdvlem2  26549  abelthlem8  26560  xrlimcnp  27091  jensen  27111  lgamucov  27160  logfac2  27339  dchrelbas3  27360  dchrpt  27389  gausslemma2dlem1a  27487  lgsquad3  27509  2sqb  27554  rpvmasumlem  27609  dchrisumlem1  27611  dchrisumlem3  27613  dchrmusum2  27616  dchrvmasumlem2  27620  dchrisum0flblem1  27630  dchrisum0lem1b  27637  dchrisum0lem1  27638  dchrisum0  27642  mulog2sumlem2  27657  pntlem3  27731  ostth3  27760  lesrec  27950  cofcutr  28075  remulscllem2  28652  istrkgcb  28683  tgbtwndiff  28733  iscgrglt  28741  tgcgrxfr  28745  motcgrg  28771  lnext  28794  tgbtwnconn1  28802  tgbtwnconn3  28804  legval  28811  legtrid  28818  legso  28826  hlcgreu  28845  tglnne  28855  tglineeltr  28858  tglnne0  28868  colline  28877  tglowdim2l  28878  tglowdim2ln  28879  mirreu3  28885  mirbtwnhl  28911  krippenlem  28921  midexlem  28923  perpcom  28944  perpneq  28945  footexALT  28949  footex  28952  colperpexlem3  28963  colperpex  28964  opphllem  28966  midex  28968  oppne3  28974  opptgdim2  28976  oppnid  28977  opphllem2  28979  opphllem5  28982  opphllem6  28983  oppperpex  28984  outpasch  28986  hlpasch  28987  lnopp2hpgb  28994  hpgerlem  28996  colopp  29000  colhp  29001  plngrnssp  29009  lnincplng  29014  plngrotlem1  29017  plngrotlem2  29018  plngrotlem3  29019  lnssplnglem  29021  lmieu  29036  lnperpex  29055  trgcopy  29056  trgcopyeulem  29057  iscgra1  29062  cgrane1  29064  cgrane2  29065  cgrane3  29066  cgrane4  29067  cgrahl1  29068  cgrahl2  29069  cgracgr  29070  cgraswap  29072  cgracom  29074  cgratr  29075  flatcgra  29076  cgrabtwn  29078  cgrahl  29079  sacgr  29083  acopyeu  29086  cgrg3col4  29105  tgasa1  29110  f1otrg  29129  f1otrge  29130  axeuclidlem  29221  axcontlem2  29224  umgrvad2edg  29472  usgredg2vlem2  29485  pthdepisspth  29993  clwwlkccatlem  30249  clwlkclwwlklem2  30260  3cycld  30438  eupth2lems  30498  eucrctshift  30503  frgr3vlem2  30534  n4cyclfrgr  30551  numclwwlk1lem2f1  30617  numclwwlk2lem1  30636  ubthlem3  31133  chirredlem1  32651  chirredlem3  32653  cdj1i  32694  fnpreimac  32927  xrge0infss  33017  nn0xmulclb  33028  hashxpe  33064  2exple2exp  33091  ccatf1  33182  ccatws1f1o  33184  swrdf1  33189  dfmgc2lem  33228  mgcf1o  33236  mndlactf1  33259  mndlactfo  33260  mndractf1  33261  mndractfo  33262  gsumfs2d  33294  gsumhashmul  33300  suppgsumssiun  33305  xrge0tsmsd  33306  gsumwun  33309  psgnfzto1stlem  33333  cycpmco2  33366  cycpmrn  33376  tocyccntz  33377  cycpmconjslem2  33388  cyc3conja  33390  conjga  33403  submarchi  33419  isarchiofld  33432  elrgspnlem1  33475  elrgspnlem2  33476  elrgspnlem3  33477  elrgspnlem4  33478  elrgspnsubrunlem1  33480  elrgspnsubrunlem2  33481  elrgspnsubrun  33482  erlval  33491  erler  33498  rloccring  33504  rlocf1  33507  rlocisunit  33509  domnprodn0  33511  domnprodeq0  33512  subrdom  33518  imaslmod  33588  znfermltl  33596  lindfpropd  33611  unitprodclb  33618  nsgmgc  33637  nsgqusf1olem1  33638  unitpidl1  33648  elrspunidl  33652  elrspunsn  33653  rhmimaidl  33656  drngidl  33657  mxidlprm  33670  mxidlirredi  33671  drngmxidlr  33677  qsdrngilem  33693  qsdrngi  33694  drnglring  33699  dflringlem2  33702  dflring3  33704  dflring4  33705  rsprprmprmidl  33729  rsprprmprmidlb  33730  rprmasso2  33733  rprmirred  33738  rprmirredb  33739  rprmdvdspow  33740  1arithidom  33744  pidufd  33750  1arithufdlem3  33753  dfufd2  33757  deg1prod  33790  ply1dg3rt0irred  33791  0mplrim  33821  mplidomlem  33834  extvfvcl  33843  mplvrpmga  33852  mplvrpmmhm  33853  mplvrpmrhm  33854  psrgsum  33855  psrmonprod  33859  esplymhp  33875  esplyfval3  33879  esplyfval1  33880  esplyfvaln  33881  esplyind  33882  exsslsb  33904  lbslelsp  33905  ply1degltdimlem  33929  lindsunlem  33931  lindsun  33932  lbsdiflsp0  33933  dimkerim  33934  fedgmul  33938  dimlssid  33939  assalactf1o  33942  extdg1id  33973  evls1fldgencl  33977  fldextrspunlsplem  33980  fldextrspunlsp  33981  extdgfialglem1  33999  minplyirred  34018  fldext2chn  34035  cos9thpiminplylem2  34090  smatrcl  34103  1smat1  34111  submateq  34116  mdetpmtr1  34130  madjusmdetlem2  34135  locfinreflem  34147  cmppcmp  34165  rhmpreimacn  34192  ordtrest2NEWlem  34229  ordtconnlem1  34231  lmdvg  34260  zrhcntr  34286  esumpcvgval  34385  esum2d  34400  sigapildsys  34469  ldgenpisyslem1  34470  fiunelros  34481  volmeas  34538  imambfm  34569  omssubadd  34607  carsggect  34625  carsgclctunlem3  34627  signsply0  34855  signstres  34879  actfunsnf1o  34908  actfunsnrndisj  34909  reprsuc  34919  reprinfz1  34926  breprexplema  34934  breprexplemc  34936  breprexp  34937  breprexpnat  34938  circlemeth  34944  hgt750lemb  34960  tgoldbachgtd  34966  erdszelem8  35561  pconnconn  35594  cvmlift2lem12  35677  cvmlift3lem5  35686  cvmlift3lem7  35688  cvmlift3lem8  35689  fmla1  35750  mrsubrn  35876  msrval  35901  msubff1  35919  btwnconn1lem13  36462  elicc3  36690  neibastop2lem  36733  weiunfr  36840  unbdqndv2  36962  irrdifflemf  37829  ltflcei  38119  lindsenlbs  38126  matunitlindflem1  38127  matunitlindflem2  38128  poimirlem4  38135  poimirlem13  38144  poimirlem14  38145  poimirlem22  38153  poimirlem26  38157  poimirlem27  38158  heicant  38166  mblfinlem2  38169  mblfinlem3  38170  mblfinlem4  38171  cnambfre  38179  itg2addnclem  38182  itg2addnclem2  38183  itg2gt0cn  38186  ftc1cnnc  38203  ftc1anclem5  38208  ftc1anclem7  38210  ftc1anc  38212  equivtotbnd  38289  isbndx  38293  ssbnd  38299  heibor1lem  38320  rrncmslem  38343  islshpat  39653  lfl1dim  39757  lfl1dim2N  39758  lkrpssN  39799  glbconN  40013  hlhgt2  40025  3dim2  40104  3dim3  40105  islln3  40146  islvol5  40215  2lplnja  40255  dalem19  40318  isline4N  40413  2polssN  40551  lhpmatb  40667  4atex  40712  trlatn0  40808  cdlemf2  41198  dialss  41682  diaglbN  41691  diaintclN  41694  dibglbN  41802  dibintclN  41803  dihlsscpre  41870  dihglblem5aN  41928  dihglblem2aN  41929  dihglblem4  41933  dihatexv  41974  dihjat1lem  42064  lcfl6  42136  mapdval2N  42266  aks4d1p8  42716  fldhmf1  42719  primrootscoprmpow  42728  primrootscoprbij2  42732  primrootspoweq0  42735  evl1gprodd  42746  hashscontpow  42751  aks6d1c2lem4  42756  idomnnzgmulnz  42762  deg1gprod  42769  sticksstones8  42782  sticksstones12a  42786  aks6d1c6lem3  42801  aks6d1c6lem5  42806  aks6d1c7  42813  aks5lem5a  42820  unitscyglem2  42825  sn-0tie0  43085  imacrhmcl  43148  fiabv  43166  evlselv  43183  fsuppind  43184  prjspertr  43199  prjspreln0  43203  prjspner1  43220  elrfi  43287  eldioph2  43355  diophin  43365  irrapxlem2  43412  irrapxlem3  43413  irrapxlem4  43414  irrapxlem5  43415  pell1234qrne0  43442  pell1234qrreccl  43443  pell1234qrmulcl  43444  pell14qrgt0  43448  pell14qrdich  43458  pell1qrge1  43459  pellfundex  43475  congabseq  43563  jm2.27b  43595  jm2.27  43597  fnwe2lem2  43640  kelac1  43652  lnrfg  43708  hbt  43719  omabs2  43921  nadd1suc  43981  rfovcnvf1od  44592  ntrneiiso  44679  ntrneikb  44682  ntrneixb  44683  ntrneik3  44684  ntrneix3  44685  ntrneik13  44686  ntrneix13  44687  cvgdvgrat  44887  binomcxplemnotnn0  44930  sineq0ALT  45510  fnchoice  45607  disjf1  45759  supxrgere  45907  supxrgelem  45911  supxrge  45912  suplesup  45913  xralrple2  45928  infxr  45940  infleinflem2  45944  infleinf  45945  uzub  46003  mccl  46172  limcrecl  46203  lptioo2  46205  lptioo1  46206  lptre2pt  46212  addlimc  46220  limsupmnflem  46292  climxrre  46322  liminflimsupclim  46379  climxlim2lem  46417  xlimliminflimsup  46434  icccncfext  46459  cncfiooicclem1  46465  cncfiooiccre  46467  dvbdfbdioolem2  46501  ioodvbdlimc1lem1  46503  dvnxpaek  46514  dvmptfprodlem  46516  dvmptfprod  46517  dvnprodlem3  46520  itgioocnicc  46549  itgspltprt  46551  stoweidlem31  46603  fourierdlem39  46718  fourierdlem42  46721  fourierdlem48  46726  fourierdlem49  46727  fourierdlem50  46728  fourierdlem51  46729  fourierdlem64  46742  fourierdlem65  46743  fourierdlem74  46752  fourierdlem75  46753  fourierdlem81  46759  fourierdlem82  46760  fourierdlem101  46779  etransclem23  46829  etransclem27  46833  etransclem32  46838  etransclem33  46839  etransclem35  46841  etransclem38  46844  sge0tsms  46952  sge0cl  46953  sge0f1o  46954  sge0split  46981  sge0rpcpnf  46993  sge0seq  47018  nnfoctbdjlem  47027  iundjiun  47032  meaiuninc3v  47056  meaiininclem  47058  omeiunltfirp  47091  carageniuncllem2  47094  carageniuncl  47095  hoicvr  47120  hoidmv1lelem1  47163  hoidmvlelem3  47169  hoidmvlelem5  47171  hoidmvle  47172  hoiqssbllem3  47196  iunhoiioolem  47247  pimdecfgtioo  47289  pimincfltioo  47290  preimageiingt  47292  preimaleiinlt  47293  smflimlem4  47346  chnerlem1  47456  iccpartigtl  48027  iccpartgt  48031  sprsymrelf1lem  48095  paireqne  48115  proththd  48221  requad2  48243  sbgoldbst  48398  bgoldbtbndlem4  48428  isuspgrim0lem  48513  isuspgrim0  48514  isuspgrimlem  48515  gricushgr  48537  grimedg  48555  grimgrtri  48569  isubgr3stgrlem7  48592  gpgusgralem  48676  pgn4cyclex  48746  2zrngmmgm  48872  cznrng  48881  rhmsubcALTVlem4  48904  srhmsubcALTV  48945  lincsum  49060  lcoss  49067  snlindsntor  49102  islindeps2  49114  line2x  49385  line2y  49386  itscnhlinecirc02p  49416  discsubc  49693  imasubc3  49785  uppropd  49810  swapfval  49891  fucofvalg  49947  fuco21  49965  precofvalALT  49997  2arwcat  50229  lanup  50270  ranup  50271