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  7275  fimaproj  8132  frxp3  8148  oaabs  8658  oaabs2  8659  omabs  8661  cofon1  8682  undomOLD  9072  sbthlem8  9102  findcard3OLD  9289  cantnfle  9683  cantnfp1  9693  cantnflem1c  9699  sornom  10289  enfin2i  10333  ttukeylem6  10526  fpwwe2lem12  10654  fpwwe2  10655  winalim2  10708  wuncval2  10759  negf1o  11665  xlemul1a  13302  difreicc  13499  flflp1  13822  faclbnd  14306  swrdswrd  14721  swrdccatin1  14741  pfxccatin12lem3  14748  swrdccat3blem  14755  ello12  15530  lo1bdd2  15538  elo12  15541  rlimclim1  15559  rlimcld2  15592  o1co  15600  o1of2  15627  o1rlimmul  15633  rlimsqzlem  15663  isercoll  15682  o1fsum  15827  supcvg  15870  dvds2ln  16306  lcmgcdlem  16623  cncongr2  16685  isprm5  16724  prmdvdsncoprmbd  16744  pcadd  16907  vdwlem2  17000  vdwlem11  17009  sbcie3s  17179  prdsval  17467  mreexexlem4d  17657  isacs2  17663  catcocl  17695  catass  17696  subccocl  17856  fullsubc  17861  funcco  17882  funcpropd  17913  fullpropd  17933  ffthiso  17942  isnat  17961  natpropd  17990  fucpropd  17991  xpcval  18187  evlf2  18228  curfpropd  18243  curfuncf  18248  uncfcurf  18249  curf2ndf  18257  hofcl  18269  hofpropd  18277  yonffthlem  18292  isacs3lem  18550  acsfiindd  18561  gsumpropd2lem  18655  resmgmhm2b  18689  resmhm2b  18798  mhmid  19044  mhmmnd  19045  ghmgrp  19047  conjnmzb  19234  ghmqusnsg  19263  ghmquskerlem3  19267  ghmqusker  19268  pgpfi  19584  sylow3lem2  19607  efgredlem  19726  frgpnabllem1  19852  imasabl  19855  dprdfcntz  19996  ablfac1b  20051  pgpfac1lem3  20058  pgpfac1lem5  20060  pgpfaclem3  20064  ringinvnzdiv  20259  rnghmsubcsetclem2  20590  rhmsubcsetclem2  20619  srhmsubc  20638  rhmsubclem4  20646  imadrhmcl  20755  cntzsdrg  20760  islmhm2  20994  lspsneleq  21074  rhmpreimaidl  21236  znunit  21522  psgndiflemB  21558  uvcff  21749  uvcf1  21750  lindfmm  21785  sraassab  21826  psrval  21873  psrass1  21922  resspsrmul  21934  mplbas2  21998  mhpmulcl  22085  psdmul  22102  coe1tmmul  22212  gsummoncoe1  22244  evls1fpws  22305  dmatsubcl  22434  scmatscm  22449  smatvscl  22460  marrepval  22498  mdetdiaglem  22534  mdetunilem8  22555  mdetunilem9  22556  pmatcoe1fsupp  22637  decpmatmulsumfsupp  22709  pmatcollpw2lem  22713  mp2pm2mplem4  22745  pm2mpmhmlem1  22754  pm2mpmhmlem2  22755  pm2mp  22761  fvmptnn04if  22785  cpmadugsumfi  22813  cpmidg2sum  22816  cpmadumatpoly  22819  cayhamlem4  22824  neiptoptop  23067  neitr  23116  ordtrest2lem  23139  cnpnei  23200  iscncl  23205  cncls  23210  cnntr  23211  cncnp  23216  lmcnp  23240  isreg2  23313  hauscmplem  23342  cmpfi  23344  1stcfb  23381  1stcrest  23389  2ndcctbss  23391  2ndcomap  23394  islly2  23420  cldllycmp  23431  lly1stc  23432  locfincmp  23462  llycmpkgen2  23486  1stckgenlem  23489  kgencn2  23493  kgencn3  23494  ptbasfi  23517  ptpjopn  23548  txdis1cn  23571  txlly  23572  txnlly  23573  txtube  23576  txcmplem2  23578  tx1stc  23586  txkgen  23588  xkopt  23591  xkoco2cn  23594  xkococnlem  23595  xkococn  23596  xkoinjcn  23623  tgqtop  23648  regr1lem  23675  kqreglem1  23677  nrmhmph  23730  rnelfmlem  23888  rnelfm  23889  fmfnfmlem4  23893  fmfnfm  23894  ufldom  23898  flimopn  23911  hauspwpwf1  23923  fclsopn  23950  fclsnei  23955  fclsrest  23960  alexsublem  23980  alexsubALTlem3  23985  ptcmplem2  23989  ptcmplem3  23990  cnextfun  24000  cnextcn  24003  symgtgp  24042  tgpt0  24055  qustgpopn  24056  tsmsxplem1  24089  trust  24166  utopsnneiplem  24184  utop3cls  24188  utopreg  24189  isucn2  24215  cstucnd  24220  ucncn  24221  fmucnd  24228  cfilufg  24229  neipcfilu  24232  met2ndci  24459  prdsxmslem2  24466  metcnp3  24477  metustid  24491  metustexhalf  24493  metust  24495  psmetutop  24504  nmoleub  24668  reconnlem2  24765  xrge0tsms  24772  cncfco  24849  lebnumlem3  24911  lebnum  24912  nmoleub2lem2  25065  nmoleub3  25068  iscfil2  25216  iscau4  25229  iscmet3lem2  25242  equivcfil  25249  equivcau  25250  caubl  25258  rrxdstprj1  25359  ovolshftlem2  25461  ovolicc2lem4  25471  uniioombl  25540  i1fmulclem  25653  mbfi1fseqlem6  25671  itg2const2  25692  itg2split  25700  bddiblnc  25793  ellimc2  25828  ellimc3  25830  limcflf  25832  dvmptfsum  25929  dvferm1  25939  dvferm2  25941  dvlip2  25950  c1lip1  25952  lhop1  25969  ftc1a  25994  ply1divex  26092  plyeq0lem  26165  plymullem1  26169  coemullem  26205  coemulc  26210  ulmshftlem  26348  ulmcaulem  26353  ulmbdd  26357  ulmcn  26358  ulmdvlem3  26361  mtestbdd  26364  pserulm  26381  pserdvlem2  26388  abelthlem8  26399  xrlimcnp  26928  jensen  26949  lgamucov  26998  logfac2  27178  dchrelbas3  27199  dchrpt  27228  gausslemma2dlem1a  27326  lgsquad3  27348  2sqb  27393  rpvmasumlem  27448  dchrisumlem1  27450  dchrisumlem3  27452  dchrmusum2  27455  dchrvmasumlem2  27459  dchrisum0flblem1  27469  dchrisum0lem1b  27476  dchrisum0lem1  27477  dchrisum0  27481  mulog2sumlem2  27496  pntlem3  27570  ostth3  27599  slerec  27781  cofcutr  27875  remulscllem2  28350  istrkgcb  28381  tgbtwndiff  28431  iscgrglt  28439  tgcgrxfr  28443  motcgrg  28469  lnext  28492  tgbtwnconn1  28500  tgbtwnconn3  28502  legval  28509  legtrid  28516  legso  28524  hlcgreu  28543  tglnne  28553  tglineeltr  28556  tglnne0  28565  colline  28574  tglowdim2l  28575  tglowdim2ln  28576  mirreu3  28579  mirbtwnhl  28605  krippenlem  28615  midexlem  28617  perpcom  28638  perpneq  28639  footexALT  28643  footex  28646  colperpexlem3  28657  colperpex  28658  opphllem  28660  midex  28662  oppne3  28668  opptgdim2  28670  oppnid  28671  opphllem2  28673  opphllem5  28676  opphllem6  28677  oppperpex  28678  outpasch  28680  hlpasch  28681  lnopp2hpgb  28688  hpgerlem  28690  colopp  28694  colhp  28695  lmieu  28709  lnperpex  28728  trgcopy  28729  trgcopyeulem  28730  iscgra1  28735  cgrane1  28737  cgrane2  28738  cgrane3  28739  cgrane4  28740  cgrahl1  28741  cgrahl2  28742  cgracgr  28743  cgraswap  28745  cgracom  28747  cgratr  28748  flatcgra  28749  cgrabtwn  28751  cgrahl  28752  sacgr  28756  acopyeu  28759  cgrg3col4  28778  tgasa1  28783  f1otrg  28796  f1otrge  28797  axeuclidlem  28887  axcontlem2  28890  umgrvad2edg  29138  usgredg2vlem2  29151  pthdepisspth  29663  clwwlkccatlem  29916  clwlkclwwlklem2  29927  3cycld  30105  eupth2lems  30165  eucrctshift  30170  frgr3vlem2  30201  n4cyclfrgr  30218  numclwwlk1lem2f1  30284  numclwwlk2lem1  30303  ubthlem3  30799  chirredlem1  32317  chirredlem3  32319  cdj1i  32360  fnpreimac  32595  xrge0infss  32683  nn0xmulclb  32694  hashxpe  32732  sgnmul  32760  2exple2exp  32770  ccatf1  32870  ccatws1f1o  32873  swrdf1  32878  dfmgc2lem  32921  mgcf1o  32929  chnind  32937  mndlactf1  32967  mndlactfo  32968  mndractf1  32969  mndractfo  32970  gsumfs2d  32995  gsumhashmul  33001  xrge0tsmsd  33002  gsumwun  33005  omndmul2  33026  gsumle  33038  psgnfzto1stlem  33057  cycpmco2  33090  cycpmrn  33100  tocyccntz  33101  cycpmconjslem2  33112  cyc3conja  33114  submarchi  33130  elrgspnlem1  33183  elrgspnlem2  33184  elrgspnlem3  33185  elrgspnlem4  33186  elrgspnsubrunlem1  33188  elrgspnsubrunlem2  33189  elrgspnsubrun  33190  erlval  33199  erler  33206  rloccring  33211  rlocf1  33214  domnprodn0  33216  subrdom  33225  suborng  33283  isarchiofld  33285  imaslmod  33314  znfermltl  33327  lindfpropd  33343  unitprodclb  33350  nsgmgc  33373  nsgqusf1olem1  33374  unitpidl1  33385  elrspunidl  33389  elrspunsn  33390  rhmimaidl  33393  drngidl  33394  qsidomlem1  33413  mxidlprm  33431  mxidlirredi  33432  drngmxidlr  33439  qsdrngilem  33455  qsdrngi  33456  rsprprmprmidl  33483  rsprprmprmidlb  33484  rprmasso2  33487  rprmirred  33492  rprmirredb  33493  rprmdvdspow  33494  1arithidom  33498  pidufd  33504  1arithufdlem3  33507  dfufd2  33511  ply1dg3rt0irred  33541  exsslsb  33582  lbslelsp  33583  ply1degltdimlem  33608  lindsunlem  33610  lindsun  33611  lbsdiflsp0  33612  dimkerim  33613  fedgmul  33617  dimlssid  33618  assalactf1o  33621  extdg1id  33653  evls1fldgencl  33657  fldextrspunlsplem  33660  fldextrspunlsp  33661  minplyirred  33691  fldext2chn  33708  cos9thpiminplylem2  33763  smatrcl  33773  1smat1  33781  submateq  33786  mdetpmtr1  33800  madjusmdetlem2  33805  locfinreflem  33817  cmppcmp  33835  rhmpreimacn  33862  ordtrest2NEWlem  33899  ordtconnlem1  33901  lmdvg  33930  zrhcntr  33956  esumpcvgval  34055  esum2d  34070  sigapildsys  34139  ldgenpisyslem1  34140  fiunelros  34151  volmeas  34208  imambfm  34240  omssubadd  34278  carsggect  34296  carsgclctunlem3  34298  signsply0  34529  signstres  34553  actfunsnf1o  34582  actfunsnrndisj  34583  reprsuc  34593  reprinfz1  34600  breprexplema  34608  breprexplemc  34610  breprexp  34611  breprexpnat  34612  circlemeth  34618  hgt750lemb  34634  tgoldbachgtd  34640  erdszelem8  35166  pconnconn  35199  cvmlift2lem12  35282  cvmlift3lem5  35291  cvmlift3lem7  35293  cvmlift3lem8  35294  fmla1  35355  mrsubrn  35481  msrval  35506  msubff1  35524  btwnconn1lem13  36063  elicc3  36281  neibastop2lem  36324  weiunfr  36431  unbdqndv2  36475  irrdifflemf  37289  ltflcei  37578  lindsenlbs  37585  matunitlindflem1  37586  matunitlindflem2  37587  poimirlem4  37594  poimirlem13  37603  poimirlem14  37604  poimirlem22  37612  poimirlem26  37616  poimirlem27  37617  heicant  37625  mblfinlem2  37628  mblfinlem3  37629  mblfinlem4  37630  cnambfre  37638  itg2addnclem  37641  itg2addnclem2  37642  itg2gt0cn  37645  ftc1cnnc  37662  ftc1anclem5  37667  ftc1anclem7  37669  ftc1anc  37671  equivtotbnd  37748  isbndx  37752  ssbnd  37758  heibor1lem  37779  rrncmslem  37802  islshpat  38981  lfl1dim  39085  lfl1dim2N  39086  lkrpssN  39127  glbconN  39341  glbconNOLD  39342  hlhgt2  39354  3dim2  39433  3dim3  39434  islln3  39475  islvol5  39544  2lplnja  39584  dalem19  39647  isline4N  39742  2polssN  39880  lhpmatb  39996  4atex  40041  trlatn0  40137  cdlemf2  40527  dialss  41011  diaglbN  41020  diaintclN  41023  dibglbN  41131  dibintclN  41132  dihlsscpre  41199  dihglblem5aN  41257  dihglblem2aN  41258  dihglblem4  41262  dihatexv  41303  dihjat1lem  41393  lcfl6  41465  mapdval2N  41595  aks4d1p8  42046  fldhmf1  42049  primrootscoprmpow  42058  primrootscoprbij2  42062  primrootspoweq0  42065  evl1gprodd  42076  hashscontpow  42081  aks6d1c2lem4  42086  idomnnzgmulnz  42092  deg1gprod  42099  sticksstones8  42112  sticksstones12a  42116  aks6d1c6lem3  42131  aks6d1c6lem5  42136  aks6d1c7  42143  aks5lem5a  42150  unitscyglem2  42155  sn-0tie0  42429  imacrhmcl  42484  fiabv  42506  evlsvvval  42533  evlselv  42557  fsuppind  42560  prjspertr  42575  prjspreln0  42579  prjspner1  42596  elrfi  42664  eldioph2  42732  diophin  42742  irrapxlem2  42793  irrapxlem3  42794  irrapxlem4  42795  irrapxlem5  42796  pell1234qrne0  42823  pell1234qrreccl  42824  pell1234qrmulcl  42825  pell14qrgt0  42829  pell14qrdich  42839  pell1qrge1  42840  pellfundex  42856  congabseq  42945  jm2.27b  42977  jm2.27  42979  fnwe2lem2  43022  kelac1  43034  lnrfg  43090  hbt  43101  omabs2  43303  nadd1suc  43363  rfovcnvf1od  43975  ntrneiiso  44062  ntrneikb  44065  ntrneixb  44066  ntrneik3  44067  ntrneix3  44068  ntrneik13  44069  ntrneix13  44070  cvgdvgrat  44285  binomcxplemnotnn0  44328  sineq0ALT  44909  fnchoice  45001  disjf1  45155  supxrgere  45308  supxrgelem  45312  supxrge  45313  suplesup  45314  xralrple2  45329  infxr  45342  infleinflem2  45346  infleinf  45347  uzub  45406  mccl  45575  limcrecl  45606  lptioo2  45608  lptioo1  45609  lptre2pt  45617  addlimc  45625  limsupmnflem  45697  climxrre  45727  liminflimsupclim  45784  climxlim2lem  45822  xlimliminflimsup  45839  icccncfext  45864  cncfiooicclem1  45870  cncfiooiccre  45872  dvbdfbdioolem2  45906  ioodvbdlimc1lem1  45908  dvnxpaek  45919  dvmptfprodlem  45921  dvmptfprod  45922  dvnprodlem3  45925  itgioocnicc  45954  itgspltprt  45956  stoweidlem31  46008  fourierdlem39  46123  fourierdlem42  46126  fourierdlem48  46131  fourierdlem49  46132  fourierdlem50  46133  fourierdlem51  46134  fourierdlem64  46147  fourierdlem65  46148  fourierdlem74  46157  fourierdlem75  46158  fourierdlem81  46164  fourierdlem82  46165  fourierdlem101  46184  etransclem23  46234  etransclem27  46238  etransclem32  46243  etransclem33  46244  etransclem35  46246  etransclem38  46249  sge0tsms  46357  sge0cl  46358  sge0f1o  46359  sge0split  46386  sge0rpcpnf  46398  sge0seq  46423  nnfoctbdjlem  46432  iundjiun  46437  meaiuninc3v  46461  meaiininclem  46463  omeiunltfirp  46496  carageniuncllem2  46499  carageniuncl  46500  hoidmv1lelem1  46568  hoidmvlelem3  46574  hoidmvlelem5  46576  hoidmvle  46577  hoiqssbllem3  46601  iunhoiioolem  46652  pimdecfgtioo  46694  pimincfltioo  46695  preimageiingt  46697  preimaleiinlt  46698  smflimlem4  46751  iccpartigtl  47385  iccpartgt  47389  sprsymrelf1lem  47453  paireqne  47473  proththd  47576  requad2  47585  sbgoldbst  47740  bgoldbtbndlem4  47770  isuspgrim0lem  47854  isuspgrim0  47855  isuspgrimlem  47856  gricushgr  47878  grimedg  47896  grimgrtri  47909  isubgr3stgrlem7  47932  gpgusgralem  48008  2zrngmmgm  48175  cznrng  48184  rhmsubcALTVlem4  48207  srhmsubcALTV  48248  lincsum  48353  lcoss  48360  snlindsntor  48395  islindeps2  48407  line2x  48682  line2y  48683  itscnhlinecirc02p  48713  discsubc  48979  imasubc3  49044  swapfval  49127  fucofvalg  49177  fuco21  49195  precofvalALT  49227  2arwcat  49425  lanup  49463  ranup  49464