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  7212  fimaproj  8060  frxp3  8076  oaabs  8558  oaabs2  8559  omabs  8561  cofon1  8582  sbthlem8  9002  cantnfle  9556  cantnfp1  9566  cantnflem1c  9572  sornom  10160  enfin2i  10204  ttukeylem6  10397  fpwwe2lem12  10525  fpwwe2  10526  winalim2  10579  wuncval2  10630  negf1o  11539  xlemul1a  13179  difreicc  13376  flflp1  13703  faclbnd  14189  swrdswrd  14604  swrdccatin1  14624  pfxccatin12lem3  14631  swrdccat3blem  14638  ello12  15415  lo1bdd2  15423  elo12  15426  rlimclim1  15444  rlimcld2  15477  o1co  15485  o1of2  15512  o1rlimmul  15518  rlimsqzlem  15548  isercoll  15567  o1fsum  15712  supcvg  15755  dvds2ln  16192  lcmgcdlem  16509  cncongr2  16571  isprm5  16610  prmdvdsncoprmbd  16630  pcadd  16793  vdwlem2  16886  vdwlem11  16895  sbcie3s  17065  prdsval  17351  mreexexlem4d  17545  isacs2  17551  catcocl  17583  catass  17584  subccocl  17744  fullsubc  17749  funcco  17770  funcpropd  17801  fullpropd  17821  ffthiso  17830  isnat  17849  natpropd  17878  fucpropd  17879  xpcval  18075  evlf2  18116  curfpropd  18131  curfuncf  18136  uncfcurf  18137  curf2ndf  18145  hofcl  18157  hofpropd  18165  yonffthlem  18180  isacs3lem  18440  acsfiindd  18451  chnind  18519  gsumpropd2lem  18579  resmgmhm2b  18613  resmhm2b  18722  mhmid  18968  mhmmnd  18969  ghmgrp  18971  conjnmzb  19158  ghmqusnsg  19187  ghmquskerlem3  19191  ghmqusker  19192  pgpfi  19510  sylow3lem2  19533  efgredlem  19652  frgpnabllem1  19778  imasabl  19781  dprdfcntz  19922  ablfac1b  19977  pgpfac1lem3  19984  pgpfac1lem5  19986  pgpfaclem3  19990  omndmul2  20038  gsumle  20050  ringinvnzdiv  20212  rnghmsubcsetclem2  20540  rhmsubcsetclem2  20569  srhmsubc  20588  rhmsubclem4  20596  imadrhmcl  20705  cntzsdrg  20710  suborng  20784  islmhm2  20965  lspsneleq  21045  rhmpreimaidl  21207  znunit  21493  psgndiflemB  21530  uvcff  21721  uvcf1  21722  lindfmm  21757  sraassab  21798  psrval  21845  psrass1  21894  resspsrmul  21906  mplbas2  21970  mhpmulcl  22057  psdmul  22074  coe1tmmul  22184  gsummoncoe1  22216  evls1fpws  22277  dmatsubcl  22406  scmatscm  22421  smatvscl  22432  marrepval  22470  mdetdiaglem  22506  mdetunilem8  22527  mdetunilem9  22528  pmatcoe1fsupp  22609  decpmatmulsumfsupp  22681  pmatcollpw2lem  22685  mp2pm2mplem4  22717  pm2mpmhmlem1  22726  pm2mpmhmlem2  22727  pm2mp  22733  fvmptnn04if  22757  cpmadugsumfi  22785  cpmidg2sum  22788  cpmadumatpoly  22791  cayhamlem4  22796  neiptoptop  23039  neitr  23088  ordtrest2lem  23111  cnpnei  23172  iscncl  23177  cncls  23182  cnntr  23183  cncnp  23188  lmcnp  23212  isreg2  23285  hauscmplem  23314  cmpfi  23316  1stcfb  23353  1stcrest  23361  2ndcctbss  23363  2ndcomap  23366  islly2  23392  cldllycmp  23403  lly1stc  23404  locfincmp  23434  llycmpkgen2  23458  1stckgenlem  23461  kgencn2  23465  kgencn3  23466  ptbasfi  23489  ptpjopn  23520  txdis1cn  23543  txlly  23544  txnlly  23545  txtube  23548  txcmplem2  23550  tx1stc  23558  txkgen  23560  xkopt  23563  xkoco2cn  23566  xkococnlem  23567  xkococn  23568  xkoinjcn  23595  tgqtop  23620  regr1lem  23647  kqreglem1  23649  nrmhmph  23702  rnelfmlem  23860  rnelfm  23861  fmfnfmlem4  23865  fmfnfm  23866  ufldom  23870  flimopn  23883  hauspwpwf1  23895  fclsopn  23922  fclsnei  23927  fclsrest  23932  alexsublem  23952  alexsubALTlem3  23957  ptcmplem2  23961  ptcmplem3  23962  cnextfun  23972  cnextcn  23975  symgtgp  24014  tgpt0  24027  qustgpopn  24028  tsmsxplem1  24061  trust  24137  utopsnneiplem  24155  utop3cls  24159  utopreg  24160  isucn2  24186  cstucnd  24191  ucncn  24192  fmucnd  24199  cfilufg  24200  neipcfilu  24203  met2ndci  24430  prdsxmslem2  24437  metcnp3  24448  metustid  24462  metustexhalf  24464  metust  24466  psmetutop  24475  nmoleub  24639  reconnlem2  24736  xrge0tsms  24743  cncfco  24820  lebnumlem3  24882  lebnum  24883  nmoleub2lem2  25036  nmoleub3  25039  iscfil2  25186  iscau4  25199  iscmet3lem2  25212  equivcfil  25219  equivcau  25220  caubl  25228  rrxdstprj1  25329  ovolshftlem2  25431  ovolicc2lem4  25441  uniioombl  25510  i1fmulclem  25623  mbfi1fseqlem6  25641  itg2const2  25662  itg2split  25670  bddiblnc  25763  ellimc2  25798  ellimc3  25800  limcflf  25802  dvmptfsum  25899  dvferm1  25909  dvferm2  25911  dvlip2  25920  c1lip1  25922  lhop1  25939  ftc1a  25964  ply1divex  26062  plyeq0lem  26135  plymullem1  26139  coemullem  26175  coemulc  26180  ulmshftlem  26318  ulmcaulem  26323  ulmbdd  26327  ulmcn  26328  ulmdvlem3  26331  mtestbdd  26334  pserulm  26351  pserdvlem2  26358  abelthlem8  26369  xrlimcnp  26898  jensen  26919  lgamucov  26968  logfac2  27148  dchrelbas3  27169  dchrpt  27198  gausslemma2dlem1a  27296  lgsquad3  27318  2sqb  27363  rpvmasumlem  27418  dchrisumlem1  27420  dchrisumlem3  27422  dchrmusum2  27425  dchrvmasumlem2  27429  dchrisum0flblem1  27439  dchrisum0lem1b  27446  dchrisum0lem1  27447  dchrisum0  27451  mulog2sumlem2  27466  pntlem3  27540  ostth3  27569  slerec  27753  cofcutr  27861  remulscllem2  28396  istrkgcb  28427  tgbtwndiff  28477  iscgrglt  28485  tgcgrxfr  28489  motcgrg  28515  lnext  28538  tgbtwnconn1  28546  tgbtwnconn3  28548  legval  28555  legtrid  28562  legso  28570  hlcgreu  28589  tglnne  28599  tglineeltr  28602  tglnne0  28611  colline  28620  tglowdim2l  28621  tglowdim2ln  28622  mirreu3  28625  mirbtwnhl  28651  krippenlem  28661  midexlem  28663  perpcom  28684  perpneq  28685  footexALT  28689  footex  28692  colperpexlem3  28703  colperpex  28704  opphllem  28706  midex  28708  oppne3  28714  opptgdim2  28716  oppnid  28717  opphllem2  28719  opphllem5  28722  opphllem6  28723  oppperpex  28724  outpasch  28726  hlpasch  28727  lnopp2hpgb  28734  hpgerlem  28736  colopp  28740  colhp  28741  lmieu  28755  lnperpex  28774  trgcopy  28775  trgcopyeulem  28776  iscgra1  28781  cgrane1  28783  cgrane2  28784  cgrane3  28785  cgrane4  28786  cgrahl1  28787  cgrahl2  28788  cgracgr  28789  cgraswap  28791  cgracom  28793  cgratr  28794  flatcgra  28795  cgrabtwn  28797  cgrahl  28798  sacgr  28802  acopyeu  28805  cgrg3col4  28824  tgasa1  28829  f1otrg  28842  f1otrge  28843  axeuclidlem  28933  axcontlem2  28936  umgrvad2edg  29184  usgredg2vlem2  29197  pthdepisspth  29706  clwwlkccatlem  29959  clwlkclwwlklem2  29970  3cycld  30148  eupth2lems  30208  eucrctshift  30213  frgr3vlem2  30244  n4cyclfrgr  30261  numclwwlk1lem2f1  30327  numclwwlk2lem1  30346  ubthlem3  30842  chirredlem1  32360  chirredlem3  32362  cdj1i  32403  fnpreimac  32643  xrge0infss  32733  nn0xmulclb  32744  hashxpe  32779  sgnmul  32808  2exple2exp  32818  ccatf1  32920  ccatws1f1o  32922  swrdf1  32927  dfmgc2lem  32966  mgcf1o  32974  mndlactf1  32997  mndlactfo  32998  mndractf1  32999  mndractfo  33000  gsumfs2d  33025  gsumhashmul  33031  xrge0tsmsd  33032  gsumwun  33035  psgnfzto1stlem  33059  cycpmco2  33092  cycpmrn  33102  tocyccntz  33103  cycpmconjslem2  33114  cyc3conja  33116  conjga  33129  submarchi  33145  isarchiofld  33158  elrgspnlem1  33199  elrgspnlem2  33200  elrgspnlem3  33201  elrgspnlem4  33202  elrgspnsubrunlem1  33204  elrgspnsubrunlem2  33205  elrgspnsubrun  33206  erlval  33215  erler  33222  rloccring  33227  rlocf1  33230  domnprodn0  33232  subrdom  33241  imaslmod  33308  znfermltl  33321  lindfpropd  33337  unitprodclb  33344  nsgmgc  33367  nsgqusf1olem1  33368  unitpidl1  33379  elrspunidl  33383  elrspunsn  33384  rhmimaidl  33387  drngidl  33388  qsidomlem1  33407  mxidlprm  33425  mxidlirredi  33426  drngmxidlr  33433  qsdrngilem  33449  qsdrngi  33450  rsprprmprmidl  33477  rsprprmprmidlb  33478  rprmasso2  33481  rprmirred  33486  rprmirredb  33487  rprmdvdspow  33488  1arithidom  33492  pidufd  33498  1arithufdlem3  33501  dfufd2  33505  ply1dg3rt0irred  33536  mplvrpmga  33565  mplvrpmmhm  33566  mplvrpmrhm  33567  esplymhp  33579  exsslsb  33599  lbslelsp  33600  ply1degltdimlem  33625  lindsunlem  33627  lindsun  33628  lbsdiflsp0  33629  dimkerim  33630  fedgmul  33634  dimlssid  33635  assalactf1o  33638  extdg1id  33669  evls1fldgencl  33673  fldextrspunlsplem  33676  fldextrspunlsp  33677  extdgfialglem1  33695  minplyirred  33714  fldext2chn  33731  cos9thpiminplylem2  33786  smatrcl  33799  1smat1  33807  submateq  33812  mdetpmtr1  33826  madjusmdetlem2  33831  locfinreflem  33843  cmppcmp  33861  rhmpreimacn  33888  ordtrest2NEWlem  33925  ordtconnlem1  33927  lmdvg  33956  zrhcntr  33982  esumpcvgval  34081  esum2d  34096  sigapildsys  34165  ldgenpisyslem1  34166  fiunelros  34177  volmeas  34234  imambfm  34265  omssubadd  34303  carsggect  34321  carsgclctunlem3  34323  signsply0  34554  signstres  34578  actfunsnf1o  34607  actfunsnrndisj  34608  reprsuc  34618  reprinfz1  34625  breprexplema  34633  breprexplemc  34635  breprexp  34636  breprexpnat  34637  circlemeth  34643  hgt750lemb  34659  tgoldbachgtd  34665  erdszelem8  35210  pconnconn  35243  cvmlift2lem12  35326  cvmlift3lem5  35335  cvmlift3lem7  35337  cvmlift3lem8  35338  fmla1  35399  mrsubrn  35525  msrval  35550  msubff1  35568  btwnconn1lem13  36112  elicc3  36330  neibastop2lem  36373  weiunfr  36480  unbdqndv2  36524  irrdifflemf  37338  ltflcei  37627  lindsenlbs  37634  matunitlindflem1  37635  matunitlindflem2  37636  poimirlem4  37643  poimirlem13  37652  poimirlem14  37653  poimirlem22  37661  poimirlem26  37665  poimirlem27  37666  heicant  37674  mblfinlem2  37677  mblfinlem3  37678  mblfinlem4  37679  cnambfre  37687  itg2addnclem  37690  itg2addnclem2  37691  itg2gt0cn  37694  ftc1cnnc  37711  ftc1anclem5  37716  ftc1anclem7  37718  ftc1anc  37720  equivtotbnd  37797  isbndx  37801  ssbnd  37807  heibor1lem  37828  rrncmslem  37851  islshpat  39035  lfl1dim  39139  lfl1dim2N  39140  lkrpssN  39181  glbconN  39395  hlhgt2  39407  3dim2  39486  3dim3  39487  islln3  39528  islvol5  39597  2lplnja  39637  dalem19  39700  isline4N  39795  2polssN  39933  lhpmatb  40049  4atex  40094  trlatn0  40190  cdlemf2  40580  dialss  41064  diaglbN  41073  diaintclN  41076  dibglbN  41184  dibintclN  41185  dihlsscpre  41252  dihglblem5aN  41310  dihglblem2aN  41311  dihglblem4  41315  dihatexv  41356  dihjat1lem  41446  lcfl6  41518  mapdval2N  41648  aks4d1p8  42099  fldhmf1  42102  primrootscoprmpow  42111  primrootscoprbij2  42115  primrootspoweq0  42118  evl1gprodd  42129  hashscontpow  42134  aks6d1c2lem4  42139  idomnnzgmulnz  42145  deg1gprod  42152  sticksstones8  42165  sticksstones12a  42169  aks6d1c6lem3  42184  aks6d1c6lem5  42189  aks6d1c7  42196  aks5lem5a  42203  unitscyglem2  42208  sn-0tie0  42463  imacrhmcl  42526  fiabv  42548  evlsvvval  42575  evlselv  42599  fsuppind  42602  prjspertr  42617  prjspreln0  42621  prjspner1  42638  elrfi  42706  eldioph2  42774  diophin  42784  irrapxlem2  42835  irrapxlem3  42836  irrapxlem4  42837  irrapxlem5  42838  pell1234qrne0  42865  pell1234qrreccl  42866  pell1234qrmulcl  42867  pell14qrgt0  42871  pell14qrdich  42881  pell1qrge1  42882  pellfundex  42898  congabseq  42986  jm2.27b  43018  jm2.27  43020  fnwe2lem2  43063  kelac1  43075  lnrfg  43131  hbt  43142  omabs2  43344  nadd1suc  43404  rfovcnvf1od  44016  ntrneiiso  44103  ntrneikb  44106  ntrneixb  44107  ntrneik3  44108  ntrneix3  44109  ntrneik13  44110  ntrneix13  44111  cvgdvgrat  44325  binomcxplemnotnn0  44368  sineq0ALT  44948  fnchoice  45045  disjf1  45199  supxrgere  45351  supxrgelem  45355  supxrge  45356  suplesup  45357  xralrple2  45372  infxr  45384  infleinflem2  45388  infleinf  45389  uzub  45448  mccl  45617  limcrecl  45648  lptioo2  45650  lptioo1  45651  lptre2pt  45657  addlimc  45665  limsupmnflem  45737  climxrre  45767  liminflimsupclim  45824  climxlim2lem  45862  xlimliminflimsup  45879  icccncfext  45904  cncfiooicclem1  45910  cncfiooiccre  45912  dvbdfbdioolem2  45946  ioodvbdlimc1lem1  45948  dvnxpaek  45959  dvmptfprodlem  45961  dvmptfprod  45962  dvnprodlem3  45965  itgioocnicc  45994  itgspltprt  45996  stoweidlem31  46048  fourierdlem39  46163  fourierdlem42  46166  fourierdlem48  46171  fourierdlem49  46172  fourierdlem50  46173  fourierdlem51  46174  fourierdlem64  46187  fourierdlem65  46188  fourierdlem74  46197  fourierdlem75  46198  fourierdlem81  46204  fourierdlem82  46205  fourierdlem101  46224  etransclem23  46274  etransclem27  46278  etransclem32  46283  etransclem33  46284  etransclem35  46286  etransclem38  46289  sge0tsms  46397  sge0cl  46398  sge0f1o  46399  sge0split  46426  sge0rpcpnf  46438  sge0seq  46463  nnfoctbdjlem  46472  iundjiun  46477  meaiuninc3v  46501  meaiininclem  46503  omeiunltfirp  46536  carageniuncllem2  46539  carageniuncl  46540  hoidmv1lelem1  46608  hoidmvlelem3  46614  hoidmvlelem5  46616  hoidmvle  46617  hoiqssbllem3  46641  iunhoiioolem  46692  pimdecfgtioo  46734  pimincfltioo  46735  preimageiingt  46737  preimaleiinlt  46738  smflimlem4  46791  iccpartigtl  47433  iccpartgt  47437  sprsymrelf1lem  47501  paireqne  47521  proththd  47624  requad2  47633  sbgoldbst  47788  bgoldbtbndlem4  47818  isuspgrim0lem  47903  isuspgrim0  47904  isuspgrimlem  47905  gricushgr  47927  grimedg  47945  grimgrtri  47959  isubgr3stgrlem7  47982  gpgusgralem  48066  pgn4cyclex  48136  2zrngmmgm  48262  cznrng  48271  rhmsubcALTVlem4  48294  srhmsubcALTV  48335  lincsum  48440  lcoss  48447  snlindsntor  48482  islindeps2  48494  line2x  48765  line2y  48766  itscnhlinecirc02p  48796  discsubc  49075  imasubc3  49167  uppropd  49192  swapfval  49273  fucofvalg  49329  fuco21  49347  precofvalALT  49379  2arwcat  49611  lanup  49652  ranup  49653