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  7224  fimaproj  8075  frxp3  8091  oaabs  8573  oaabs2  8574  omabs  8576  cofon1  8597  sbthlem8  9018  findcard3OLD  9188  cantnfle  9586  cantnfp1  9596  cantnflem1c  9602  sornom  10190  enfin2i  10234  ttukeylem6  10427  fpwwe2lem12  10555  fpwwe2  10556  winalim2  10609  wuncval2  10660  negf1o  11568  xlemul1a  13208  difreicc  13405  flflp1  13729  faclbnd  14215  swrdswrd  14629  swrdccatin1  14649  pfxccatin12lem3  14656  swrdccat3blem  14663  ello12  15441  lo1bdd2  15449  elo12  15452  rlimclim1  15470  rlimcld2  15503  o1co  15511  o1of2  15538  o1rlimmul  15544  rlimsqzlem  15574  isercoll  15593  o1fsum  15738  supcvg  15781  dvds2ln  16218  lcmgcdlem  16535  cncongr2  16597  isprm5  16636  prmdvdsncoprmbd  16656  pcadd  16819  vdwlem2  16912  vdwlem11  16921  sbcie3s  17091  prdsval  17377  mreexexlem4d  17571  isacs2  17577  catcocl  17609  catass  17610  subccocl  17770  fullsubc  17775  funcco  17796  funcpropd  17827  fullpropd  17847  ffthiso  17856  isnat  17875  natpropd  17904  fucpropd  17905  xpcval  18101  evlf2  18142  curfpropd  18157  curfuncf  18162  uncfcurf  18163  curf2ndf  18171  hofcl  18183  hofpropd  18191  yonffthlem  18206  isacs3lem  18466  acsfiindd  18477  gsumpropd2lem  18571  resmgmhm2b  18605  resmhm2b  18714  mhmid  18960  mhmmnd  18961  ghmgrp  18963  conjnmzb  19150  ghmqusnsg  19179  ghmquskerlem3  19183  ghmqusker  19184  pgpfi  19502  sylow3lem2  19525  efgredlem  19644  frgpnabllem1  19770  imasabl  19773  dprdfcntz  19914  ablfac1b  19969  pgpfac1lem3  19976  pgpfac1lem5  19978  pgpfaclem3  19982  omndmul2  20030  gsumle  20042  ringinvnzdiv  20204  rnghmsubcsetclem2  20535  rhmsubcsetclem2  20564  srhmsubc  20583  rhmsubclem4  20591  imadrhmcl  20700  cntzsdrg  20705  suborng  20779  islmhm2  20960  lspsneleq  21040  rhmpreimaidl  21202  znunit  21488  psgndiflemB  21525  uvcff  21716  uvcf1  21717  lindfmm  21752  sraassab  21793  psrval  21840  psrass1  21889  resspsrmul  21901  mplbas2  21965  mhpmulcl  22052  psdmul  22069  coe1tmmul  22179  gsummoncoe1  22211  evls1fpws  22272  dmatsubcl  22401  scmatscm  22416  smatvscl  22427  marrepval  22465  mdetdiaglem  22501  mdetunilem8  22522  mdetunilem9  22523  pmatcoe1fsupp  22604  decpmatmulsumfsupp  22676  pmatcollpw2lem  22680  mp2pm2mplem4  22712  pm2mpmhmlem1  22721  pm2mpmhmlem2  22722  pm2mp  22728  fvmptnn04if  22752  cpmadugsumfi  22780  cpmidg2sum  22783  cpmadumatpoly  22786  cayhamlem4  22791  neiptoptop  23034  neitr  23083  ordtrest2lem  23106  cnpnei  23167  iscncl  23172  cncls  23177  cnntr  23178  cncnp  23183  lmcnp  23207  isreg2  23280  hauscmplem  23309  cmpfi  23311  1stcfb  23348  1stcrest  23356  2ndcctbss  23358  2ndcomap  23361  islly2  23387  cldllycmp  23398  lly1stc  23399  locfincmp  23429  llycmpkgen2  23453  1stckgenlem  23456  kgencn2  23460  kgencn3  23461  ptbasfi  23484  ptpjopn  23515  txdis1cn  23538  txlly  23539  txnlly  23540  txtube  23543  txcmplem2  23545  tx1stc  23553  txkgen  23555  xkopt  23558  xkoco2cn  23561  xkococnlem  23562  xkococn  23563  xkoinjcn  23590  tgqtop  23615  regr1lem  23642  kqreglem1  23644  nrmhmph  23697  rnelfmlem  23855  rnelfm  23856  fmfnfmlem4  23860  fmfnfm  23861  ufldom  23865  flimopn  23878  hauspwpwf1  23890  fclsopn  23917  fclsnei  23922  fclsrest  23927  alexsublem  23947  alexsubALTlem3  23952  ptcmplem2  23956  ptcmplem3  23957  cnextfun  23967  cnextcn  23970  symgtgp  24009  tgpt0  24022  qustgpopn  24023  tsmsxplem1  24056  trust  24133  utopsnneiplem  24151  utop3cls  24155  utopreg  24156  isucn2  24182  cstucnd  24187  ucncn  24188  fmucnd  24195  cfilufg  24196  neipcfilu  24199  met2ndci  24426  prdsxmslem2  24433  metcnp3  24444  metustid  24458  metustexhalf  24460  metust  24462  psmetutop  24471  nmoleub  24635  reconnlem2  24732  xrge0tsms  24739  cncfco  24816  lebnumlem3  24878  lebnum  24879  nmoleub2lem2  25032  nmoleub3  25035  iscfil2  25182  iscau4  25195  iscmet3lem2  25208  equivcfil  25215  equivcau  25216  caubl  25224  rrxdstprj1  25325  ovolshftlem2  25427  ovolicc2lem4  25437  uniioombl  25506  i1fmulclem  25619  mbfi1fseqlem6  25637  itg2const2  25658  itg2split  25666  bddiblnc  25759  ellimc2  25794  ellimc3  25796  limcflf  25798  dvmptfsum  25895  dvferm1  25905  dvferm2  25907  dvlip2  25916  c1lip1  25918  lhop1  25935  ftc1a  25960  ply1divex  26058  plyeq0lem  26131  plymullem1  26135  coemullem  26171  coemulc  26176  ulmshftlem  26314  ulmcaulem  26319  ulmbdd  26323  ulmcn  26324  ulmdvlem3  26327  mtestbdd  26330  pserulm  26347  pserdvlem2  26354  abelthlem8  26365  xrlimcnp  26894  jensen  26915  lgamucov  26964  logfac2  27144  dchrelbas3  27165  dchrpt  27194  gausslemma2dlem1a  27292  lgsquad3  27314  2sqb  27359  rpvmasumlem  27414  dchrisumlem1  27416  dchrisumlem3  27418  dchrmusum2  27421  dchrvmasumlem2  27425  dchrisum0flblem1  27435  dchrisum0lem1b  27442  dchrisum0lem1  27443  dchrisum0  27447  mulog2sumlem2  27462  pntlem3  27536  ostth3  27565  slerec  27748  cofcutr  27855  remulscllem2  28388  istrkgcb  28419  tgbtwndiff  28469  iscgrglt  28477  tgcgrxfr  28481  motcgrg  28507  lnext  28530  tgbtwnconn1  28538  tgbtwnconn3  28540  legval  28547  legtrid  28554  legso  28562  hlcgreu  28581  tglnne  28591  tglineeltr  28594  tglnne0  28603  colline  28612  tglowdim2l  28613  tglowdim2ln  28614  mirreu3  28617  mirbtwnhl  28643  krippenlem  28653  midexlem  28655  perpcom  28676  perpneq  28677  footexALT  28681  footex  28684  colperpexlem3  28695  colperpex  28696  opphllem  28698  midex  28700  oppne3  28706  opptgdim2  28708  oppnid  28709  opphllem2  28711  opphllem5  28714  opphllem6  28715  oppperpex  28716  outpasch  28718  hlpasch  28719  lnopp2hpgb  28726  hpgerlem  28728  colopp  28732  colhp  28733  lmieu  28747  lnperpex  28766  trgcopy  28767  trgcopyeulem  28768  iscgra1  28773  cgrane1  28775  cgrane2  28776  cgrane3  28777  cgrane4  28778  cgrahl1  28779  cgrahl2  28780  cgracgr  28781  cgraswap  28783  cgracom  28785  cgratr  28786  flatcgra  28787  cgrabtwn  28789  cgrahl  28790  sacgr  28794  acopyeu  28797  cgrg3col4  28816  tgasa1  28821  f1otrg  28834  f1otrge  28835  axeuclidlem  28925  axcontlem2  28928  umgrvad2edg  29176  usgredg2vlem2  29189  pthdepisspth  29698  clwwlkccatlem  29951  clwlkclwwlklem2  29962  3cycld  30140  eupth2lems  30200  eucrctshift  30205  frgr3vlem2  30236  n4cyclfrgr  30253  numclwwlk1lem2f1  30319  numclwwlk2lem1  30338  ubthlem3  30834  chirredlem1  32352  chirredlem3  32354  cdj1i  32395  fnpreimac  32628  xrge0infss  32716  nn0xmulclb  32727  hashxpe  32765  sgnmul  32793  2exple2exp  32803  ccatf1  32903  ccatws1f1o  32906  swrdf1  32911  dfmgc2lem  32950  mgcf1o  32958  chnind  32966  mndlactf1  32993  mndlactfo  32994  mndractf1  32995  mndractfo  32996  gsumfs2d  33021  gsumhashmul  33027  xrge0tsmsd  33028  gsumwun  33031  psgnfzto1stlem  33055  cycpmco2  33088  cycpmrn  33098  tocyccntz  33099  cycpmconjslem2  33110  cyc3conja  33112  conjga  33125  submarchi  33138  isarchiofld  33151  elrgspnlem1  33192  elrgspnlem2  33193  elrgspnlem3  33194  elrgspnlem4  33195  elrgspnsubrunlem1  33197  elrgspnsubrunlem2  33198  elrgspnsubrun  33199  erlval  33208  erler  33215  rloccring  33220  rlocf1  33223  domnprodn0  33225  subrdom  33234  imaslmod  33300  znfermltl  33313  lindfpropd  33329  unitprodclb  33336  nsgmgc  33359  nsgqusf1olem1  33360  unitpidl1  33371  elrspunidl  33375  elrspunsn  33376  rhmimaidl  33379  drngidl  33380  qsidomlem1  33399  mxidlprm  33417  mxidlirredi  33418  drngmxidlr  33425  qsdrngilem  33441  qsdrngi  33442  rsprprmprmidl  33469  rsprprmprmidlb  33470  rprmasso2  33473  rprmirred  33478  rprmirredb  33479  rprmdvdspow  33480  1arithidom  33484  pidufd  33490  1arithufdlem3  33493  dfufd2  33497  ply1dg3rt0irred  33527  exsslsb  33568  lbslelsp  33569  ply1degltdimlem  33594  lindsunlem  33596  lindsun  33597  lbsdiflsp0  33598  dimkerim  33599  fedgmul  33603  dimlssid  33604  assalactf1o  33607  extdg1id  33637  evls1fldgencl  33641  fldextrspunlsplem  33644  fldextrspunlsp  33645  minplyirred  33677  fldext2chn  33694  cos9thpiminplylem2  33749  smatrcl  33762  1smat1  33770  submateq  33775  mdetpmtr1  33789  madjusmdetlem2  33794  locfinreflem  33806  cmppcmp  33824  rhmpreimacn  33851  ordtrest2NEWlem  33888  ordtconnlem1  33890  lmdvg  33919  zrhcntr  33945  esumpcvgval  34044  esum2d  34059  sigapildsys  34128  ldgenpisyslem1  34129  fiunelros  34140  volmeas  34197  imambfm  34229  omssubadd  34267  carsggect  34285  carsgclctunlem3  34287  signsply0  34518  signstres  34542  actfunsnf1o  34571  actfunsnrndisj  34572  reprsuc  34582  reprinfz1  34589  breprexplema  34597  breprexplemc  34599  breprexp  34600  breprexpnat  34601  circlemeth  34607  hgt750lemb  34623  tgoldbachgtd  34629  erdszelem8  35170  pconnconn  35203  cvmlift2lem12  35286  cvmlift3lem5  35295  cvmlift3lem7  35297  cvmlift3lem8  35298  fmla1  35359  mrsubrn  35485  msrval  35510  msubff1  35528  btwnconn1lem13  36072  elicc3  36290  neibastop2lem  36333  weiunfr  36440  unbdqndv2  36484  irrdifflemf  37298  ltflcei  37587  lindsenlbs  37594  matunitlindflem1  37595  matunitlindflem2  37596  poimirlem4  37603  poimirlem13  37612  poimirlem14  37613  poimirlem22  37621  poimirlem26  37625  poimirlem27  37626  heicant  37634  mblfinlem2  37637  mblfinlem3  37638  mblfinlem4  37639  cnambfre  37647  itg2addnclem  37650  itg2addnclem2  37651  itg2gt0cn  37654  ftc1cnnc  37671  ftc1anclem5  37676  ftc1anclem7  37678  ftc1anc  37680  equivtotbnd  37757  isbndx  37761  ssbnd  37767  heibor1lem  37788  rrncmslem  37811  islshpat  38995  lfl1dim  39099  lfl1dim2N  39100  lkrpssN  39141  glbconN  39355  glbconNOLD  39356  hlhgt2  39368  3dim2  39447  3dim3  39448  islln3  39489  islvol5  39558  2lplnja  39598  dalem19  39661  isline4N  39756  2polssN  39894  lhpmatb  40010  4atex  40055  trlatn0  40151  cdlemf2  40541  dialss  41025  diaglbN  41034  diaintclN  41037  dibglbN  41145  dibintclN  41146  dihlsscpre  41213  dihglblem5aN  41271  dihglblem2aN  41272  dihglblem4  41276  dihatexv  41317  dihjat1lem  41407  lcfl6  41479  mapdval2N  41609  aks4d1p8  42060  fldhmf1  42063  primrootscoprmpow  42072  primrootscoprbij2  42076  primrootspoweq0  42079  evl1gprodd  42090  hashscontpow  42095  aks6d1c2lem4  42100  idomnnzgmulnz  42106  deg1gprod  42113  sticksstones8  42126  sticksstones12a  42130  aks6d1c6lem3  42145  aks6d1c6lem5  42150  aks6d1c7  42157  aks5lem5a  42164  unitscyglem2  42169  sn-0tie0  42424  imacrhmcl  42487  fiabv  42509  evlsvvval  42536  evlselv  42560  fsuppind  42563  prjspertr  42578  prjspreln0  42582  prjspner1  42599  elrfi  42667  eldioph2  42735  diophin  42745  irrapxlem2  42796  irrapxlem3  42797  irrapxlem4  42798  irrapxlem5  42799  pell1234qrne0  42826  pell1234qrreccl  42827  pell1234qrmulcl  42828  pell14qrgt0  42832  pell14qrdich  42842  pell1qrge1  42843  pellfundex  42859  congabseq  42947  jm2.27b  42979  jm2.27  42981  fnwe2lem2  43024  kelac1  43036  lnrfg  43092  hbt  43103  omabs2  43305  nadd1suc  43365  rfovcnvf1od  43977  ntrneiiso  44064  ntrneikb  44067  ntrneixb  44068  ntrneik3  44069  ntrneix3  44070  ntrneik13  44071  ntrneix13  44072  cvgdvgrat  44286  binomcxplemnotnn0  44329  sineq0ALT  44910  fnchoice  45007  disjf1  45161  supxrgere  45313  supxrgelem  45317  supxrge  45318  suplesup  45319  xralrple2  45334  infxr  45347  infleinflem2  45351  infleinf  45352  uzub  45411  mccl  45580  limcrecl  45611  lptioo2  45613  lptioo1  45614  lptre2pt  45622  addlimc  45630  limsupmnflem  45702  climxrre  45732  liminflimsupclim  45789  climxlim2lem  45827  xlimliminflimsup  45844  icccncfext  45869  cncfiooicclem1  45875  cncfiooiccre  45877  dvbdfbdioolem2  45911  ioodvbdlimc1lem1  45913  dvnxpaek  45924  dvmptfprodlem  45926  dvmptfprod  45927  dvnprodlem3  45930  itgioocnicc  45959  itgspltprt  45961  stoweidlem31  46013  fourierdlem39  46128  fourierdlem42  46131  fourierdlem48  46136  fourierdlem49  46137  fourierdlem50  46138  fourierdlem51  46139  fourierdlem64  46152  fourierdlem65  46153  fourierdlem74  46162  fourierdlem75  46163  fourierdlem81  46169  fourierdlem82  46170  fourierdlem101  46189  etransclem23  46239  etransclem27  46243  etransclem32  46248  etransclem33  46249  etransclem35  46251  etransclem38  46254  sge0tsms  46362  sge0cl  46363  sge0f1o  46364  sge0split  46391  sge0rpcpnf  46403  sge0seq  46428  nnfoctbdjlem  46437  iundjiun  46442  meaiuninc3v  46466  meaiininclem  46468  omeiunltfirp  46501  carageniuncllem2  46504  carageniuncl  46505  hoidmv1lelem1  46573  hoidmvlelem3  46579  hoidmvlelem5  46581  hoidmvle  46582  hoiqssbllem3  46606  iunhoiioolem  46657  pimdecfgtioo  46699  pimincfltioo  46700  preimageiingt  46702  preimaleiinlt  46703  smflimlem4  46756  iccpartigtl  47408  iccpartgt  47412  sprsymrelf1lem  47476  paireqne  47496  proththd  47599  requad2  47608  sbgoldbst  47763  bgoldbtbndlem4  47793  isuspgrim0lem  47878  isuspgrim0  47879  isuspgrimlem  47880  gricushgr  47902  grimedg  47920  grimgrtri  47934  isubgr3stgrlem7  47957  gpgusgralem  48041  pgn4cyclex  48111  2zrngmmgm  48237  cznrng  48246  rhmsubcALTVlem4  48269  srhmsubcALTV  48310  lincsum  48415  lcoss  48422  snlindsntor  48457  islindeps2  48469  line2x  48740  line2y  48741  itscnhlinecirc02p  48771  discsubc  49050  imasubc3  49142  uppropd  49167  swapfval  49248  fucofvalg  49304  fuco21  49322  precofvalALT  49354  2arwcat  49586  lanup  49627  ranup  49628