Theorem ad3antrrr 729

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  ad4antr  731  ad4antlr  732  ad5ant12  755  simplll  774  fsnex  7281  fimaproj  8121  frxp3  8137  oaabs  8647  oaabs2  8648  omabs  8650  cofon1  8671  undomOLD  9060  sbthlem8  9090  findcard3OLD  9286  cantnfle  9666  cantnfp1  9676  cantnflem1c  9682  sornom  10272  enfin2i  10316  ttukeylem6  10509  fpwwe2lem12  10637  winalim2  10691  wuncval2  10742  negf1o  11644  xlemul1a  13267  difreicc  13461  flflp1  13772  faclbnd  14250  swrdswrd  14655  pfxccatin12lem3  14682  swrdccat3blem  14689  ello12  15460  elo12  15471  rlimclim1  15489  rlimcld2  15522  o1co  15530  o1of2  15557  o1rlimmul  15563  rlimsqzlem  15595  isercoll  15614  o1fsum  15759  supcvg  15802  dvds2ln  16232  lcmgcdlem  16543  cncongr2  16605  isprm5  16644  prmdvdsncoprmbd  16663  pcadd  16822  vdwlem2  16915  vdwlem11  16924  sbcie3s  17095  prdsval  17401  mreexexlem4d  17591  isacs2  17597  catcocl  17629  catass  17630  subccocl  17795  fullsubc  17800  funcco  17821  fullpropd  17871  ffthiso  17880  isnat  17898  natpropd  17929  fucpropd  17930  xpcval  18129  evlf2  18171  curfpropd  18186  curfuncf  18191  uncfcurf  18192  hofcl  18212  hofpropd  18220  yonffthlem  18235  isacs3lem  18495  acsfiindd  18506  gsumpropd2lem  18598  resmhm2b  18703  mhmid  18946  mhmmnd  18947  ghmgrp  18949  conjnmzb  19127  pgpfi  19473  sylow3lem2  19496  efgredlem  19615  frgpnabllem1  19741  imasabl  19744  dprdfcntz  19885  ablfac1b  19940  pgpfac1lem3  19947  pgpfac1lem5  19949  pgpfaclem3  19953  ringinvnzdiv  20113  imadrhmcl  20413  cntzsdrg  20418  islmhm2  20649  lspsneleq  20728  znunit  21119  psgndiflemB  21153  uvcff  21346  uvcf1  21347  lindfmm  21382  sraassab  21422  psrval  21468  psrass1  21525  resspsrmul  21537  mplbas2  21597  mhpmulcl  21692  coe1tmmul  21799  gsummoncoe1  21828  dmatsubcl  22000  scmatscm  22015  smatvscl  22026  marrepval  22064  mdetdiaglem  22100  mdetunilem8  22121  mdetunilem9  22122  pmatcoe1fsupp  22203  decpmatmulsumfsupp  22275  pmatcollpw2lem  22279  mp2pm2mplem4  22311  pm2mpmhmlem1  22320  pm2mpmhmlem2  22321  pm2mp  22327  fvmptnn04if  22351  cpmadugsumfi  22379  cpmidg2sum  22382  cpmadumatpoly  22385  cayhamlem4  22390  neiptoptop  22635  neitr  22684  ordtrest2lem  22707  cnpnei  22768  iscncl  22773  cncls  22778  cnntr  22779  cncnp  22784  lmcnp  22808  isreg2  22881  hauscmplem  22910  cmpfi  22912  1stcfb  22949  1stcrest  22957  2ndcctbss  22959  2ndcomap  22962  islly2  22988  cldllycmp  22999  lly1stc  23000  locfincmp  23030  llycmpkgen2  23054  1stckgenlem  23057  kgencn2  23061  kgencn3  23062  ptbasfi  23085  ptpjopn  23116  txdis1cn  23139  txlly  23140  txnlly  23141  txtube  23144  txcmplem2  23146  tx1stc  23154  txkgen  23156  xkopt  23159  xkoco2cn  23162  xkococnlem  23163  xkococn  23164  xkoinjcn  23191  tgqtop  23216  regr1lem  23243  kqreglem1  23245  nrmhmph  23298  rnelfmlem  23456  rnelfm  23457  fmfnfmlem4  23461  fmfnfm  23462  ufldom  23466  flimopn  23479  hauspwpwf1  23491  fclsopn  23518  fclsnei  23523  fclsrest  23528  alexsublem  23548  alexsubALTlem3  23553  ptcmplem2  23557  ptcmplem3  23558  cnextfun  23568  cnextcn  23571  symgtgp  23610  tgpt0  23623  qustgpopn  23624  tsmsxplem1  23657  trust  23734  utopsnneiplem  23752  utop3cls  23756  utopreg  23757  isucn2  23784  cstucnd  23789  ucncn  23790  fmucnd  23797  cfilufg  23798  neipcfilu  23801  met2ndci  24031  prdsxmslem2  24038  metustid  24063  metustexhalf  24065  metust  24067  psmetutop  24076  nmoleub  24248  reconnlem2  24343  xrge0tsms  24350  cncfco  24423  lebnumlem3  24479  lebnum  24480  nmoleub2lem2  24632  nmoleub3  24635  iscfil2  24783  iscau4  24796  iscmet3lem2  24809  equivcfil  24816  equivcau  24817  caubl  24825  rrxdstprj1  24926  ovolshftlem2  25027  ovolicc2lem4  25037  uniioombl  25106  i1fmulclem  25220  mbfi1fseqlem6  25238  itg2const2  25259  itg2split  25267  bddiblnc  25359  ellimc2  25394  ellimc3  25396  limcflf  25398  dvmptfsum  25492  dvferm1  25502  dvferm2  25504  dvlip2  25512  c1lip1  25514  lhop1  25531  ftc1a  25554  ply1divex  25654  plyeq0lem  25724  plymullem1  25728  coemullem  25764  coemulc  25769  ulmshftlem  25901  ulmcaulem  25906  ulmbdd  25910  ulmcn  25911  ulmdvlem3  25914  mtestbdd  25917  pserulm  25934  pserdvlem2  25940  abelthlem8  25951  xrlimcnp  26473  jensen  26493  lgamucov  26542  logfac2  26720  dchrelbas3  26741  dchrpt  26770  gausslemma2dlem1a  26868  lgsquad3  26890  2sqb  26935  rpvmasumlem  26990  dchrisumlem1  26992  dchrisumlem3  26994  dchrmusum2  26997  dchrvmasumlem2  27001  dchrisum0flblem1  27011  dchrisum0lem1b  27018  dchrisum0lem1  27019  dchrisum0  27023  mulog2sumlem2  27038  pntlem3  27112  ostth3  27141  slerec  27320  cofcutr  27411  istrkgcb  27707  tgbtwndiff  27757  iscgrglt  27765  tgcgrxfr  27769  motcgrg  27795  lnext  27818  tgbtwnconn1  27826  tgbtwnconn3  27828  legval  27835  legtrid  27842  legso  27850  hlcgreu  27869  tglnne  27879  tglineeltr  27882  tglnne0  27891  colline  27900  tglowdim2l  27901  tglowdim2ln  27902  mirreu3  27905  mirbtwnhl  27931  krippenlem  27941  midexlem  27943  perpcom  27964  footexALT  27969  footex  27972  colperpexlem3  27983  colperpex  27984  opphllem  27986  midex  27988  oppne3  27994  opptgdim2  27996  oppnid  27997  opphllem2  27999  opphllem5  28002  opphllem6  28003  oppperpex  28004  outpasch  28006  hlpasch  28007  lnopp2hpgb  28014  hpgerlem  28016  colopp  28020  colhp  28021  lmieu  28035  lnperpex  28054  trgcopy  28055  trgcopyeulem  28056  iscgra1  28061  cgrane1  28063  cgrane2  28064  cgrane3  28065  cgrane4  28066  cgrahl1  28067  cgrahl2  28068  cgracgr  28069  cgraswap  28071  cgracom  28073  cgratr  28074  flatcgra  28075  cgrabtwn  28077  cgrahl  28078  sacgr  28082  acopyeu  28085  cgrg3col4  28104  tgasa1  28109  f1otrg  28122  f1otrge  28123  axeuclidlem  28220  axcontlem2  28223  umgrvad2edg  28470  usgredg2vlem2  28483  pthdepisspth  28992  clwwlkccatlem  29242  clwlkclwwlklem2  29253  3cycld  29431  eupth2lems  29491  eucrctshift  29496  frgr3vlem2  29527  n4cyclfrgr  29544  numclwwlk1lem2f1  29610  numclwwlk2lem1  29629  ubthlem3  30125  chirredlem1  31643  chirredlem3  31645  cdj1i  31686  fnpreimac  31896  xrge0infss  31973  nn0xmulclb  31984  hashxpe  32019  ccatf1  32115  swrdf1  32120  dfmgc2lem  32165  mgcf1o  32173  gsumhashmul  32208  xrge0tsmsd  32209  omndmul2  32230  gsumle  32242  psgnfzto1stlem  32259  cycpmco2  32292  cycpmrn  32302  tocyccntz  32303  cycpmconjslem2  32314  cyc3conja  32316  submarchi  32332  suborng  32433  isarchiofld  32435  imaslmod  32468  znfermltl  32479  lindfpropd  32498  nsgqusf1olem1  32524  ghmquskerlem3  32531  ghmqusker  32532  rhmpreimaidl  32537  unitpidl1  32542  elrspunidl  32546  elrspunsn  32547  rhmimaidl  32550  drngidl  32551  qsidomlem1  32571  mxidlprm  32586  mxidlirredi  32587  qsdrngilem  32608  qsdrngi  32609  evls1fpws  32646  ply1degltdimlem  32707  lindsunlem  32709  lindsun  32710  lbsdiflsp0  32711  dimkerim  32712  fedgmul  32716  extdg1id  32742  minplyirred  32770  smatrcl  32776  1smat1  32784  submateq  32789  mdetpmtr1  32803  madjusmdetlem2  32808  locfinreflem  32820  cmppcmp  32838  rhmpreimacn  32865  ordtrest2NEWlem  32902  ordtconnlem1  32904  lmdvg  32933  esumpcvgval  33076  esum2d  33091  sigapildsys  33160  ldgenpisyslem1  33161  fiunelros  33172  volmeas  33229  imambfm  33261  omssubadd  33299  carsggect  33317  carsgclctunlem3  33319  sgnmul  33541  signsply0  33562  signstres  33586  actfunsnf1o  33616  actfunsnrndisj  33617  reprsuc  33627  reprinfz1  33634  breprexplema  33642  breprexplemc  33644  breprexp  33645  breprexpnat  33646  circlemeth  33652  hgt750lemb  33668  tgoldbachgtd  33674  erdszelem8  34189  pconnconn  34222  cvmlift2lem12  34305  cvmlift3lem5  34314  cvmlift3lem7  34316  cvmlift3lem8  34317  mrsubrn  34504  msrval  34529  msubff1  34547  btwnconn1lem13  35071  elicc3  35202  neibastop2lem  35245  unbdqndv2  35387  irrdifflemf  36206  ltflcei  36476  lindsenlbs  36483  matunitlindflem1  36484  matunitlindflem2  36485  poimirlem4  36492  poimirlem13  36501  poimirlem14  36502  poimirlem22  36510  poimirlem26  36514  poimirlem27  36515  heicant  36523  mblfinlem2  36526  mblfinlem3  36527  mblfinlem4  36528  cnambfre  36536  itg2addnclem  36539  itg2addnclem2  36540  itg2gt0cn  36543  ftc1cnnc  36560  ftc1anclem5  36565  ftc1anclem7  36567  ftc1anc  36569  equivtotbnd  36646  isbndx  36650  ssbnd  36656  heibor1lem  36677  rrncmslem  36700  islshpat  37887  lfl1dim  37991  lfl1dim2N  37992  lkrpssN  38033  glbconN  38247  glbconNOLD  38248  hlhgt2  38260  3dim2  38339  3dim3  38340  islln3  38381  islvol5  38450  2lplnja  38490  dalem19  38553  isline4N  38648  2polssN  38786  lhpmatb  38902  4atex  38947  trlatn0  39043  cdlemf2  39433  dialss  39917  diaglbN  39926  diaintclN  39929  dibglbN  40037  dibintclN  40038  dihlsscpre  40105  dihglblem5aN  40163  dihglblem2aN  40164  dihglblem4  40168  dihatexv  40209  dihjat1lem  40299  lcfl6  40371  mapdval2N  40501  aks4d1p8  40952  fldhmf1  40955  sticksstones8  40969  sticksstones12a  40973  imacrhmcl  41089  evlsvvval  41135  evlselv  41159  fsuppind  41162  sn-0tie0  41312  prjspertr  41347  prjspreln0  41351  prjspner1  41368  elrfi  41432  eldioph2  41500  diophin  41510  irrapxlem2  41561  irrapxlem3  41562  irrapxlem4  41563  irrapxlem5  41564  pell1234qrne0  41591  pell1234qrreccl  41592  pell1234qrmulcl  41593  pell14qrgt0  41597  pell14qrdich  41607  pell1qrge1  41608  pellfundex  41624  congabseq  41713  jm2.27b  41745  jm2.27  41747  fnwe2lem2  41793  kelac1  41805  lnrfg  41861  hbt  41872  nadd1suc  42142  rfovcnvf1od  42755  ntrneiiso  42842  ntrneikb  42845  ntrneixb  42846  ntrneik3  42847  ntrneix3  42848  ntrneik13  42849  ntrneix13  42850  cvgdvgrat  43072  binomcxplemnotnn0  43115  sineq0ALT  43698  disjf1  43880  supxrgere  44043  supxrgelem  44047  supxrge  44048  suplesup  44049  xralrple2  44064  infxr  44077  infleinflem2  44081  infleinf  44082  uzub  44141  mccl  44314  limcrecl  44345  lptioo2  44347  lptioo1  44348  lptre2pt  44356  addlimc  44364  limsupmnflem  44436  climxrre  44466  liminflimsupclim  44523  climxlim2lem  44561  xlimliminflimsup  44578  icccncfext  44603  cncfiooicclem1  44609  cncfiooiccre  44611  dvbdfbdioolem2  44645  ioodvbdlimc1lem1  44647  dvnxpaek  44658  dvmptfprodlem  44660  dvmptfprod  44661  dvnprodlem3  44664  itgioocnicc  44693  itgspltprt  44695  stoweidlem31  44747  fourierdlem39  44862  fourierdlem42  44865  fourierdlem48  44870  fourierdlem49  44871  fourierdlem50  44872  fourierdlem51  44873  fourierdlem64  44886  fourierdlem65  44887  fourierdlem74  44896  fourierdlem75  44897  fourierdlem81  44903  fourierdlem82  44904  fourierdlem101  44923  etransclem23  44973  etransclem27  44977  etransclem32  44982  etransclem33  44983  etransclem35  44985  etransclem38  44988  sge0tsms  45096  sge0cl  45097  sge0f1o  45098  sge0split  45125  sge0rpcpnf  45137  sge0seq  45162  nnfoctbdjlem  45171  iundjiun  45176  meaiuninc3v  45200  meaiininclem  45202  omeiunltfirp  45235  carageniuncllem2  45238  carageniuncl  45239  hoidmv1lelem1  45307  hoidmvlelem3  45313  hoidmvlelem5  45315  hoidmvle  45316  hoiqssbllem3  45340  iunhoiioolem  45391  pimdecfgtioo  45433  pimincfltioo  45434  preimageiingt  45436  preimaleiinlt  45437  smflimlem4  45490  iccpartigtl  46091  iccpartgt  46095  sprsymrelf1lem  46159  paireqne  46179  proththd  46282  requad2  46291  sbgoldbst  46446  bgoldbtbndlem4  46476  isomushgr  46494  isomuspgrlem2d  46499  resmgmhm2b  46570  2zrngmmgm  46844  cznrng  46853  rnghmsubcsetclem2  46874  rhmsubcsetclem2  46920  srhmsubc  46974  rhmsubclem4  46987  srhmsubcALTV  46992  rhmsubcALTVlem4  47005  lincsum  47110  lcoss  47117  snlindsntor  47152  islindeps2  47164  line2x  47440  line2y  47441  itscnhlinecirc02p  47471