Theorem ad3antrrr 742

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

Syntax hints:   → wi 4   ∧ wa 400

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 401

This theorem is referenced by:  ad4antr  744  ad4antlr  745  simplll  786  fsnex  7283  fimaproj  8132  frxp3  8148  oaabs  8635  oaabs2  8636  omabs  8638  cofon1  8659  sbthlem8  9083  cantnfle  9641  cantnfp1  9651  cantnflem1c  9657  sornom  10262  enfin2i  10306  ttukeylem6  10499  fpwwe2lem12  10628  fpwwe2  10629  winalim2  10682  wuncval2  10733  negf1o  11645  xlemul1a  13315  difreicc  13512  flflp1  13842  faclbnd  14328  swrdswrd  14744  swrdccatin1  14764  pfxccatin12lem3  14771  swrdccat3blem  14778  sgnmul  15146  ello12  15569  lo1bdd2  15577  elo12  15580  rlimclim1  15598  rlimcld2  15631  o1co  15639  o1of2  15666  o1rlimmul  15672  rlimsqzlem  15702  isercoll  15721  o1fsum  15867  supcvg  15912  dvds2ln  16348  lcmgcdlem  16665  cncongr2  16727  isprm5  16767  prmdvdsncoprmbd  16787  pcadd  16950  vdwlem2  17043  vdwlem11  17052  sbcie3s  17223  prdsval  17509  mreexexlem4d  17704  isacs2  17710  catcocl  17742  catass  17743  subccocl  17903  fullsubc  17908  funcco  17929  funcpropd  17960  fullpropd  17980  ffthiso  17989  isnat  18008  natpropd  18037  fucpropd  18038  xpcval  18234  evlf2  18275  curfpropd  18290  curfuncf  18295  uncfcurf  18296  curf2ndf  18304  hofcl  18316  hofpropd  18324  yonffthlem  18339  isacs3lem  18599  acsfiindd  18610  chnind  18678  gsumpropd2lem  18738  resmgmhm2b  18772  resmhm2b  18882  mhmid  19130  mhmmnd  19131  ghmgrp  19133  conjnmzb  19324  ghmqusnsg  19353  ghmquskerlem3  19357  ghmqusker  19358  pgpfi  19676  sylow3lem2  19699  efgredlem  19818  frgpnabllem1  19944  imasabl  19947  dprdfcntz  20088  ablfac1b  20143  pgpfac1lem3  20150  pgpfac1lem5  20152  pgpfaclem3  20156  omndmul2  20204  gsumle  20216  ringinvnzdiv  20385  rnghmsubcsetclem2  20718  rhmsubcsetclem2  20747  srhmsubc  20766  rhmsubclem4  20774  imadrhmcl  20881  cntzsdrg  20886  suborng  20960  islmhm2  21140  lspsneleq  21220  drngidl  21366  rhmpreimaidl  21397  qsidomlem1  21461  prmidlsubm  21468  znunit  21694  psgndiflemB  21731  uvcff  21922  uvcf1  21923  lindfmm  21958  sraassab  21999  psrval  22046  psrass1  22094  resspsrmul  22106  mplbas2  22174  evlsvvval  22225  mhpmulcl  22293  psdmul  22310  coe1tmmul  22419  gsummoncoe1  22449  evls1fpws  22510  dmatsubcl  22636  scmatscm  22651  smatvscl  22662  marrepval  22700  mdetdiaglem  22736  mdetunilem8  22757  mdetunilem9  22758  pmatcoe1fsupp  22839  decpmatmulsumfsupp  22911  pmatcollpw2lem  22915  mp2pm2mplem4  22947  pm2mpmhmlem1  22956  pm2mpmhmlem2  22957  pm2mp  22963  fvmptnn04if  22987  cpmadugsumfi  23015  cpmidg2sum  23018  cpmadumatpoly  23021  cayhamlem4  23026  neiptoptop  23269  neitr  23318  ordtrest2lem  23341  cnpnei  23402  iscncl  23407  cncls  23412  cnntr  23413  cncnp  23418  lmcnp  23442  isreg2  23515  hauscmplem  23544  cmpfi  23546  1stcfb  23583  1stcrest  23591  2ndcctbss  23593  2ndcomap  23596  islly2  23622  cldllycmp  23633  lly1stc  23634  locfincmp  23664  llycmpkgen2  23688  1stckgenlem  23691  kgencn2  23695  kgencn3  23696  ptbasfi  23719  ptpjopn  23750  txdis1cn  23773  txlly  23774  txnlly  23775  txtube  23778  txcmplem2  23780  tx1stc  23788  txkgen  23790  xkopt  23793  xkoco2cn  23796  xkococnlem  23797  xkococn  23798  xkoinjcn  23825  tgqtop  23850  regr1lem  23877  kqreglem1  23879  nrmhmph  23932  rnelfmlem  24090  rnelfm  24091  fmfnfmlem4  24095  fmfnfm  24096  ufldom  24100  flimopn  24113  hauspwpwf1  24125  fclsopn  24152  fclsnei  24157  fclsrest  24162  alexsublem  24182  alexsubALTlem3  24187  ptcmplem2  24191  ptcmplem3  24192  cnextfun  24202  cnextcn  24205  symgtgp  24244  tgpt0  24257  qustgpopn  24258  tsmsxplem1  24291  trust  24367  utopsnneiplem  24385  utop3cls  24389  utopreg  24390  isucn2  24416  cstucnd  24421  ucncn  24422  fmucnd  24429  cfilufg  24430  neipcfilu  24433  met2ndci  24660  prdsxmslem2  24667  metcnp3  24678  metustid  24692  metustexhalf  24694  metust  24696  psmetutop  24705  nmoleub  24869  reconnlem2  24966  xrge0tsms  24973  cncfco  25047  lebnumlem3  25103  lebnum  25104  nmoleub2lem2  25256  nmoleub3  25259  iscfil2  25406  iscau4  25419  iscmet3lem2  25432  equivcfil  25439  equivcau  25440  caubl  25448  rrxdstprj1  25549  ovolshftlem2  25650  ovolicc2lem4  25660  uniioombl  25729  i1fmulclem  25842  mbfi1fseqlem6  25860  itg2const2  25881  itg2split  25889  bddiblnc  25982  ellimc2  26017  ellimc3  26019  limcflf  26021  dvmptfsum  26115  dvferm1  26125  dvferm2  26127  dvlip2  26135  c1lip1  26137  lhop1  26154  ftc1a  26177  ply1divex  26275  plyeq0lem  26348  plymullem1  26352  coemullem  26388  coemulc  26393  ulmshftlem  26530  ulmcaulem  26535  ulmbdd  26539  ulmcn  26540  ulmdvlem3  26543  mtestbdd  26546  pserulm  26563  pserdvlem2  26569  abelthlem8  26580  xrlimcnp  27111  jensen  27131  lgamucov  27180  logfac2  27359  dchrelbas3  27380  dchrpt  27409  gausslemma2dlem1a  27507  lgsquad3  27529  2sqb  27574  rpvmasumlem  27629  dchrisumlem1  27631  dchrisumlem3  27633  dchrmusum2  27636  dchrvmasumlem2  27640  dchrisum0flblem1  27650  dchrisum0lem1b  27657  dchrisum0lem1  27658  dchrisum0  27662  mulog2sumlem2  27677  pntlem3  27751  ostth3  27780  lesrec  27970  cofcutr  28095  remulscllem2  28672  istrkgcb  28703  tgbtwndiff  28753  iscgrglt  28761  tgcgrxfr  28765  motcgrg  28791  lnext  28814  tgbtwnconn1  28822  tgbtwnconn3  28824  legval  28831  legtrid  28838  legso  28846  hlcgreu  28868  tglnne  28879  tglineeltr  28882  tglnne0  28892  colline  28901  tglowdim2l  28902  tglowdim2ln  28903  mirreu3  28909  mirbtwnhl  28935  krippenlem  28945  midexlem  28947  perpcom  28971  perpneq  28972  footexALT  28976  footex  28979  colperpexlem3  28991  colperpex  28992  opphllem  28994  midex  28996  oppne3  29002  opptgdim2  29004  oppnid  29005  opphllem2  29007  opphllem5  29010  opphllem6  29011  oppperpex  29012  outpasch  29015  hlpasch  29016  lnopp2hpgb  29023  hpgerlem  29025  colopp  29029  colhp  29030  plngrnssp  29039  lnincplng  29044  plngrotlem1  29047  plngrotlem2  29048  plngrotlem3  29049  lnssplnglem  29051  lmieu  29071  lnperpex  29091  trgcopy  29093  trgcopyeulem  29094  iscgra1  29099  cgrane1  29101  cgrane2  29102  cgrane3  29103  cgrane4  29104  cgrahl1  29105  cgrahl2  29106  cgracgr  29107  cgraswap  29109  cgracom  29111  cgratr  29112  flatcgra  29113  cgrabtwn  29115  cgrahl  29116  sacgr  29120  acopyeu  29123  ragcgra  29124  cgrg3col4  29148  tgasa1  29153  prlnghpg  29174  dfprlng2  29175  perpprlng  29178  prlngex  29179  prlngmolem1  29180  prlngmolem2  29181  prlngplngtr  29187  prlngmid2  29189  quadcgrprlng  29194  f1otrg  29198  f1otrge  29199  axeuclidlem  29290  axcontlem2  29293  umgrvad2edg  29541  usgredg2vlem2  29554  pthdepisspth  30062  clwwlkccatlem  30318  clwlkclwwlklem2  30329  3cycld  30507  eupth2lems  30567  eucrctshift  30572  frgr3vlem2  30603  n4cyclfrgr  30620  numclwwlk1lem2f1  30686  numclwwlk2lem1  30705  ubthlem3  31202  chirredlem1  32720  chirredlem3  32722  cdj1i  32763  fnpreimac  32993  xrge0infss  33083  nn0xmulclb  33094  hashxpe  33130  2exple2exp  33156  ccatf1  33247  ccatws1f1o  33249  swrdf1  33254  dfmgc2lem  33293  mgcf1o  33301  mndlactf1  33324  mndlactfo  33325  mndractf1  33326  mndractfo  33327  gsumfs2d  33359  gsumhashmul  33365  suppgsumssiun  33370  xrge0tsmsd  33371  gsumwun  33374  psgnfzto1stlem  33398  cycpmco2  33431  cycpmrn  33441  tocyccntz  33442  cycpmconjslem2  33453  cyc3conja  33455  conjga  33468  submarchi  33484  isarchiofld  33497  elrgspnlem1  33540  elrgspnlem2  33541  elrgspnlem3  33542  elrgspnlem4  33543  elrgspnsubrunlem1  33545  elrgspnsubrunlem2  33546  elrgspnsubrun  33547  erlval  33556  erler  33563  rloccring  33569  rlocf1  33572  rlocisunit  33574  domnprodn0  33576  domnprodeq0  33577  subrdom  33583  imaslmod  33651  znfermltl  33659  lindfpropd  33673  unitprodclb  33680  nsgmgc  33699  nsgqusf1olem1  33700  unitpidl1  33710  elrspunidl  33714  elrspunsn  33715  rhmimaidl  33718  mxidlprm  33731  mxidlirredi  33732  drngmxidlr  33738  qsdrngilem  33754  qsdrngi  33755  drnglring  33760  dflringlem2  33763  dflring3  33765  dflring4  33766  rsprprmprmidl  33790  rsprprmprmidlb  33791  rprmasso2  33794  rprmirred  33799  rprmirredb  33800  rprmdvdspow  33801  1arithidom  33805  pidufd  33811  1arithufdlem3  33814  dfufd2  33818  deg1prod  33851  ply1dg3rt0irred  33852  0mplrim  33882  mplidomlem  33895  extvfvcl  33904  mplvrpmga  33913  mplvrpmmhm  33914  mplvrpmrhm  33915  psrgsum  33916  psrmonprod  33920  esplymhp  33936  esplyfval3  33940  esplyfval1  33941  esplyfvaln  33942  esplyind  33943  exsslsb  33965  lbslelsp  33966  ply1degltdimlem  33990  lindsunlem  33992  lindsun  33993  lbsdiflsp0  33994  dimkerim  33995  fedgmul  33999  dimlssid  34000  assalactf1o  34003  extdg1id  34034  evls1fldgencl  34038  fldextrspunlsplem  34041  fldextrspunlsp  34042  extdgfialglem1  34060  minplyirred  34079  fldext2chn  34096  cos9thpiminplylem2  34151  smatrcl  34164  1smat1  34172  submateq  34177  mdetpmtr1  34191  madjusmdetlem2  34196  locfinreflem  34208  cmppcmp  34226  rhmpreimacn  34253  ordtrest2NEWlem  34290  ordtconnlem1  34292  lmdvg  34321  zrhcntr  34347  esumpcvgval  34446  esum2d  34461  sigapildsys  34530  ldgenpisyslem1  34531  fiunelros  34542  volmeas  34599  imambfm  34630  omssubadd  34668  carsggect  34686  carsgclctunlem3  34688  signsply0  34916  signstres  34940  actfunsnf1o  34969  actfunsnrndisj  34970  reprsuc  34980  reprinfz1  34987  breprexplema  34995  breprexplemc  34997  breprexp  34998  breprexpnat  34999  circlemeth  35005  hgt750lemb  35021  tgoldbachgtd  35027  erdszelem8  35668  pconnconn  35701  cvmlift2lem12  35784  cvmlift3lem5  35793  cvmlift3lem7  35795  cvmlift3lem8  35796  fmla1  35857  mrsubrn  35983  msrval  36008  msubff1  36026  btwnconn1lem13  36569  elicc3  36806  neibastop2lem  36849  weiunfr  36956  unbdqndv2  37078  irrdifflemf  37947  ltflcei  38237  lindsenlbs  38244  matunitlindflem1  38245  matunitlindflem2  38246  poimirlem4  38253  poimirlem13  38262  poimirlem14  38263  poimirlem22  38271  poimirlem26  38275  poimirlem27  38276  heicant  38284  mblfinlem2  38287  mblfinlem3  38288  mblfinlem4  38289  cnambfre  38297  itg2addnclem  38300  itg2addnclem2  38301  itg2gt0cn  38304  ftc1cnnc  38321  ftc1anclem5  38326  ftc1anclem7  38328  ftc1anc  38330  equivtotbnd  38407  isbndx  38411  ssbnd  38417  heibor1lem  38438  rrncmslem  38461  islshpat  39769  lfl1dim  39873  lfl1dim2N  39874  lkrpssN  39915  glbconN  40129  hlhgt2  40141  3dim2  40220  3dim3  40221  islln3  40262  islvol5  40331  2lplnja  40371  dalem19  40434  isline4N  40529  2polssN  40667  lhpmatb  40783  4atex  40828  trlatn0  40924  cdlemf2  41314  dialss  41798  diaglbN  41807  diaintclN  41810  dibglbN  41918  dibintclN  41919  dihlsscpre  41986  dihglblem5aN  42044  dihglblem2aN  42045  dihglblem4  42049  dihatexv  42090  dihjat1lem  42180  lcfl6  42252  mapdval2N  42382  aks4d1p8  42832  fldhmf1  42835  primrootscoprmpow  42844  primrootscoprbij2  42848  primrootspoweq0  42851  evl1gprodd  42862  hashscontpow  42867  aks6d1c2lem4  42872  idomnnzgmulnz  42878  deg1gprod  42885  sticksstones8  42898  sticksstones12a  42902  aks6d1c6lem3  42917  aks6d1c6lem5  42922  aks6d1c7  42929  aks5lem5a  42936  unitscyglem2  42941  sn-0tie0  43203  imacrhmcl  43266  fiabv  43284  evlselv  43301  fsuppind  43302  prjspertr  43317  prjspreln0  43321  prjspner1  43338  elrfi  43405  eldioph2  43473  diophin  43483  irrapxlem2  43530  irrapxlem3  43531  irrapxlem4  43532  irrapxlem5  43533  pell1234qrne0  43560  pell1234qrreccl  43561  pell1234qrmulcl  43562  pell14qrgt0  43566  pell14qrdich  43576  pell1qrge1  43577  pellfundex  43593  congabseq  43681  jm2.27b  43713  jm2.27  43715  fnwe2lem2  43758  kelac1  43770  lnrfg  43826  hbt  43837  omabs2  44039  nadd1suc  44099  rfovcnvf1od  44710  ntrneiiso  44797  ntrneikb  44800  ntrneixb  44801  ntrneik3  44802  ntrneix3  44803  ntrneik13  44804  ntrneix13  44805  cvgdvgrat  45003  binomcxplemnotnn0  45046  sineq0ALT  45625  fnchoice  45729  disjf1  45881  supxrgere  46029  supxrgelem  46033  supxrge  46034  suplesup  46035  xralrple2  46050  infxr  46062  infleinflem2  46066  infleinf  46067  uzub  46125  mccl  46294  limcrecl  46325  lptioo2  46327  lptioo1  46328  lptre2pt  46334  addlimc  46342  limsupmnflem  46414  climxrre  46444  liminflimsupclim  46501  climxlim2lem  46539  xlimliminflimsup  46556  icccncfext  46581  cncfiooicclem1  46587  cncfiooiccre  46589  dvbdfbdioolem2  46623  ioodvbdlimc1lem1  46625  dvnxpaek  46636  dvmptfprodlem  46638  dvmptfprod  46639  dvnprodlem3  46642  itgioocnicc  46671  itgspltprt  46673  stoweidlem31  46725  fourierdlem39  46840  fourierdlem42  46843  fourierdlem48  46848  fourierdlem49  46849  fourierdlem50  46850  fourierdlem51  46851  fourierdlem64  46864  fourierdlem65  46865  fourierdlem74  46874  fourierdlem75  46875  fourierdlem81  46881  fourierdlem82  46882  fourierdlem101  46901  etransclem23  46951  etransclem27  46955  etransclem32  46960  etransclem33  46961  etransclem35  46963  etransclem38  46966  sge0tsms  47074  sge0cl  47075  sge0f1o  47076  sge0split  47103  sge0rpcpnf  47115  sge0seq  47140  nnfoctbdjlem  47149  iundjiun  47154  meaiuninc3v  47178  meaiininclem  47180  omeiunltfirp  47213  carageniuncllem2  47216  carageniuncl  47217  hoicvr  47242  hoidmv1lelem1  47285  hoidmvlelem3  47291  hoidmvlelem5  47293  hoidmvle  47294  hoiqssbllem3  47318  iunhoiioolem  47369  pimdecfgtioo  47411  pimincfltioo  47412  preimageiingt  47414  preimaleiinlt  47415  smflimlem4  47468  chnerlem1  47578  iccpartigtl  48149  iccpartgt  48153  sprsymrelf1lem  48217  paireqne  48237  proththd  48343  requad2  48365  sbgoldbst  48520  bgoldbtbndlem4  48550  isuspgrim0lem  48635  isuspgrim0  48636  isuspgrimlem  48637  gricushgr  48659  grimedg  48677  grimgrtri  48691  isubgr3stgrlem7  48714  gpgusgralem  48798  pgn4cyclex  48868  2zrngmmgm  48994  cznrng  49003  rhmsubcALTVlem4  49026  srhmsubcALTV  49067  lincsum  49186  lcoss  49193  snlindsntor  49228  islindeps2  49240  line2x  49511  line2y  49512  itscnhlinecirc02p  49542  discsubc  49819  imasubc3  49911  uppropd  49936  swapfval  50017  fucofvalg  50073  fuco21  50091  precofvalALT  50123  2arwcat  50355  lanup  50396  ranup  50397