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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  ad4antr  731  ad4antlr  732  ad5ant12  755  simplll  774  fsnex  7017  fimaproj  7812  oaabs  8254  oaabs2  8255  omabs  8257  undom  8588  sbthlem8  8618  findcard3  8745  cantnfle  9118  cantnfp1  9128  cantnflem1c  9134  sornom  9688  enfin2i  9732  ttukeylem6  9925  fpwwe2lem13  10053  winalim2  10107  wuncval2  10158  negf1o  11059  xlemul1a  12669  difreicc  12862  flflp1  13172  faclbnd  13646  swrdswrd  14058  pfxccatin12lem3  14085  swrdccat3blem  14092  ello12  14865  elo12  14876  rlimclim1  14894  rlimcld2  14927  o1co  14935  o1of2  14961  o1rlimmul  14967  rlimsqzlem  14997  isercoll  15016  o1fsum  15160  supcvg  15203  dvds2ln  15634  lcmgcdlem  15940  cncongr2  16002  isprm5  16041  pcadd  16215  vdwlem2  16308  vdwlem11  16317  sbcie3s  16533  prdsval  16720  mreexexlem4d  16910  isacs2  16916  catcocl  16948  catass  16949  subccocl  17107  fullsubc  17112  funcco  17133  fullpropd  17182  ffthiso  17191  isnat  17209  natpropd  17238  fucpropd  17239  xpcval  17419  evlf2  17460  curfpropd  17475  curfuncf  17480  uncfcurf  17481  hofcl  17501  hofpropd  17509  yonffthlem  17524  isacs3lem  17768  acsfiindd  17779  gsumpropd2lem  17881  resmhm2b  17979  mhmid  18212  mhmmnd  18213  ghmgrp  18215  conjnmzb  18385  pgpfi  18722  sylow3lem2  18745  efgredlem  18865  frgpnabllem1  18986  dprdfcntz  19130  ablfac1b  19185  pgpfac1lem3  19192  pgpfac1lem5  19194  pgpfaclem3  19198  ringinvnzdiv  19339  cntzsdrg  19574  islmhm2  19803  lspsneleq  19880  znunit  20255  psgndiflemB  20289  uvcff  20480  uvcf1  20481  lindfmm  20516  psrval  20600  psrass1  20643  resspsrmul  20655  mplbas2  20710  coe1tmmul  20906  gsummoncoe1  20933  dmatsubcl  21103  scmatscm  21118  smatvscl  21129  marrepval  21167  mdetdiaglem  21203  mdetunilem8  21224  mdetunilem9  21225  pmatcoe1fsupp  21306  decpmatmulsumfsupp  21378  pmatcollpw2lem  21382  mp2pm2mplem4  21414  pm2mpmhmlem1  21423  pm2mpmhmlem2  21424  pm2mp  21430  fvmptnn04if  21454  cpmadugsumfi  21482  cpmidg2sum  21485  cpmadumatpoly  21488  cayhamlem4  21493  neiptoptop  21736  neitr  21785  ordtrest2lem  21808  cnpnei  21869  iscncl  21874  cncls  21879  cnntr  21880  cncnp  21885  lmcnp  21909  isreg2  21982  hauscmplem  22011  cmpfi  22013  1stcfb  22050  1stcrest  22058  2ndcctbss  22060  2ndcomap  22063  islly2  22089  cldllycmp  22100  lly1stc  22101  locfincmp  22131  llycmpkgen2  22155  1stckgenlem  22158  kgencn2  22162  kgencn3  22163  ptbasfi  22186  ptpjopn  22217  txdis1cn  22240  txlly  22241  txnlly  22242  txtube  22245  txcmplem2  22247  tx1stc  22255  txkgen  22257  xkopt  22260  xkoco2cn  22263  xkococnlem  22264  xkococn  22265  xkoinjcn  22292  tgqtop  22317  regr1lem  22344  kqreglem1  22346  nrmhmph  22399  rnelfmlem  22557  rnelfm  22558  fmfnfmlem4  22562  fmfnfm  22563  ufldom  22567  flimopn  22580  hauspwpwf1  22592  fclsopn  22619  fclsnei  22624  fclsrest  22629  alexsublem  22649  alexsubALTlem3  22654  ptcmplem2  22658  ptcmplem3  22659  cnextfun  22669  cnextcn  22672  symgtgp  22711  tgpt0  22724  qustgpopn  22725  tsmsxplem1  22758  trust  22835  utopsnneiplem  22853  utop3cls  22857  utopreg  22858  isucn2  22885  cstucnd  22890  ucncn  22891  fmucnd  22898  cfilufg  22899  neipcfilu  22902  met2ndci  23129  prdsxmslem2  23136  metustid  23161  metustexhalf  23163  metust  23165  psmetutop  23174  nmoleub  23337  reconnlem2  23432  xrge0tsms  23439  cncfco  23512  lebnumlem3  23568  lebnum  23569  nmoleub2lem2  23721  nmoleub3  23724  iscfil2  23870  iscau4  23883  iscmet3lem2  23896  equivcfil  23903  equivcau  23904  caubl  23912  rrxdstprj1  24013  ovolshftlem2  24114  ovolicc2lem4  24124  uniioombl  24193  i1fmulclem  24306  mbfi1fseqlem6  24324  itg2const2  24345  itg2split  24353  bddiblnc  24445  ellimc2  24480  ellimc3  24482  limcflf  24484  dvmptfsum  24578  dvferm1  24588  dvferm2  24590  dvlip2  24598  c1lip1  24600  lhop1  24617  ftc1a  24640  ply1divex  24737  plyeq0lem  24807  plymullem1  24811  coemullem  24847  coemulc  24852  ulmshftlem  24984  ulmcaulem  24989  ulmbdd  24993  ulmcn  24994  ulmdvlem3  24997  mtestbdd  25000  pserulm  25017  pserdvlem2  25023  abelthlem8  25034  xrlimcnp  25554  jensen  25574  lgamucov  25623  logfac2  25801  dchrelbas3  25822  dchrpt  25851  gausslemma2dlem1a  25949  lgsquad3  25971  2sqb  26016  rpvmasumlem  26071  dchrisumlem1  26073  dchrisumlem3  26075  dchrmusum2  26078  dchrvmasumlem2  26082  dchrisum0flblem1  26092  dchrisum0lem1b  26099  dchrisum0lem1  26100  dchrisum0  26104  mulog2sumlem2  26119  pntlem3  26193  ostth3  26222  istrkgcb  26250  tgbtwndiff  26300  iscgrglt  26308  tgcgrxfr  26312  motcgrg  26338  lnext  26361  tgbtwnconn1  26369  tgbtwnconn3  26371  legval  26378  legtrid  26385  legso  26393  hlcgreu  26412  tglnne  26422  tglineeltr  26425  tglnne0  26434  colline  26443  tglowdim2l  26444  tglowdim2ln  26445  mirreu3  26448  mirbtwnhl  26474  krippenlem  26484  midexlem  26486  perpcom  26507  footexALT  26512  footex  26515  colperpexlem3  26526  colperpex  26527  opphllem  26529  midex  26531  oppne3  26537  opptgdim2  26539  oppnid  26540  opphllem2  26542  opphllem5  26545  opphllem6  26546  oppperpex  26547  outpasch  26549  hlpasch  26550  lnopp2hpgb  26557  hpgerlem  26559  colopp  26563  colhp  26564  lmieu  26578  lnperpex  26597  trgcopy  26598  trgcopyeulem  26599  iscgra1  26604  cgrane1  26606  cgrane2  26607  cgrane3  26608  cgrane4  26609  cgrahl1  26610  cgrahl2  26611  cgracgr  26612  cgraswap  26614  cgracom  26616  cgratr  26617  flatcgra  26618  cgrabtwn  26620  cgrahl  26621  sacgr  26625  acopyeu  26628  cgrg3col4  26647  tgasa1  26652  f1otrg  26665  f1otrge  26666  axeuclidlem  26756  axcontlem2  26759  umgrvad2edg  27003  usgredg2vlem2  27016  pthdepisspth  27524  clwwlkccatlem  27774  clwlkclwwlklem2  27785  3cycld  27963  eupth2lems  28023  eucrctshift  28028  frgr3vlem2  28059  n4cyclfrgr  28076  numclwwlk1lem2f1  28142  numclwwlk2lem1  28161  ubthlem3  28655  chirredlem1  30173  chirredlem3  30175  cdj1i  30216  fnpreimac  30434  xrge0infss  30510  nn0xmulclb  30522  hashxpe  30555  ccatf1  30651  swrdf1  30656  dfmgc2lem  30703  gsumhashmul  30741  xrge0tsmsd  30742  omndmul2  30763  gsumle  30775  psgnfzto1stlem  30792  cycpmco2  30825  cycpmrn  30835  tocyccntz  30836  cycpmconjslem2  30847  cyc3conja  30849  submarchi  30865  suborng  30939  isarchiofld  30941  imaslmod  30973  lindfpropd  30996  rhmpreimaidl  31011  elrspunidl  31014  rhmimaidl  31017  qsidomlem1  31036  mxidlprm  31048  lindsunlem  31108  lindsun  31109  lbsdiflsp0  31110  dimkerim  31111  fedgmul  31115  extdg1id  31141  smatrcl  31149  1smat1  31157  submateq  31162  mdetpmtr1  31176  madjusmdetlem2  31181  locfinreflem  31193  cmppcmp  31211  rhmpreimacn  31238  ordtrest2NEWlem  31275  ordtconnlem1  31277  lmdvg  31306  esumpcvgval  31447  esum2d  31462  sigapildsys  31531  ldgenpisyslem1  31532  fiunelros  31543  volmeas  31600  imambfm  31630  omssubadd  31668  carsggect  31686  carsgclctunlem3  31688  sgnmul  31910  signsply0  31931  signstres  31955  actfunsnf1o  31985  actfunsnrndisj  31986  reprsuc  31996  reprinfz1  32003  breprexplema  32011  breprexplemc  32013  breprexp  32014  breprexpnat  32015  circlemeth  32021  hgt750lemb  32037  tgoldbachgtd  32043  erdszelem8  32558  pconnconn  32591  cvmlift2lem12  32674  cvmlift3lem5  32683  cvmlift3lem7  32685  cvmlift3lem8  32686  mrsubrn  32873  msrval  32898  msubff1  32916  slerec  33390  btwnconn1lem13  33673  elicc3  33778  neibastop2lem  33821  unbdqndv2  33963  irrdifflemf  34739  ltflcei  35045  lindsenlbs  35052  matunitlindflem1  35053  matunitlindflem2  35054  poimirlem4  35061  poimirlem13  35070  poimirlem14  35071  poimirlem22  35079  poimirlem26  35083  poimirlem27  35084  heicant  35092  mblfinlem2  35095  mblfinlem3  35096  mblfinlem4  35097  cnambfre  35105  itg2addnclem  35108  itg2addnclem2  35109  itg2gt0cn  35112  ftc1cnnc  35129  ftc1anclem5  35134  ftc1anclem7  35136  ftc1anc  35138  equivtotbnd  35216  isbndx  35220  ssbnd  35226  heibor1lem  35247  rrncmslem  35270  islshpat  36313  lfl1dim  36417  lfl1dim2N  36418  lkrpssN  36459  glbconN  36673  hlhgt2  36685  3dim2  36764  3dim3  36765  islln3  36806  islvol5  36875  2lplnja  36915  dalem19  36978  isline4N  37073  2polssN  37211  lhpmatb  37327  4atex  37372  trlatn0  37468  cdlemf2  37858  dialss  38342  diaglbN  38351  diaintclN  38354  dibglbN  38462  dibintclN  38463  dihlsscpre  38530  dihglblem5aN  38588  dihglblem2aN  38589  dihglblem4  38593  dihatexv  38634  dihjat1lem  38724  lcfl6  38796  mapdval2N  38926  fsuppind  39456  sn-0tie0  39576  prjspertr  39599  prjspreln0  39603  elrfi  39635  eldioph2  39703  diophin  39713  irrapxlem2  39764  irrapxlem3  39765  irrapxlem4  39766  irrapxlem5  39767  pell1234qrne0  39794  pell1234qrreccl  39795  pell1234qrmulcl  39796  pell14qrgt0  39800  pell14qrdich  39810  pell1qrge1  39811  pellfundex  39827  congabseq  39915  jm2.27b  39947  jm2.27  39949  fnwe2lem2  39995  kelac1  40007  lnrfg  40063  hbt  40074  rfovcnvf1od  40705  ntrneiiso  40794  ntrneikb  40797  ntrneixb  40798  ntrneik3  40799  ntrneix3  40800  ntrneik13  40801  ntrneix13  40802  cvgdvgrat  41017  binomcxplemnotnn0  41060  sineq0ALT  41643  disjf1  41809  supxrgere  41965  supxrgelem  41969  supxrge  41970  suplesup  41971  xralrple2  41986  infxr  41999  infleinflem2  42003  infleinf  42004  uzub  42068  mccl  42240  limcrecl  42271  lptioo2  42273  lptioo1  42274  lptre2pt  42282  addlimc  42290  limsupmnflem  42362  climxrre  42392  liminflimsupclim  42449  climxlim2lem  42487  xlimliminflimsup  42504  icccncfext  42529  cncfiooicclem1  42535  cncfiooiccre  42537  dvbdfbdioolem2  42571  ioodvbdlimc1lem1  42573  dvnxpaek  42584  dvmptfprodlem  42586  dvmptfprod  42587  dvnprodlem3  42590  itgioocnicc  42619  itgspltprt  42621  stoweidlem31  42673  fourierdlem39  42788  fourierdlem42  42791  fourierdlem48  42796  fourierdlem49  42797  fourierdlem50  42798  fourierdlem51  42799  fourierdlem64  42812  fourierdlem65  42813  fourierdlem74  42822  fourierdlem75  42823  fourierdlem81  42829  fourierdlem82  42830  fourierdlem101  42849  etransclem23  42899  etransclem27  42903  etransclem32  42908  etransclem33  42909  etransclem35  42911  etransclem38  42914  sge0tsms  43019  sge0cl  43020  sge0f1o  43021  sge0split  43048  sge0rpcpnf  43060  sge0seq  43085  nnfoctbdjlem  43094  iundjiun  43099  meaiuninc3v  43123  meaiininclem  43125  omeiunltfirp  43158  carageniuncllem2  43161  carageniuncl  43162  hoidmv1lelem1  43230  hoidmvlelem3  43236  hoidmvlelem5  43238  hoidmvle  43239  hoiqssbllem3  43263  iunhoiioolem  43314  pimdecfgtioo  43352  pimincfltioo  43353  preimageiingt  43355  preimaleiinlt  43356  smflimlem4  43407  iccpartigtl  43940  iccpartgt  43944  sprsymrelf1lem  44008  paireqne  44028  proththd  44132  requad2  44141  sbgoldbst  44296  bgoldbtbndlem4  44326  isomushgr  44344  isomuspgrlem2d  44349  resmgmhm2b  44420  2zrngmmgm  44570  cznrng  44579  rnghmsubcsetclem2  44600  rhmsubcsetclem2  44646  srhmsubc  44700  rhmsubclem4  44713  srhmsubcALTV  44718  rhmsubcALTVlem4  44731  lincsum  44838  lcoss  44845  snlindsntor  44880  islindeps2  44892  line2x  45168  line2y  45169  itscnhlinecirc02p  45199