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  7239  fimaproj  8087  frxp3  8103  oaabs  8586  oaabs2  8587  omabs  8589  cofon1  8610  sbthlem8  9034  cantnfle  9592  cantnfp1  9602  cantnflem1c  9608  sornom  10199  enfin2i  10243  ttukeylem6  10436  fpwwe2lem12  10565  fpwwe2  10566  winalim2  10619  wuncval2  10670  negf1o  11579  xlemul1a  13215  difreicc  13412  flflp1  13739  faclbnd  14225  swrdswrd  14640  swrdccatin1  14660  pfxccatin12lem3  14667  swrdccat3blem  14674  ello12  15451  lo1bdd2  15459  elo12  15462  rlimclim1  15480  rlimcld2  15513  o1co  15521  o1of2  15548  o1rlimmul  15554  rlimsqzlem  15584  isercoll  15603  o1fsum  15748  supcvg  15791  dvds2ln  16228  lcmgcdlem  16545  cncongr2  16607  isprm5  16646  prmdvdsncoprmbd  16666  pcadd  16829  vdwlem2  16922  vdwlem11  16931  sbcie3s  17101  prdsval  17387  mreexexlem4d  17582  isacs2  17588  catcocl  17620  catass  17621  subccocl  17781  fullsubc  17786  funcco  17807  funcpropd  17838  fullpropd  17858  ffthiso  17867  isnat  17886  natpropd  17915  fucpropd  17916  xpcval  18112  evlf2  18153  curfpropd  18168  curfuncf  18173  uncfcurf  18174  curf2ndf  18182  hofcl  18194  hofpropd  18202  yonffthlem  18217  isacs3lem  18477  acsfiindd  18488  chnind  18556  gsumpropd2lem  18616  resmgmhm2b  18650  resmhm2b  18759  mhmid  19005  mhmmnd  19006  ghmgrp  19008  conjnmzb  19194  ghmqusnsg  19223  ghmquskerlem3  19227  ghmqusker  19228  pgpfi  19546  sylow3lem2  19569  efgredlem  19688  frgpnabllem1  19814  imasabl  19817  dprdfcntz  19958  ablfac1b  20013  pgpfac1lem3  20020  pgpfac1lem5  20022  pgpfaclem3  20026  omndmul2  20074  gsumle  20086  ringinvnzdiv  20248  rnghmsubcsetclem2  20577  rhmsubcsetclem2  20606  srhmsubc  20625  rhmsubclem4  20633  imadrhmcl  20742  cntzsdrg  20747  suborng  20821  islmhm2  21002  lspsneleq  21082  rhmpreimaidl  21244  znunit  21530  psgndiflemB  21567  uvcff  21758  uvcf1  21759  lindfmm  21794  sraassab  21835  psrval  21883  psrass1  21931  resspsrmul  21943  mplbas2  22009  evlsvvval  22060  mhpmulcl  22104  psdmul  22121  coe1tmmul  22231  gsummoncoe1  22264  evls1fpws  22325  dmatsubcl  22454  scmatscm  22469  smatvscl  22480  marrepval  22518  mdetdiaglem  22554  mdetunilem8  22575  mdetunilem9  22576  pmatcoe1fsupp  22657  decpmatmulsumfsupp  22729  pmatcollpw2lem  22733  mp2pm2mplem4  22765  pm2mpmhmlem1  22774  pm2mpmhmlem2  22775  pm2mp  22781  fvmptnn04if  22805  cpmadugsumfi  22833  cpmidg2sum  22836  cpmadumatpoly  22839  cayhamlem4  22844  neiptoptop  23087  neitr  23136  ordtrest2lem  23159  cnpnei  23220  iscncl  23225  cncls  23230  cnntr  23231  cncnp  23236  lmcnp  23260  isreg2  23333  hauscmplem  23362  cmpfi  23364  1stcfb  23401  1stcrest  23409  2ndcctbss  23411  2ndcomap  23414  islly2  23440  cldllycmp  23451  lly1stc  23452  locfincmp  23482  llycmpkgen2  23506  1stckgenlem  23509  kgencn2  23513  kgencn3  23514  ptbasfi  23537  ptpjopn  23568  txdis1cn  23591  txlly  23592  txnlly  23593  txtube  23596  txcmplem2  23598  tx1stc  23606  txkgen  23608  xkopt  23611  xkoco2cn  23614  xkococnlem  23615  xkococn  23616  xkoinjcn  23643  tgqtop  23668  regr1lem  23695  kqreglem1  23697  nrmhmph  23750  rnelfmlem  23908  rnelfm  23909  fmfnfmlem4  23913  fmfnfm  23914  ufldom  23918  flimopn  23931  hauspwpwf1  23943  fclsopn  23970  fclsnei  23975  fclsrest  23980  alexsublem  24000  alexsubALTlem3  24005  ptcmplem2  24009  ptcmplem3  24010  cnextfun  24020  cnextcn  24023  symgtgp  24062  tgpt0  24075  qustgpopn  24076  tsmsxplem1  24109  trust  24185  utopsnneiplem  24203  utop3cls  24207  utopreg  24208  isucn2  24234  cstucnd  24239  ucncn  24240  fmucnd  24247  cfilufg  24248  neipcfilu  24251  met2ndci  24478  prdsxmslem2  24485  metcnp3  24496  metustid  24510  metustexhalf  24512  metust  24514  psmetutop  24523  nmoleub  24687  reconnlem2  24784  xrge0tsms  24791  cncfco  24868  lebnumlem3  24930  lebnum  24931  nmoleub2lem2  25084  nmoleub3  25087  iscfil2  25234  iscau4  25247  iscmet3lem2  25260  equivcfil  25267  equivcau  25268  caubl  25276  rrxdstprj1  25377  ovolshftlem2  25479  ovolicc2lem4  25489  uniioombl  25558  i1fmulclem  25671  mbfi1fseqlem6  25689  itg2const2  25710  itg2split  25718  bddiblnc  25811  ellimc2  25846  ellimc3  25848  limcflf  25850  dvmptfsum  25947  dvferm1  25957  dvferm2  25959  dvlip2  25968  c1lip1  25970  lhop1  25987  ftc1a  26012  ply1divex  26110  plyeq0lem  26183  plymullem1  26187  coemullem  26223  coemulc  26228  ulmshftlem  26366  ulmcaulem  26371  ulmbdd  26375  ulmcn  26376  ulmdvlem3  26379  mtestbdd  26382  pserulm  26399  pserdvlem2  26406  abelthlem8  26417  xrlimcnp  26946  jensen  26967  lgamucov  27016  logfac2  27196  dchrelbas3  27217  dchrpt  27246  gausslemma2dlem1a  27344  lgsquad3  27366  2sqb  27411  rpvmasumlem  27466  dchrisumlem1  27468  dchrisumlem3  27470  dchrmusum2  27473  dchrvmasumlem2  27477  dchrisum0flblem1  27487  dchrisum0lem1b  27494  dchrisum0lem1  27495  dchrisum0  27499  mulog2sumlem2  27514  pntlem3  27588  ostth3  27617  lesrec  27807  cofcutr  27932  remulscllem2  28509  istrkgcb  28540  tgbtwndiff  28590  iscgrglt  28598  tgcgrxfr  28602  motcgrg  28628  lnext  28651  tgbtwnconn1  28659  tgbtwnconn3  28661  legval  28668  legtrid  28675  legso  28683  hlcgreu  28702  tglnne  28712  tglineeltr  28715  tglnne0  28724  colline  28733  tglowdim2l  28734  tglowdim2ln  28735  mirreu3  28738  mirbtwnhl  28764  krippenlem  28774  midexlem  28776  perpcom  28797  perpneq  28798  footexALT  28802  footex  28805  colperpexlem3  28816  colperpex  28817  opphllem  28819  midex  28821  oppne3  28827  opptgdim2  28829  oppnid  28830  opphllem2  28832  opphllem5  28835  opphllem6  28836  oppperpex  28837  outpasch  28839  hlpasch  28840  lnopp2hpgb  28847  hpgerlem  28849  colopp  28853  colhp  28854  lmieu  28868  lnperpex  28887  trgcopy  28888  trgcopyeulem  28889  iscgra1  28894  cgrane1  28896  cgrane2  28897  cgrane3  28898  cgrane4  28899  cgrahl1  28900  cgrahl2  28901  cgracgr  28902  cgraswap  28904  cgracom  28906  cgratr  28907  flatcgra  28908  cgrabtwn  28910  cgrahl  28911  sacgr  28915  acopyeu  28918  cgrg3col4  28937  tgasa1  28942  f1otrg  28955  f1otrge  28956  axeuclidlem  29047  axcontlem2  29050  umgrvad2edg  29298  usgredg2vlem2  29311  pthdepisspth  29820  clwwlkccatlem  30076  clwlkclwwlklem2  30087  3cycld  30265  eupth2lems  30325  eucrctshift  30330  frgr3vlem2  30361  n4cyclfrgr  30378  numclwwlk1lem2f1  30444  numclwwlk2lem1  30463  ubthlem3  30959  chirredlem1  32477  chirredlem3  32479  cdj1i  32520  fnpreimac  32759  xrge0infss  32850  nn0xmulclb  32861  hashxpe  32897  sgnmul  32926  2exple2exp  32936  ccatf1  33041  ccatws1f1o  33043  swrdf1  33048  dfmgc2lem  33087  mgcf1o  33095  mndlactf1  33118  mndlactfo  33119  mndractf1  33120  mndractfo  33121  gsumfs2d  33154  gsumhashmul  33160  suppgsumssiun  33165  xrge0tsmsd  33166  gsumwun  33169  psgnfzto1stlem  33193  cycpmco2  33226  cycpmrn  33236  tocyccntz  33237  cycpmconjslem2  33248  cyc3conja  33250  conjga  33263  submarchi  33279  isarchiofld  33292  elrgspnlem1  33335  elrgspnlem2  33336  elrgspnlem3  33337  elrgspnlem4  33338  elrgspnsubrunlem1  33340  elrgspnsubrunlem2  33341  elrgspnsubrun  33342  erlval  33351  erler  33358  rloccring  33363  rlocf1  33366  domnprodn0  33368  domnprodeq0  33369  subrdom  33378  imaslmod  33445  znfermltl  33458  lindfpropd  33474  unitprodclb  33481  nsgmgc  33504  nsgqusf1olem1  33505  unitpidl1  33516  elrspunidl  33520  elrspunsn  33521  rhmimaidl  33524  drngidl  33525  qsidomlem1  33544  mxidlprm  33562  mxidlirredi  33563  drngmxidlr  33570  qsdrngilem  33586  qsdrngi  33587  rsprprmprmidl  33614  rsprprmprmidlb  33615  rprmasso2  33618  rprmirred  33623  rprmirredb  33624  rprmdvdspow  33625  1arithidom  33629  pidufd  33635  1arithufdlem3  33638  dfufd2  33642  deg1prod  33675  ply1dg3rt0irred  33676  extvfvcl  33712  mplvrpmga  33721  mplvrpmmhm  33722  mplvrpmrhm  33723  psrgsum  33724  psrmonprod  33728  esplymhp  33744  esplyfval3  33748  esplyfval1  33749  esplyfvaln  33750  esplyind  33751  exsslsb  33773  lbslelsp  33774  ply1degltdimlem  33799  lindsunlem  33801  lindsun  33802  lbsdiflsp0  33803  dimkerim  33804  fedgmul  33808  dimlssid  33809  assalactf1o  33812  extdg1id  33843  evls1fldgencl  33847  fldextrspunlsplem  33850  fldextrspunlsp  33851  extdgfialglem1  33869  minplyirred  33888  fldext2chn  33905  cos9thpiminplylem2  33960  smatrcl  33973  1smat1  33981  submateq  33986  mdetpmtr1  34000  madjusmdetlem2  34005  locfinreflem  34017  cmppcmp  34035  rhmpreimacn  34062  ordtrest2NEWlem  34099  ordtconnlem1  34101  lmdvg  34130  zrhcntr  34156  esumpcvgval  34255  esum2d  34270  sigapildsys  34339  ldgenpisyslem1  34340  fiunelros  34351  volmeas  34408  imambfm  34439  omssubadd  34477  carsggect  34495  carsgclctunlem3  34497  signsply0  34728  signstres  34752  actfunsnf1o  34781  actfunsnrndisj  34782  reprsuc  34792  reprinfz1  34799  breprexplema  34807  breprexplemc  34809  breprexp  34810  breprexpnat  34811  circlemeth  34817  hgt750lemb  34833  tgoldbachgtd  34839  erdszelem8  35411  pconnconn  35444  cvmlift2lem12  35527  cvmlift3lem5  35536  cvmlift3lem7  35538  cvmlift3lem8  35539  fmla1  35600  mrsubrn  35726  msrval  35751  msubff1  35769  btwnconn1lem13  36312  elicc3  36530  neibastop2lem  36573  weiunfr  36680  unbdqndv2  36730  irrdifflemf  37574  ltflcei  37853  lindsenlbs  37860  matunitlindflem1  37861  matunitlindflem2  37862  poimirlem4  37869  poimirlem13  37878  poimirlem14  37879  poimirlem22  37887  poimirlem26  37891  poimirlem27  37892  heicant  37900  mblfinlem2  37903  mblfinlem3  37904  mblfinlem4  37905  cnambfre  37913  itg2addnclem  37916  itg2addnclem2  37917  itg2gt0cn  37920  ftc1cnnc  37937  ftc1anclem5  37942  ftc1anclem7  37944  ftc1anc  37946  equivtotbnd  38023  isbndx  38027  ssbnd  38033  heibor1lem  38054  rrncmslem  38077  islshpat  39387  lfl1dim  39491  lfl1dim2N  39492  lkrpssN  39533  glbconN  39747  hlhgt2  39759  3dim2  39838  3dim3  39839  islln3  39880  islvol5  39949  2lplnja  39989  dalem19  40052  isline4N  40147  2polssN  40285  lhpmatb  40401  4atex  40446  trlatn0  40542  cdlemf2  40932  dialss  41416  diaglbN  41425  diaintclN  41428  dibglbN  41536  dibintclN  41537  dihlsscpre  41604  dihglblem5aN  41662  dihglblem2aN  41663  dihglblem4  41667  dihatexv  41708  dihjat1lem  41798  lcfl6  41870  mapdval2N  42000  aks4d1p8  42451  fldhmf1  42454  primrootscoprmpow  42463  primrootscoprbij2  42467  primrootspoweq0  42470  evl1gprodd  42481  hashscontpow  42486  aks6d1c2lem4  42491  idomnnzgmulnz  42497  deg1gprod  42504  sticksstones8  42517  sticksstones12a  42521  aks6d1c6lem3  42536  aks6d1c6lem5  42541  aks6d1c7  42548  aks5lem5a  42555  unitscyglem2  42560  sn-0tie0  42815  imacrhmcl  42878  fiabv  42900  evlselv  42939  fsuppind  42942  prjspertr  42957  prjspreln0  42961  prjspner1  42978  elrfi  43045  eldioph2  43113  diophin  43123  irrapxlem2  43174  irrapxlem3  43175  irrapxlem4  43176  irrapxlem5  43177  pell1234qrne0  43204  pell1234qrreccl  43205  pell1234qrmulcl  43206  pell14qrgt0  43210  pell14qrdich  43220  pell1qrge1  43221  pellfundex  43237  congabseq  43325  jm2.27b  43357  jm2.27  43359  fnwe2lem2  43402  kelac1  43414  lnrfg  43470  hbt  43481  omabs2  43683  nadd1suc  43743  rfovcnvf1od  44354  ntrneiiso  44441  ntrneikb  44444  ntrneixb  44445  ntrneik3  44446  ntrneix3  44447  ntrneik13  44448  ntrneix13  44449  cvgdvgrat  44663  binomcxplemnotnn0  44706  sineq0ALT  45286  fnchoice  45383  disjf1  45536  supxrgere  45686  supxrgelem  45690  supxrge  45691  suplesup  45692  xralrple2  45707  infxr  45719  infleinflem2  45723  infleinf  45724  uzub  45783  mccl  45952  limcrecl  45983  lptioo2  45985  lptioo1  45986  lptre2pt  45992  addlimc  46000  limsupmnflem  46072  climxrre  46102  liminflimsupclim  46159  climxlim2lem  46197  xlimliminflimsup  46214  icccncfext  46239  cncfiooicclem1  46245  cncfiooiccre  46247  dvbdfbdioolem2  46281  ioodvbdlimc1lem1  46283  dvnxpaek  46294  dvmptfprodlem  46296  dvmptfprod  46297  dvnprodlem3  46300  itgioocnicc  46329  itgspltprt  46331  stoweidlem31  46383  fourierdlem39  46498  fourierdlem42  46501  fourierdlem48  46506  fourierdlem49  46507  fourierdlem50  46508  fourierdlem51  46509  fourierdlem64  46522  fourierdlem65  46523  fourierdlem74  46532  fourierdlem75  46533  fourierdlem81  46539  fourierdlem82  46540  fourierdlem101  46559  etransclem23  46609  etransclem27  46613  etransclem32  46618  etransclem33  46619  etransclem35  46621  etransclem38  46624  sge0tsms  46732  sge0cl  46733  sge0f1o  46734  sge0split  46761  sge0rpcpnf  46773  sge0seq  46798  nnfoctbdjlem  46807  iundjiun  46812  meaiuninc3v  46836  meaiininclem  46838  omeiunltfirp  46871  carageniuncllem2  46874  carageniuncl  46875  hoidmv1lelem1  46943  hoidmvlelem3  46949  hoidmvlelem5  46951  hoidmvle  46952  hoiqssbllem3  46976  iunhoiioolem  47027  pimdecfgtioo  47069  pimincfltioo  47070  preimageiingt  47072  preimaleiinlt  47073  smflimlem4  47126  chnerlem1  47234  iccpartigtl  47777  iccpartgt  47781  sprsymrelf1lem  47845  paireqne  47865  proththd  47968  requad2  47977  sbgoldbst  48132  bgoldbtbndlem4  48162  isuspgrim0lem  48247  isuspgrim0  48248  isuspgrimlem  48249  gricushgr  48271  grimedg  48289  grimgrtri  48303  isubgr3stgrlem7  48326  gpgusgralem  48410  pgn4cyclex  48480  2zrngmmgm  48606  cznrng  48615  rhmsubcALTVlem4  48638  srhmsubcALTV  48679  lincsum  48783  lcoss  48790  snlindsntor  48825  islindeps2  48837  line2x  49108  line2y  49109  itscnhlinecirc02p  49139  discsubc  49417  imasubc3  49509  uppropd  49534  swapfval  49615  fucofvalg  49671  fuco21  49689  precofvalALT  49721  2arwcat  49953  lanup  49994  ranup  49995