Theorem ad3antrrr 728

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

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  ad4antr  730  ad4antlr  731  ad5ant12  754  simplll  773  fsnex  7297  fimaproj  8149  frxp3  8165  oaabs  8678  oaabs2  8679  omabs  8681  cofon1  8702  undomOLD  9098  sbthlem8  9128  findcard3OLD  9320  cantnfle  9714  cantnfp1  9724  cantnflem1c  9730  sornom  10320  enfin2i  10364  ttukeylem6  10557  fpwwe2lem12  10685  winalim2  10739  wuncval2  10790  negf1o  11694  xlemul1a  13321  difreicc  13515  flflp1  13827  faclbnd  14307  swrdswrd  14713  pfxccatin12lem3  14740  swrdccat3blem  14747  ello12  15518  elo12  15529  rlimclim1  15547  rlimcld2  15580  o1co  15588  o1of2  15615  o1rlimmul  15621  rlimsqzlem  15653  isercoll  15672  o1fsum  15817  supcvg  15860  dvds2ln  16291  lcmgcdlem  16607  cncongr2  16669  isprm5  16708  prmdvdsncoprmbd  16729  pcadd  16891  vdwlem2  16984  vdwlem11  16993  sbcie3s  17164  prdsval  17470  mreexexlem4d  17660  isacs2  17666  catcocl  17698  catass  17699  subccocl  17864  fullsubc  17869  funcco  17890  fullpropd  17942  ffthiso  17951  isnat  17970  natpropd  18001  fucpropd  18002  xpcval  18201  evlf2  18243  curfpropd  18258  curfuncf  18263  uncfcurf  18264  hofcl  18284  hofpropd  18292  yonffthlem  18307  isacs3lem  18567  acsfiindd  18578  gsumpropd2lem  18672  resmgmhm2b  18706  resmhm2b  18812  mhmid  19057  mhmmnd  19058  ghmgrp  19060  conjnmzb  19247  ghmqusnsg  19276  ghmquskerlem3  19280  ghmqusker  19281  pgpfi  19603  sylow3lem2  19626  efgredlem  19745  frgpnabllem1  19871  imasabl  19874  dprdfcntz  20015  ablfac1b  20070  pgpfac1lem3  20077  pgpfac1lem5  20079  pgpfaclem3  20083  ringinvnzdiv  20280  rnghmsubcsetclem2  20610  rhmsubcsetclem2  20639  srhmsubc  20658  rhmsubclem4  20666  imadrhmcl  20776  cntzsdrg  20781  islmhm2  21016  lspsneleq  21096  rhmpreimaidl  21266  znunit  21561  psgndiflemB  21596  uvcff  21789  uvcf1  21790  lindfmm  21825  sraassab  21865  psrval  21912  psrass1  21973  resspsrmul  21985  mplbas2  22049  mhpmulcl  22143  psdmul  22160  coe1tmmul  22268  gsummoncoe1  22299  evls1fpws  22360  dmatsubcl  22491  scmatscm  22506  smatvscl  22517  marrepval  22555  mdetdiaglem  22591  mdetunilem8  22612  mdetunilem9  22613  pmatcoe1fsupp  22694  decpmatmulsumfsupp  22766  pmatcollpw2lem  22770  mp2pm2mplem4  22802  pm2mpmhmlem1  22811  pm2mpmhmlem2  22812  pm2mp  22818  fvmptnn04if  22842  cpmadugsumfi  22870  cpmidg2sum  22873  cpmadumatpoly  22876  cayhamlem4  22881  neiptoptop  23126  neitr  23175  ordtrest2lem  23198  cnpnei  23259  iscncl  23264  cncls  23269  cnntr  23270  cncnp  23275  lmcnp  23299  isreg2  23372  hauscmplem  23401  cmpfi  23403  1stcfb  23440  1stcrest  23448  2ndcctbss  23450  2ndcomap  23453  islly2  23479  cldllycmp  23490  lly1stc  23491  locfincmp  23521  llycmpkgen2  23545  1stckgenlem  23548  kgencn2  23552  kgencn3  23553  ptbasfi  23576  ptpjopn  23607  txdis1cn  23630  txlly  23631  txnlly  23632  txtube  23635  txcmplem2  23637  tx1stc  23645  txkgen  23647  xkopt  23650  xkoco2cn  23653  xkococnlem  23654  xkococn  23655  xkoinjcn  23682  tgqtop  23707  regr1lem  23734  kqreglem1  23736  nrmhmph  23789  rnelfmlem  23947  rnelfm  23948  fmfnfmlem4  23952  fmfnfm  23953  ufldom  23957  flimopn  23970  hauspwpwf1  23982  fclsopn  24009  fclsnei  24014  fclsrest  24019  alexsublem  24039  alexsubALTlem3  24044  ptcmplem2  24048  ptcmplem3  24049  cnextfun  24059  cnextcn  24062  symgtgp  24101  tgpt0  24114  qustgpopn  24115  tsmsxplem1  24148  trust  24225  utopsnneiplem  24243  utop3cls  24247  utopreg  24248  isucn2  24275  cstucnd  24280  ucncn  24281  fmucnd  24288  cfilufg  24289  neipcfilu  24292  met2ndci  24522  prdsxmslem2  24529  metustid  24554  metustexhalf  24556  metust  24558  psmetutop  24567  nmoleub  24739  reconnlem2  24834  xrge0tsms  24841  cncfco  24918  lebnumlem3  24980  lebnum  24981  nmoleub2lem2  25134  nmoleub3  25137  iscfil2  25285  iscau4  25298  iscmet3lem2  25311  equivcfil  25318  equivcau  25319  caubl  25327  rrxdstprj1  25428  ovolshftlem2  25530  ovolicc2lem4  25540  uniioombl  25609  i1fmulclem  25723  mbfi1fseqlem6  25741  itg2const2  25762  itg2split  25770  bddiblnc  25862  ellimc2  25897  ellimc3  25899  limcflf  25901  dvmptfsum  25998  dvferm1  26008  dvferm2  26010  dvlip2  26019  c1lip1  26021  lhop1  26038  ftc1a  26063  ply1divex  26164  plyeq0lem  26237  plymullem1  26241  coemullem  26277  coemulc  26282  ulmshftlem  26418  ulmcaulem  26423  ulmbdd  26427  ulmcn  26428  ulmdvlem3  26431  mtestbdd  26434  pserulm  26451  pserdvlem2  26458  abelthlem8  26469  xrlimcnp  26996  jensen  27017  lgamucov  27066  logfac2  27246  dchrelbas3  27267  dchrpt  27296  gausslemma2dlem1a  27394  lgsquad3  27416  2sqb  27461  rpvmasumlem  27516  dchrisumlem1  27518  dchrisumlem3  27520  dchrmusum2  27523  dchrvmasumlem2  27527  dchrisum0flblem1  27537  dchrisum0lem1b  27544  dchrisum0lem1  27545  dchrisum0  27549  mulog2sumlem2  27564  pntlem3  27638  ostth3  27667  slerec  27849  cofcutr  27941  remulscllem2  28352  istrkgcb  28383  tgbtwndiff  28433  iscgrglt  28441  tgcgrxfr  28445  motcgrg  28471  lnext  28494  tgbtwnconn1  28502  tgbtwnconn3  28504  legval  28511  legtrid  28518  legso  28526  hlcgreu  28545  tglnne  28555  tglineeltr  28558  tglnne0  28567  colline  28576  tglowdim2l  28577  tglowdim2ln  28578  mirreu3  28581  mirbtwnhl  28607  krippenlem  28617  midexlem  28619  perpcom  28640  footexALT  28645  footex  28648  colperpexlem3  28659  colperpex  28660  opphllem  28662  midex  28664  oppne3  28670  opptgdim2  28672  oppnid  28673  opphllem2  28675  opphllem5  28678  opphllem6  28679  oppperpex  28680  outpasch  28682  hlpasch  28683  lnopp2hpgb  28690  hpgerlem  28692  colopp  28696  colhp  28697  lmieu  28711  lnperpex  28730  trgcopy  28731  trgcopyeulem  28732  iscgra1  28737  cgrane1  28739  cgrane2  28740  cgrane3  28741  cgrane4  28742  cgrahl1  28743  cgrahl2  28744  cgracgr  28745  cgraswap  28747  cgracom  28749  cgratr  28750  flatcgra  28751  cgrabtwn  28753  cgrahl  28754  sacgr  28758  acopyeu  28761  cgrg3col4  28780  tgasa1  28785  f1otrg  28798  f1otrge  28799  axeuclidlem  28896  axcontlem2  28899  umgrvad2edg  29149  usgredg2vlem2  29162  pthdepisspth  29672  clwwlkccatlem  29922  clwlkclwwlklem2  29933  3cycld  30111  eupth2lems  30171  eucrctshift  30176  frgr3vlem2  30207  n4cyclfrgr  30224  numclwwlk1lem2f1  30290  numclwwlk2lem1  30309  ubthlem3  30805  chirredlem1  32323  chirredlem3  32325  cdj1i  32366  fnpreimac  32588  xrge0infss  32664  nn0xmulclb  32675  hashxpe  32711  ccatf1  32812  ccatws1f1o  32815  swrdf1  32820  dfmgc2lem  32865  mgcf1o  32873  chnind  32880  gsumhashmul  32925  xrge0tsmsd  32926  omndmul2  32947  gsumle  32959  psgnfzto1stlem  32978  cycpmco2  33011  cycpmrn  33021  tocyccntz  33022  cycpmconjslem2  33033  cyc3conja  33035  submarchi  33051  erlval  33113  erler  33120  rlocf1  33128  domnprodn0  33130  subrdom  33137  suborng  33193  isarchiofld  33195  imaslmod  33228  znfermltl  33241  lindfpropd  33257  unitprodclb  33264  nsgqusf1olem1  33288  unitpidl1  33299  elrspunidl  33303  elrspunsn  33304  rhmimaidl  33307  drngidl  33308  qsidomlem1  33327  mxidlprm  33345  mxidlirredi  33346  qsdrngilem  33369  qsdrngi  33370  rsprprmprmidl  33397  rsprprmprmidlb  33398  rprmasso2  33401  rprmirred  33406  rprmirredb  33407  rprmdvdspow  33408  1arithidom  33412  pidufd  33418  1arithufdlem3  33421  dfufd2  33425  ply1dg3rt0irred  33454  ply1degltdimlem  33517  lindsunlem  33519  lindsun  33520  lbsdiflsp0  33521  dimkerim  33522  fedgmul  33526  extdg1id  33552  evls1fldgencl  33556  minplyirred  33580  fldext2chn  33606  smatrcl  33611  1smat1  33619  submateq  33624  mdetpmtr1  33638  madjusmdetlem2  33643  locfinreflem  33655  cmppcmp  33673  rhmpreimacn  33700  ordtrest2NEWlem  33737  ordtconnlem1  33739  lmdvg  33768  esumpcvgval  33911  esum2d  33926  sigapildsys  33995  ldgenpisyslem1  33996  fiunelros  34007  volmeas  34064  imambfm  34096  omssubadd  34134  carsggect  34152  carsgclctunlem3  34154  sgnmul  34376  signsply0  34397  signstres  34421  actfunsnf1o  34450  actfunsnrndisj  34451  reprsuc  34461  reprinfz1  34468  breprexplema  34476  breprexplemc  34478  breprexp  34479  breprexpnat  34480  circlemeth  34486  hgt750lemb  34502  tgoldbachgtd  34508  erdszelem8  35026  pconnconn  35059  cvmlift2lem12  35142  cvmlift3lem5  35151  cvmlift3lem7  35153  cvmlift3lem8  35154  mrsubrn  35341  msrval  35366  msubff1  35384  btwnconn1lem13  35923  elicc3  36029  neibastop2lem  36072  unbdqndv2  36214  irrdifflemf  37032  ltflcei  37309  lindsenlbs  37316  matunitlindflem1  37317  matunitlindflem2  37318  poimirlem4  37325  poimirlem13  37334  poimirlem14  37335  poimirlem22  37343  poimirlem26  37347  poimirlem27  37348  heicant  37356  mblfinlem2  37359  mblfinlem3  37360  mblfinlem4  37361  cnambfre  37369  itg2addnclem  37372  itg2addnclem2  37373  itg2gt0cn  37376  ftc1cnnc  37393  ftc1anclem5  37398  ftc1anclem7  37400  ftc1anc  37402  equivtotbnd  37479  isbndx  37483  ssbnd  37489  heibor1lem  37510  rrncmslem  37533  islshpat  38715  lfl1dim  38819  lfl1dim2N  38820  lkrpssN  38861  glbconN  39075  glbconNOLD  39076  hlhgt2  39088  3dim2  39167  3dim3  39168  islln3  39209  islvol5  39278  2lplnja  39318  dalem19  39381  isline4N  39476  2polssN  39614  lhpmatb  39730  4atex  39775  trlatn0  39871  cdlemf2  40261  dialss  40745  diaglbN  40754  diaintclN  40757  dibglbN  40865  dibintclN  40866  dihlsscpre  40933  dihglblem5aN  40991  dihglblem2aN  40992  dihglblem4  40996  dihatexv  41037  dihjat1lem  41127  lcfl6  41199  mapdval2N  41329  aks4d1p8  41786  fldhmf1  41789  primrootscoprmpow  41797  primrootscoprbij2  41801  primrootspoweq0  41804  evl1gprodd  41815  hashscontpow  41820  aks6d1c2lem4  41825  idomnnzgmulnz  41831  deg1gprod  41838  sticksstones8  41851  sticksstones12a  41855  aks6d1c6lem3  41870  aks6d1c6lem5  41875  aks6d1c7  41882  aks5lem5a  41889  imacrhmcl  41993  evlsvvval  42035  evlselv  42059  fsuppind  42062  sn-0tie0  42219  prjspertr  42259  prjspreln0  42263  prjspner1  42280  elrfi  42351  eldioph2  42419  diophin  42429  irrapxlem2  42480  irrapxlem3  42481  irrapxlem4  42482  irrapxlem5  42483  pell1234qrne0  42510  pell1234qrreccl  42511  pell1234qrmulcl  42512  pell14qrgt0  42516  pell14qrdich  42526  pell1qrge1  42527  pellfundex  42543  congabseq  42632  jm2.27b  42664  jm2.27  42666  fnwe2lem2  42712  kelac1  42724  lnrfg  42780  hbt  42791  nadd1suc  43058  rfovcnvf1od  43671  ntrneiiso  43758  ntrneikb  43761  ntrneixb  43762  ntrneik3  43763  ntrneix3  43764  ntrneik13  43765  ntrneix13  43766  cvgdvgrat  43987  binomcxplemnotnn0  44030  sineq0ALT  44613  disjf1  44790  supxrgere  44948  supxrgelem  44952  supxrge  44953  suplesup  44954  xralrple2  44969  infxr  44982  infleinflem2  44986  infleinf  44987  uzub  45046  mccl  45219  limcrecl  45250  lptioo2  45252  lptioo1  45253  lptre2pt  45261  addlimc  45269  limsupmnflem  45341  climxrre  45371  liminflimsupclim  45428  climxlim2lem  45466  xlimliminflimsup  45483  icccncfext  45508  cncfiooicclem1  45514  cncfiooiccre  45516  dvbdfbdioolem2  45550  ioodvbdlimc1lem1  45552  dvnxpaek  45563  dvmptfprodlem  45565  dvmptfprod  45566  dvnprodlem3  45569  itgioocnicc  45598  itgspltprt  45600  stoweidlem31  45652  fourierdlem39  45767  fourierdlem42  45770  fourierdlem48  45775  fourierdlem49  45776  fourierdlem50  45777  fourierdlem51  45778  fourierdlem64  45791  fourierdlem65  45792  fourierdlem74  45801  fourierdlem75  45802  fourierdlem81  45808  fourierdlem82  45809  fourierdlem101  45828  etransclem23  45878  etransclem27  45882  etransclem32  45887  etransclem33  45888  etransclem35  45890  etransclem38  45893  sge0tsms  46001  sge0cl  46002  sge0f1o  46003  sge0split  46030  sge0rpcpnf  46042  sge0seq  46067  nnfoctbdjlem  46076  iundjiun  46081  meaiuninc3v  46105  meaiininclem  46107  omeiunltfirp  46140  carageniuncllem2  46143  carageniuncl  46144  hoidmv1lelem1  46212  hoidmvlelem3  46218  hoidmvlelem5  46220  hoidmvle  46221  hoiqssbllem3  46245  iunhoiioolem  46296  pimdecfgtioo  46338  pimincfltioo  46339  preimageiingt  46341  preimaleiinlt  46342  smflimlem4  46395  iccpartigtl  46995  iccpartgt  46999  sprsymrelf1lem  47063  paireqne  47083  proththd  47186  requad2  47195  sbgoldbst  47350  bgoldbtbndlem4  47380  isuspgrim0lem  47450  isuspgrim0  47451  gricushgr  47465  2zrngmmgm  47629  cznrng  47638  rhmsubcALTVlem4  47661  srhmsubcALTV  47702  lincsum  47812  lcoss  47819  snlindsntor  47854  islindeps2  47866  line2x  48142  line2y  48143  itscnhlinecirc02p  48173