Theorem ad3antrrr 731

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 727	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  733  ad4antlr  734  simplll  775  fsnex  7231  fimaproj  8078  frxp3  8094  oaabs  8577  oaabs2  8578  omabs  8580  cofon1  8601  sbthlem8  9025  cantnfle  9583  cantnfp1  9593  cantnflem1c  9599  sornom  10190  enfin2i  10234  ttukeylem6  10427  fpwwe2lem12  10556  fpwwe2  10557  winalim2  10610  wuncval2  10661  negf1o  11571  xlemul1a  13231  difreicc  13428  flflp1  13757  faclbnd  14243  swrdswrd  14658  swrdccatin1  14678  pfxccatin12lem3  14685  swrdccat3blem  14692  ello12  15469  lo1bdd2  15477  elo12  15480  rlimclim1  15498  rlimcld2  15531  o1co  15539  o1of2  15566  o1rlimmul  15572  rlimsqzlem  15602  isercoll  15621  o1fsum  15767  supcvg  15812  dvds2ln  16249  lcmgcdlem  16566  cncongr2  16628  isprm5  16668  prmdvdsncoprmbd  16688  pcadd  16851  vdwlem2  16944  vdwlem11  16953  sbcie3s  17123  prdsval  17409  mreexexlem4d  17604  isacs2  17610  catcocl  17642  catass  17643  subccocl  17803  fullsubc  17808  funcco  17829  funcpropd  17860  fullpropd  17880  ffthiso  17889  isnat  17908  natpropd  17937  fucpropd  17938  xpcval  18134  evlf2  18175  curfpropd  18190  curfuncf  18195  uncfcurf  18196  curf2ndf  18204  hofcl  18216  hofpropd  18224  yonffthlem  18239  isacs3lem  18499  acsfiindd  18510  chnind  18578  gsumpropd2lem  18638  resmgmhm2b  18672  resmhm2b  18781  mhmid  19030  mhmmnd  19031  ghmgrp  19033  conjnmzb  19219  ghmqusnsg  19248  ghmquskerlem3  19252  ghmqusker  19253  pgpfi  19571  sylow3lem2  19594  efgredlem  19713  frgpnabllem1  19839  imasabl  19842  dprdfcntz  19983  ablfac1b  20038  pgpfac1lem3  20045  pgpfac1lem5  20047  pgpfaclem3  20051  omndmul2  20099  gsumle  20111  ringinvnzdiv  20273  rnghmsubcsetclem2  20600  rhmsubcsetclem2  20629  srhmsubc  20648  rhmsubclem4  20656  imadrhmcl  20765  cntzsdrg  20770  suborng  20844  islmhm2  21025  lspsneleq  21105  rhmpreimaidl  21267  znunit  21553  psgndiflemB  21590  uvcff  21781  uvcf1  21782  lindfmm  21817  sraassab  21858  psrval  21905  psrass1  21952  resspsrmul  21964  mplbas2  22030  evlsvvval  22081  mhpmulcl  22125  psdmul  22142  coe1tmmul  22252  gsummoncoe1  22283  evls1fpws  22344  dmatsubcl  22473  scmatscm  22488  smatvscl  22499  marrepval  22537  mdetdiaglem  22573  mdetunilem8  22594  mdetunilem9  22595  pmatcoe1fsupp  22676  decpmatmulsumfsupp  22748  pmatcollpw2lem  22752  mp2pm2mplem4  22784  pm2mpmhmlem1  22793  pm2mpmhmlem2  22794  pm2mp  22800  fvmptnn04if  22824  cpmadugsumfi  22852  cpmidg2sum  22855  cpmadumatpoly  22858  cayhamlem4  22863  neiptoptop  23106  neitr  23155  ordtrest2lem  23178  cnpnei  23239  iscncl  23244  cncls  23249  cnntr  23250  cncnp  23255  lmcnp  23279  isreg2  23352  hauscmplem  23381  cmpfi  23383  1stcfb  23420  1stcrest  23428  2ndcctbss  23430  2ndcomap  23433  islly2  23459  cldllycmp  23470  lly1stc  23471  locfincmp  23501  llycmpkgen2  23525  1stckgenlem  23528  kgencn2  23532  kgencn3  23533  ptbasfi  23556  ptpjopn  23587  txdis1cn  23610  txlly  23611  txnlly  23612  txtube  23615  txcmplem2  23617  tx1stc  23625  txkgen  23627  xkopt  23630  xkoco2cn  23633  xkococnlem  23634  xkococn  23635  xkoinjcn  23662  tgqtop  23687  regr1lem  23714  kqreglem1  23716  nrmhmph  23769  rnelfmlem  23927  rnelfm  23928  fmfnfmlem4  23932  fmfnfm  23933  ufldom  23937  flimopn  23950  hauspwpwf1  23962  fclsopn  23989  fclsnei  23994  fclsrest  23999  alexsublem  24019  alexsubALTlem3  24024  ptcmplem2  24028  ptcmplem3  24029  cnextfun  24039  cnextcn  24042  symgtgp  24081  tgpt0  24094  qustgpopn  24095  tsmsxplem1  24128  trust  24204  utopsnneiplem  24222  utop3cls  24226  utopreg  24227  isucn2  24253  cstucnd  24258  ucncn  24259  fmucnd  24266  cfilufg  24267  neipcfilu  24270  met2ndci  24497  prdsxmslem2  24504  metcnp3  24515  metustid  24529  metustexhalf  24531  metust  24533  psmetutop  24542  nmoleub  24706  reconnlem2  24803  xrge0tsms  24810  cncfco  24884  lebnumlem3  24940  lebnum  24941  nmoleub2lem2  25093  nmoleub3  25096  iscfil2  25243  iscau4  25256  iscmet3lem2  25269  equivcfil  25276  equivcau  25277  caubl  25285  rrxdstprj1  25386  ovolshftlem2  25487  ovolicc2lem4  25497  uniioombl  25566  i1fmulclem  25679  mbfi1fseqlem6  25697  itg2const2  25718  itg2split  25726  bddiblnc  25819  ellimc2  25854  ellimc3  25856  limcflf  25858  dvmptfsum  25952  dvferm1  25962  dvferm2  25964  dvlip2  25972  c1lip1  25974  lhop1  25991  ftc1a  26014  ply1divex  26112  plyeq0lem  26185  plymullem1  26189  coemullem  26225  coemulc  26230  ulmshftlem  26367  ulmcaulem  26372  ulmbdd  26376  ulmcn  26377  ulmdvlem3  26380  mtestbdd  26383  pserulm  26400  pserdvlem2  26406  abelthlem8  26417  xrlimcnp  26945  jensen  26966  lgamucov  27015  logfac2  27194  dchrelbas3  27215  dchrpt  27244  gausslemma2dlem1a  27342  lgsquad3  27364  2sqb  27409  rpvmasumlem  27464  dchrisumlem1  27466  dchrisumlem3  27468  dchrmusum2  27471  dchrvmasumlem2  27475  dchrisum0flblem1  27485  dchrisum0lem1b  27492  dchrisum0lem1  27493  dchrisum0  27497  mulog2sumlem2  27512  pntlem3  27586  ostth3  27615  lesrec  27805  cofcutr  27930  remulscllem2  28507  istrkgcb  28538  tgbtwndiff  28588  iscgrglt  28596  tgcgrxfr  28600  motcgrg  28626  lnext  28649  tgbtwnconn1  28657  tgbtwnconn3  28659  legval  28666  legtrid  28673  legso  28681  hlcgreu  28700  tglnne  28710  tglineeltr  28713  tglnne0  28722  colline  28731  tglowdim2l  28732  tglowdim2ln  28733  mirreu3  28736  mirbtwnhl  28762  krippenlem  28772  midexlem  28774  perpcom  28795  perpneq  28796  footexALT  28800  footex  28803  colperpexlem3  28814  colperpex  28815  opphllem  28817  midex  28819  oppne3  28825  opptgdim2  28827  oppnid  28828  opphllem2  28830  opphllem5  28833  opphllem6  28834  oppperpex  28835  outpasch  28837  hlpasch  28838  lnopp2hpgb  28845  hpgerlem  28847  colopp  28851  colhp  28852  lmieu  28866  lnperpex  28885  trgcopy  28886  trgcopyeulem  28887  iscgra1  28892  cgrane1  28894  cgrane2  28895  cgrane3  28896  cgrane4  28897  cgrahl1  28898  cgrahl2  28899  cgracgr  28900  cgraswap  28902  cgracom  28904  cgratr  28905  flatcgra  28906  cgrabtwn  28908  cgrahl  28909  sacgr  28913  acopyeu  28916  cgrg3col4  28935  tgasa1  28940  f1otrg  28953  f1otrge  28954  axeuclidlem  29045  axcontlem2  29048  umgrvad2edg  29296  usgredg2vlem2  29309  pthdepisspth  29818  clwwlkccatlem  30074  clwlkclwwlklem2  30085  3cycld  30263  eupth2lems  30323  eucrctshift  30328  frgr3vlem2  30359  n4cyclfrgr  30376  numclwwlk1lem2f1  30442  numclwwlk2lem1  30461  ubthlem3  30958  chirredlem1  32476  chirredlem3  32478  cdj1i  32519  fnpreimac  32758  xrge0infss  32848  nn0xmulclb  32859  hashxpe  32895  sgnmul  32923  2exple2exp  32933  ccatf1  33024  ccatws1f1o  33026  swrdf1  33031  dfmgc2lem  33070  mgcf1o  33078  mndlactf1  33101  mndlactfo  33102  mndractf1  33103  mndractfo  33104  gsumfs2d  33137  gsumhashmul  33143  suppgsumssiun  33148  xrge0tsmsd  33149  gsumwun  33152  psgnfzto1stlem  33176  cycpmco2  33209  cycpmrn  33219  tocyccntz  33220  cycpmconjslem2  33231  cyc3conja  33233  conjga  33246  submarchi  33262  isarchiofld  33275  elrgspnlem1  33318  elrgspnlem2  33319  elrgspnlem3  33320  elrgspnlem4  33321  elrgspnsubrunlem1  33323  elrgspnsubrunlem2  33324  elrgspnsubrun  33325  erlval  33334  erler  33341  rloccring  33346  rlocf1  33349  domnprodn0  33351  domnprodeq0  33352  subrdom  33361  imaslmod  33428  znfermltl  33441  lindfpropd  33457  unitprodclb  33464  nsgmgc  33487  nsgqusf1olem1  33488  unitpidl1  33499  elrspunidl  33503  elrspunsn  33504  rhmimaidl  33507  drngidl  33508  qsidomlem1  33527  mxidlprm  33545  mxidlirredi  33546  drngmxidlr  33553  qsdrngilem  33569  qsdrngi  33570  rsprprmprmidl  33597  rsprprmprmidlb  33598  rprmasso2  33601  rprmirred  33606  rprmirredb  33607  rprmdvdspow  33608  1arithidom  33612  pidufd  33618  1arithufdlem3  33621  dfufd2  33625  deg1prod  33658  ply1dg3rt0irred  33659  extvfvcl  33695  mplvrpmga  33704  mplvrpmmhm  33705  mplvrpmrhm  33706  psrgsum  33707  psrmonprod  33711  esplymhp  33727  esplyfval3  33731  esplyfval1  33732  esplyfvaln  33733  esplyind  33734  exsslsb  33756  lbslelsp  33757  ply1degltdimlem  33782  lindsunlem  33784  lindsun  33785  lbsdiflsp0  33786  dimkerim  33787  fedgmul  33791  dimlssid  33792  assalactf1o  33795  extdg1id  33826  evls1fldgencl  33830  fldextrspunlsplem  33833  fldextrspunlsp  33834  extdgfialglem1  33852  minplyirred  33871  fldext2chn  33888  cos9thpiminplylem2  33943  smatrcl  33956  1smat1  33964  submateq  33969  mdetpmtr1  33983  madjusmdetlem2  33988  locfinreflem  34000  cmppcmp  34018  rhmpreimacn  34045  ordtrest2NEWlem  34082  ordtconnlem1  34084  lmdvg  34113  zrhcntr  34139  esumpcvgval  34238  esum2d  34253  sigapildsys  34322  ldgenpisyslem1  34323  fiunelros  34334  volmeas  34391  imambfm  34422  omssubadd  34460  carsggect  34478  carsgclctunlem3  34480  signsply0  34711  signstres  34735  actfunsnf1o  34764  actfunsnrndisj  34765  reprsuc  34775  reprinfz1  34782  breprexplema  34790  breprexplemc  34792  breprexp  34793  breprexpnat  34794  circlemeth  34800  hgt750lemb  34816  tgoldbachgtd  34822  erdszelem8  35396  pconnconn  35429  cvmlift2lem12  35512  cvmlift3lem5  35521  cvmlift3lem7  35523  cvmlift3lem8  35524  fmla1  35585  mrsubrn  35711  msrval  35736  msubff1  35754  btwnconn1lem13  36297  elicc3  36515  neibastop2lem  36558  weiunfr  36665  unbdqndv2  36787  irrdifflemf  37655  ltflcei  37943  lindsenlbs  37950  matunitlindflem1  37951  matunitlindflem2  37952  poimirlem4  37959  poimirlem13  37968  poimirlem14  37969  poimirlem22  37977  poimirlem26  37981  poimirlem27  37982  heicant  37990  mblfinlem2  37993  mblfinlem3  37994  mblfinlem4  37995  cnambfre  38003  itg2addnclem  38006  itg2addnclem2  38007  itg2gt0cn  38010  ftc1cnnc  38027  ftc1anclem5  38032  ftc1anclem7  38034  ftc1anc  38036  equivtotbnd  38113  isbndx  38117  ssbnd  38123  heibor1lem  38144  rrncmslem  38167  islshpat  39477  lfl1dim  39581  lfl1dim2N  39582  lkrpssN  39623  glbconN  39837  hlhgt2  39849  3dim2  39928  3dim3  39929  islln3  39970  islvol5  40039  2lplnja  40079  dalem19  40142  isline4N  40237  2polssN  40375  lhpmatb  40491  4atex  40536  trlatn0  40632  cdlemf2  41022  dialss  41506  diaglbN  41515  diaintclN  41518  dibglbN  41626  dibintclN  41627  dihlsscpre  41694  dihglblem5aN  41752  dihglblem2aN  41753  dihglblem4  41757  dihatexv  41798  dihjat1lem  41888  lcfl6  41960  mapdval2N  42090  aks4d1p8  42540  fldhmf1  42543  primrootscoprmpow  42552  primrootscoprbij2  42556  primrootspoweq0  42559  evl1gprodd  42570  hashscontpow  42575  aks6d1c2lem4  42580  idomnnzgmulnz  42586  deg1gprod  42593  sticksstones8  42606  sticksstones12a  42610  aks6d1c6lem3  42625  aks6d1c6lem5  42630  aks6d1c7  42637  aks5lem5a  42644  unitscyglem2  42649  sn-0tie0  42910  imacrhmcl  42973  fiabv  42995  evlselv  43034  fsuppind  43037  prjspertr  43052  prjspreln0  43056  prjspner1  43073  elrfi  43140  eldioph2  43208  diophin  43218  irrapxlem2  43269  irrapxlem3  43270  irrapxlem4  43271  irrapxlem5  43272  pell1234qrne0  43299  pell1234qrreccl  43300  pell1234qrmulcl  43301  pell14qrgt0  43305  pell14qrdich  43315  pell1qrge1  43316  pellfundex  43332  congabseq  43420  jm2.27b  43452  jm2.27  43454  fnwe2lem2  43497  kelac1  43509  lnrfg  43565  hbt  43576  omabs2  43778  nadd1suc  43838  rfovcnvf1od  44449  ntrneiiso  44536  ntrneikb  44539  ntrneixb  44540  ntrneik3  44541  ntrneix3  44542  ntrneik13  44543  ntrneix13  44544  cvgdvgrat  44758  binomcxplemnotnn0  44801  sineq0ALT  45381  fnchoice  45478  disjf1  45631  supxrgere  45781  supxrgelem  45785  supxrge  45786  suplesup  45787  xralrple2  45802  infxr  45814  infleinflem2  45818  infleinf  45819  uzub  45877  mccl  46046  limcrecl  46077  lptioo2  46079  lptioo1  46080  lptre2pt  46086  addlimc  46094  limsupmnflem  46166  climxrre  46196  liminflimsupclim  46253  climxlim2lem  46291  xlimliminflimsup  46308  icccncfext  46333  cncfiooicclem1  46339  cncfiooiccre  46341  dvbdfbdioolem2  46375  ioodvbdlimc1lem1  46377  dvnxpaek  46388  dvmptfprodlem  46390  dvmptfprod  46391  dvnprodlem3  46394  itgioocnicc  46423  itgspltprt  46425  stoweidlem31  46477  fourierdlem39  46592  fourierdlem42  46595  fourierdlem48  46600  fourierdlem49  46601  fourierdlem50  46602  fourierdlem51  46603  fourierdlem64  46616  fourierdlem65  46617  fourierdlem74  46626  fourierdlem75  46627  fourierdlem81  46633  fourierdlem82  46634  fourierdlem101  46653  etransclem23  46703  etransclem27  46707  etransclem32  46712  etransclem33  46713  etransclem35  46715  etransclem38  46718  sge0tsms  46826  sge0cl  46827  sge0f1o  46828  sge0split  46855  sge0rpcpnf  46867  sge0seq  46892  nnfoctbdjlem  46901  iundjiun  46906  meaiuninc3v  46930  meaiininclem  46932  omeiunltfirp  46965  carageniuncllem2  46968  carageniuncl  46969  hoicvr  46994  hoidmv1lelem1  47037  hoidmvlelem3  47043  hoidmvlelem5  47045  hoidmvle  47046  hoiqssbllem3  47070  iunhoiioolem  47121  pimdecfgtioo  47163  pimincfltioo  47164  preimageiingt  47166  preimaleiinlt  47167  smflimlem4  47220  chnerlem1  47328  iccpartigtl  47895  iccpartgt  47899  sprsymrelf1lem  47963  paireqne  47983  proththd  48089  requad2  48111  sbgoldbst  48266  bgoldbtbndlem4  48296  isuspgrim0lem  48381  isuspgrim0  48382  isuspgrimlem  48383  gricushgr  48405  grimedg  48423  grimgrtri  48437  isubgr3stgrlem7  48460  gpgusgralem  48544  pgn4cyclex  48614  2zrngmmgm  48740  cznrng  48749  rhmsubcALTVlem4  48772  srhmsubcALTV  48813  lincsum  48917  lcoss  48924  snlindsntor  48959  islindeps2  48971  line2x  49242  line2y  49243  itscnhlinecirc02p  49273  discsubc  49551  imasubc3  49643  uppropd  49668  swapfval  49749  fucofvalg  49805  fuco21  49823  precofvalALT  49855  2arwcat  50087  lanup  50128  ranup  50129