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  ad5ant12  756  simplll  775  fsnex  7303  fimaproj  8160  frxp3  8176  oaabs  8686  oaabs2  8687  omabs  8689  cofon1  8710  undomOLD  9100  sbthlem8  9130  findcard3OLD  9319  cantnfle  9711  cantnfp1  9721  cantnflem1c  9727  sornom  10317  enfin2i  10361  ttukeylem6  10554  fpwwe2lem12  10682  winalim2  10736  wuncval2  10787  negf1o  11693  xlemul1a  13330  difreicc  13524  flflp1  13847  faclbnd  14329  swrdswrd  14743  pfxccatin12lem3  14770  swrdccat3blem  14777  ello12  15552  elo12  15563  rlimclim1  15581  rlimcld2  15614  o1co  15622  o1of2  15649  o1rlimmul  15655  rlimsqzlem  15685  isercoll  15704  o1fsum  15849  supcvg  15892  dvds2ln  16326  lcmgcdlem  16643  cncongr2  16705  isprm5  16744  prmdvdsncoprmbd  16764  pcadd  16927  vdwlem2  17020  vdwlem11  17029  sbcie3s  17199  prdsval  17500  mreexexlem4d  17690  isacs2  17696  catcocl  17728  catass  17729  subccocl  17890  fullsubc  17895  funcco  17916  fullpropd  17967  ffthiso  17976  isnat  17995  natpropd  18024  fucpropd  18025  xpcval  18222  evlf2  18263  curfpropd  18278  curfuncf  18283  uncfcurf  18284  hofcl  18304  hofpropd  18312  yonffthlem  18327  isacs3lem  18587  acsfiindd  18598  gsumpropd2lem  18692  resmgmhm2b  18726  resmhm2b  18835  mhmid  19081  mhmmnd  19082  ghmgrp  19084  conjnmzb  19271  ghmqusnsg  19300  ghmquskerlem3  19304  ghmqusker  19305  pgpfi  19623  sylow3lem2  19646  efgredlem  19765  frgpnabllem1  19891  imasabl  19894  dprdfcntz  20035  ablfac1b  20090  pgpfac1lem3  20097  pgpfac1lem5  20099  pgpfaclem3  20103  ringinvnzdiv  20298  rnghmsubcsetclem2  20632  rhmsubcsetclem2  20661  srhmsubc  20680  rhmsubclem4  20688  imadrhmcl  20798  cntzsdrg  20803  islmhm2  21037  lspsneleq  21117  rhmpreimaidl  21287  znunit  21582  psgndiflemB  21618  uvcff  21811  uvcf1  21812  lindfmm  21847  sraassab  21888  psrval  21935  psrass1  21984  resspsrmul  21996  mplbas2  22060  mhpmulcl  22153  psdmul  22170  coe1tmmul  22280  gsummoncoe1  22312  evls1fpws  22373  dmatsubcl  22504  scmatscm  22519  smatvscl  22530  marrepval  22568  mdetdiaglem  22604  mdetunilem8  22625  mdetunilem9  22626  pmatcoe1fsupp  22707  decpmatmulsumfsupp  22779  pmatcollpw2lem  22783  mp2pm2mplem4  22815  pm2mpmhmlem1  22824  pm2mpmhmlem2  22825  pm2mp  22831  fvmptnn04if  22855  cpmadugsumfi  22883  cpmidg2sum  22886  cpmadumatpoly  22889  cayhamlem4  22894  neiptoptop  23139  neitr  23188  ordtrest2lem  23211  cnpnei  23272  iscncl  23277  cncls  23282  cnntr  23283  cncnp  23288  lmcnp  23312  isreg2  23385  hauscmplem  23414  cmpfi  23416  1stcfb  23453  1stcrest  23461  2ndcctbss  23463  2ndcomap  23466  islly2  23492  cldllycmp  23503  lly1stc  23504  locfincmp  23534  llycmpkgen2  23558  1stckgenlem  23561  kgencn2  23565  kgencn3  23566  ptbasfi  23589  ptpjopn  23620  txdis1cn  23643  txlly  23644  txnlly  23645  txtube  23648  txcmplem2  23650  tx1stc  23658  txkgen  23660  xkopt  23663  xkoco2cn  23666  xkococnlem  23667  xkococn  23668  xkoinjcn  23695  tgqtop  23720  regr1lem  23747  kqreglem1  23749  nrmhmph  23802  rnelfmlem  23960  rnelfm  23961  fmfnfmlem4  23965  fmfnfm  23966  ufldom  23970  flimopn  23983  hauspwpwf1  23995  fclsopn  24022  fclsnei  24027  fclsrest  24032  alexsublem  24052  alexsubALTlem3  24057  ptcmplem2  24061  ptcmplem3  24062  cnextfun  24072  cnextcn  24075  symgtgp  24114  tgpt0  24127  qustgpopn  24128  tsmsxplem1  24161  trust  24238  utopsnneiplem  24256  utop3cls  24260  utopreg  24261  isucn2  24288  cstucnd  24293  ucncn  24294  fmucnd  24301  cfilufg  24302  neipcfilu  24305  met2ndci  24535  prdsxmslem2  24542  metustid  24567  metustexhalf  24569  metust  24571  psmetutop  24580  nmoleub  24752  reconnlem2  24849  xrge0tsms  24856  cncfco  24933  lebnumlem3  24995  lebnum  24996  nmoleub2lem2  25149  nmoleub3  25152  iscfil2  25300  iscau4  25313  iscmet3lem2  25326  equivcfil  25333  equivcau  25334  caubl  25342  rrxdstprj1  25443  ovolshftlem2  25545  ovolicc2lem4  25555  uniioombl  25624  i1fmulclem  25737  mbfi1fseqlem6  25755  itg2const2  25776  itg2split  25784  bddiblnc  25877  ellimc2  25912  ellimc3  25914  limcflf  25916  dvmptfsum  26013  dvferm1  26023  dvferm2  26025  dvlip2  26034  c1lip1  26036  lhop1  26053  ftc1a  26078  ply1divex  26176  plyeq0lem  26249  plymullem1  26253  coemullem  26289  coemulc  26294  ulmshftlem  26432  ulmcaulem  26437  ulmbdd  26441  ulmcn  26442  ulmdvlem3  26445  mtestbdd  26448  pserulm  26465  pserdvlem2  26472  abelthlem8  26483  xrlimcnp  27011  jensen  27032  lgamucov  27081  logfac2  27261  dchrelbas3  27282  dchrpt  27311  gausslemma2dlem1a  27409  lgsquad3  27431  2sqb  27476  rpvmasumlem  27531  dchrisumlem1  27533  dchrisumlem3  27535  dchrmusum2  27538  dchrvmasumlem2  27542  dchrisum0flblem1  27552  dchrisum0lem1b  27559  dchrisum0lem1  27560  dchrisum0  27564  mulog2sumlem2  27579  pntlem3  27653  ostth3  27682  slerec  27864  cofcutr  27958  remulscllem2  28433  istrkgcb  28464  tgbtwndiff  28514  iscgrglt  28522  tgcgrxfr  28526  motcgrg  28552  lnext  28575  tgbtwnconn1  28583  tgbtwnconn3  28585  legval  28592  legtrid  28599  legso  28607  hlcgreu  28626  tglnne  28636  tglineeltr  28639  tglnne0  28648  colline  28657  tglowdim2l  28658  tglowdim2ln  28659  mirreu3  28662  mirbtwnhl  28688  krippenlem  28698  midexlem  28700  perpcom  28721  footexALT  28726  footex  28729  colperpexlem3  28740  colperpex  28741  opphllem  28743  midex  28745  oppne3  28751  opptgdim2  28753  oppnid  28754  opphllem2  28756  opphllem5  28759  opphllem6  28760  oppperpex  28761  outpasch  28763  hlpasch  28764  lnopp2hpgb  28771  hpgerlem  28773  colopp  28777  colhp  28778  lmieu  28792  lnperpex  28811  trgcopy  28812  trgcopyeulem  28813  iscgra1  28818  cgrane1  28820  cgrane2  28821  cgrane3  28822  cgrane4  28823  cgrahl1  28824  cgrahl2  28825  cgracgr  28826  cgraswap  28828  cgracom  28830  cgratr  28831  flatcgra  28832  cgrabtwn  28834  cgrahl  28835  sacgr  28839  acopyeu  28842  cgrg3col4  28861  tgasa1  28866  f1otrg  28879  f1otrge  28880  axeuclidlem  28977  axcontlem2  28980  umgrvad2edg  29230  usgredg2vlem2  29243  pthdepisspth  29755  clwwlkccatlem  30008  clwlkclwwlklem2  30019  3cycld  30197  eupth2lems  30257  eucrctshift  30262  frgr3vlem2  30293  n4cyclfrgr  30310  numclwwlk1lem2f1  30376  numclwwlk2lem1  30395  ubthlem3  30891  chirredlem1  32409  chirredlem3  32411  cdj1i  32452  fnpreimac  32681  xrge0infss  32764  nn0xmulclb  32775  hashxpe  32811  2exple2exp  32834  ccatf1  32933  ccatws1f1o  32936  swrdf1  32941  dfmgc2lem  32985  mgcf1o  32993  chnind  33001  mndlactf1  33031  mndlactfo  33032  mndractf1  33033  mndractfo  33034  gsumfs2d  33058  gsumhashmul  33064  xrge0tsmsd  33065  gsumwun  33068  omndmul2  33089  gsumle  33101  psgnfzto1stlem  33120  cycpmco2  33153  cycpmrn  33163  tocyccntz  33164  cycpmconjslem2  33175  cyc3conja  33177  submarchi  33193  elrgspnlem1  33246  elrgspnlem2  33247  elrgspnlem3  33248  elrgspnlem4  33249  elrgspnsubrunlem1  33251  elrgspnsubrunlem2  33252  elrgspnsubrun  33253  erlval  33262  erler  33269  rlocf1  33277  domnprodn0  33279  subrdom  33288  suborng  33345  isarchiofld  33347  imaslmod  33381  znfermltl  33394  lindfpropd  33410  unitprodclb  33417  nsgqusf1olem1  33441  unitpidl1  33452  elrspunidl  33456  elrspunsn  33457  rhmimaidl  33460  drngidl  33461  qsidomlem1  33480  mxidlprm  33498  mxidlirredi  33499  qsdrngilem  33522  qsdrngi  33523  rsprprmprmidl  33550  rsprprmprmidlb  33551  rprmasso2  33554  rprmirred  33559  rprmirredb  33560  rprmdvdspow  33561  1arithidom  33565  pidufd  33571  1arithufdlem3  33574  dfufd2  33578  ply1dg3rt0irred  33607  exsslsb  33647  lbslelsp  33648  ply1degltdimlem  33673  lindsunlem  33675  lindsun  33676  lbsdiflsp0  33677  dimkerim  33678  fedgmul  33682  dimlssid  33683  assalactf1o  33686  extdg1id  33716  evls1fldgencl  33720  fldextrspunlsplem  33723  fldextrspunlsp  33724  minplyirred  33754  fldext2chn  33769  smatrcl  33795  1smat1  33803  submateq  33808  mdetpmtr1  33822  madjusmdetlem2  33827  locfinreflem  33839  cmppcmp  33857  rhmpreimacn  33884  ordtrest2NEWlem  33921  ordtconnlem1  33923  lmdvg  33952  zrhcntr  33980  esumpcvgval  34079  esum2d  34094  sigapildsys  34163  ldgenpisyslem1  34164  fiunelros  34175  volmeas  34232  imambfm  34264  omssubadd  34302  carsggect  34320  carsgclctunlem3  34322  sgnmul  34545  signsply0  34566  signstres  34590  actfunsnf1o  34619  actfunsnrndisj  34620  reprsuc  34630  reprinfz1  34637  breprexplema  34645  breprexplemc  34647  breprexp  34648  breprexpnat  34649  circlemeth  34655  hgt750lemb  34671  tgoldbachgtd  34677  erdszelem8  35203  pconnconn  35236  cvmlift2lem12  35319  cvmlift3lem5  35328  cvmlift3lem7  35330  cvmlift3lem8  35331  mrsubrn  35518  msrval  35543  msubff1  35561  btwnconn1lem13  36100  elicc3  36318  neibastop2lem  36361  weiunfr  36468  unbdqndv2  36512  irrdifflemf  37326  ltflcei  37615  lindsenlbs  37622  matunitlindflem1  37623  matunitlindflem2  37624  poimirlem4  37631  poimirlem13  37640  poimirlem14  37641  poimirlem22  37649  poimirlem26  37653  poimirlem27  37654  heicant  37662  mblfinlem2  37665  mblfinlem3  37666  mblfinlem4  37667  cnambfre  37675  itg2addnclem  37678  itg2addnclem2  37679  itg2gt0cn  37682  ftc1cnnc  37699  ftc1anclem5  37704  ftc1anclem7  37706  ftc1anc  37708  equivtotbnd  37785  isbndx  37789  ssbnd  37795  heibor1lem  37816  rrncmslem  37839  islshpat  39018  lfl1dim  39122  lfl1dim2N  39123  lkrpssN  39164  glbconN  39378  glbconNOLD  39379  hlhgt2  39391  3dim2  39470  3dim3  39471  islln3  39512  islvol5  39581  2lplnja  39621  dalem19  39684  isline4N  39779  2polssN  39917  lhpmatb  40033  4atex  40078  trlatn0  40174  cdlemf2  40564  dialss  41048  diaglbN  41057  diaintclN  41060  dibglbN  41168  dibintclN  41169  dihlsscpre  41236  dihglblem5aN  41294  dihglblem2aN  41295  dihglblem4  41299  dihatexv  41340  dihjat1lem  41430  lcfl6  41502  mapdval2N  41632  aks4d1p8  42088  fldhmf1  42091  primrootscoprmpow  42100  primrootscoprbij2  42104  primrootspoweq0  42107  evl1gprodd  42118  hashscontpow  42123  aks6d1c2lem4  42128  idomnnzgmulnz  42134  deg1gprod  42141  sticksstones8  42154  sticksstones12a  42158  aks6d1c6lem3  42173  aks6d1c6lem5  42178  aks6d1c7  42185  aks5lem5a  42192  unitscyglem2  42197  sn-0tie0  42469  imacrhmcl  42524  fiabv  42546  evlsvvval  42573  evlselv  42597  fsuppind  42600  prjspertr  42615  prjspreln0  42619  prjspner1  42636  elrfi  42705  eldioph2  42773  diophin  42783  irrapxlem2  42834  irrapxlem3  42835  irrapxlem4  42836  irrapxlem5  42837  pell1234qrne0  42864  pell1234qrreccl  42865  pell1234qrmulcl  42866  pell14qrgt0  42870  pell14qrdich  42880  pell1qrge1  42881  pellfundex  42897  congabseq  42986  jm2.27b  43018  jm2.27  43020  fnwe2lem2  43063  kelac1  43075  lnrfg  43131  hbt  43142  nadd1suc  43405  rfovcnvf1od  44017  ntrneiiso  44104  ntrneikb  44107  ntrneixb  44108  ntrneik3  44109  ntrneix3  44110  ntrneik13  44111  ntrneix13  44112  cvgdvgrat  44332  binomcxplemnotnn0  44375  sineq0ALT  44957  disjf1  45188  supxrgere  45344  supxrgelem  45348  supxrge  45349  suplesup  45350  xralrple2  45365  infxr  45378  infleinflem2  45382  infleinf  45383  uzub  45442  mccl  45613  limcrecl  45644  lptioo2  45646  lptioo1  45647  lptre2pt  45655  addlimc  45663  limsupmnflem  45735  climxrre  45765  liminflimsupclim  45822  climxlim2lem  45860  xlimliminflimsup  45877  icccncfext  45902  cncfiooicclem1  45908  cncfiooiccre  45910  dvbdfbdioolem2  45944  ioodvbdlimc1lem1  45946  dvnxpaek  45957  dvmptfprodlem  45959  dvmptfprod  45960  dvnprodlem3  45963  itgioocnicc  45992  itgspltprt  45994  stoweidlem31  46046  fourierdlem39  46161  fourierdlem42  46164  fourierdlem48  46169  fourierdlem49  46170  fourierdlem50  46171  fourierdlem51  46172  fourierdlem64  46185  fourierdlem65  46186  fourierdlem74  46195  fourierdlem75  46196  fourierdlem81  46202  fourierdlem82  46203  fourierdlem101  46222  etransclem23  46272  etransclem27  46276  etransclem32  46281  etransclem33  46282  etransclem35  46284  etransclem38  46287  sge0tsms  46395  sge0cl  46396  sge0f1o  46397  sge0split  46424  sge0rpcpnf  46436  sge0seq  46461  nnfoctbdjlem  46470  iundjiun  46475  meaiuninc3v  46499  meaiininclem  46501  omeiunltfirp  46534  carageniuncllem2  46537  carageniuncl  46538  hoidmv1lelem1  46606  hoidmvlelem3  46612  hoidmvlelem5  46614  hoidmvle  46615  hoiqssbllem3  46639  iunhoiioolem  46690  pimdecfgtioo  46732  pimincfltioo  46733  preimageiingt  46735  preimaleiinlt  46736  smflimlem4  46789  iccpartigtl  47410  iccpartgt  47414  sprsymrelf1lem  47478  paireqne  47498  proththd  47601  requad2  47610  sbgoldbst  47765  bgoldbtbndlem4  47795  isuspgrim0lem  47871  isuspgrim0  47872  gricushgr  47886  grimedg  47903  grimgrtri  47916  isubgr3stgrlem7  47939  gpgusgralem  48011  2zrngmmgm  48168  cznrng  48177  rhmsubcALTVlem4  48200  srhmsubcALTV  48241  lincsum  48346  lcoss  48353  snlindsntor  48388  islindeps2  48400  line2x  48675  line2y  48676  itscnhlinecirc02p  48706  swapfval  48968  fucofvalg  49013  fuco21  49031  precofvalALT  49063