Theorem ad3antrrr 743

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ad4antr  745  ad4antlr  746  simplll  787  fsnex  7291  fnwe2lem3  8147  fimaproj  8152  frxp3  8168  oaabs  8657  oaabs2  8658  omabs  8660  cofon1  8681  sbthlem8  9113  cantnfle  9672  cantnfp1  9682  cantnflem1c  9688  sornom  10355  enfin2i  10399  ttukeylem6  10592  fpwwe2lem12  10727  fpwwe2  10728  winalim2  10781  wuncval2  10832  negf1o  11746  xlemul1a  13418  difreicc  13615  flflp1  13947  faclbnd  14434  ccatf1  14736  swrdf1  14799  swrdswrd  14854  swrdccatin1  14874  pfxccatin12lem3  14881  swrdccat3blem  14888  sgnmul  15260  ello12  15683  lo1bdd2  15691  elo12  15694  rlimclim1  15712  rlimcld2  15745  o1co  15753  o1of2  15780  o1rlimmul  15786  rlimsqzlem  15816  isercoll  15835  o1fsum  15980  supcvg  16025  dvds2ln  16459  lcmgcdlem  16781  cncongr2  16843  isprm5  16883  prmdvdsncoprmbd  16903  pcadd  17067  vdwlem2  17160  vdwlem11  17169  sbcie3s  17340  prdsval  17626  mreexexlem4d  17821  isacs2  17827  catcocl  17859  catass  17860  subccocl  18020  fullsubc  18025  funcco  18046  funcpropd  18077  fullpropd  18097  ffthiso  18106  isnat  18125  natpropd  18154  fucpropd  18155  xpcval  18351  evlf2  18392  curfpropd  18407  curfuncf  18412  uncfcurf  18413  curf2ndf  18421  hofcl  18433  hofpropd  18441  yonffthlem  18456  isacs3lem  18716  acsfiindd  18727  chnind  18795  gsumpropd2lem  18868  resmgmhm2b  18902  resmhm2b  19018  mhmid  19273  mhmmnd  19274  ghmgrp  19276  conjnmzb  19467  ghmqusnsg  19496  ghmquskerlem3  19500  ghmqusker  19501  pgpfi  19819  sylow3lem2  19842  efgredlem  19961  frgpnabllem1  20087  imasabl  20090  dprdfcntz  20231  ablfac1b  20286  pgpfac1lem3  20293  pgpfac1lem5  20295  pgpfaclem3  20299  omndmul2  20347  gsumle  20359  ringinvnzdiv  20532  rnghmsubcsetclem2  20884  rhmsubcsetclem2  20913  srhmsubc  20932  rhmsubclem4  20940  imadrhmcl  21054  cntzsdrg  21059  suborng  21133  islmhm2  21313  lspsneleq  21393  drngidl  21539  rhmpreimaidl  21571  qsidomlem1  21636  prmidlsubm  21643  znunit  21869  psgndiflemB  21906  uvcff  22097  uvcf1  22098  lindfmm  22133  lindsenlbs  22157  sraassab  22176  psrval  22223  psrass1  22271  resspsrmul  22283  mplbas2  22351  evlsvvval  22402  mhpmulcl  22470  psdmul  22487  coe1tmmul  22596  gsummoncoe1  22626  evls1fpws  22687  dmatsubcl  22813  scmatscm  22828  smatvscl  22839  marrepval  22877  mdetdiaglem  22913  mdetunilem8  22934  mdetunilem9  22935  matunitlindflem1  22994  matunitlindflem2  22995  pmatcoe1fsupp  23019  decpmatmulsumfsupp  23091  pmatcollpw2lem  23095  mp2pm2mplem4  23127  pm2mpmhmlem1  23136  pm2mpmhmlem2  23137  pm2mp  23143  fvmptnn04if  23167  cpmadugsumfi  23195  cpmidg2sum  23198  cpmadumatpoly  23201  cayhamlem4  23206  neiptoptop  23449  neitr  23498  ordtrest2lem  23521  cnpnei  23582  iscncl  23587  cncls  23592  cnntr  23593  cncnp  23598  lmcnp  23622  isreg2  23695  hauscmplem  23724  cmpfi  23726  1stcfb  23763  1stcrest  23771  2ndcctbss  23774  2ndcomap  23777  islly2  23803  cldllycmp  23814  lly1stc  23815  locfincmp  23845  llycmpkgen2  23869  1stckgenlem  23872  kgencn2  23876  kgencn3  23877  ptbasfi  23900  ptpjopn  23931  txdis1cn  23954  txlly  23955  txnlly  23956  txtube  23959  txcmplem2  23961  tx1stc  23969  txkgen  23971  xkopt  23974  xkoco2cn  23977  xkococnlem  23978  xkococn  23979  xkoinjcn  24006  tgqtop  24031  regr1lem  24058  kqreglem1  24060  nrmhmph  24113  rnelfmlem  24271  rnelfm  24272  fmfnfmlem4  24276  fmfnfm  24277  ufldom  24281  flimopn  24294  hauspwpwf1  24306  fclsopn  24333  fclsnei  24338  fclsrest  24343  alexsublem  24363  alexsubALTlem3  24368  ptcmplem2  24372  ptcmplem3  24373  cnextfun  24383  cnextcn  24386  symgtgp  24425  tgpt0  24438  qustgpopn  24439  tsmsxplem1  24472  trust  24548  utopsnneiplem  24566  utop3cls  24570  utopreg  24571  isucn2  24597  cstucnd  24602  ucncn  24603  fmucnd  24610  cfilufg  24611  neipcfilu  24614  met2ndci  24841  prdsxmslem2  24848  metcnp3  24859  metustid  24873  metustexhalf  24875  metust  24877  psmetutop  24886  nmoleub  25050  reconnlem2  25147  xrge0tsms  25154  cncfco  25228  lebnumlem3  25284  lebnum  25285  nmoleub2lem2  25437  nmoleub3  25440  iscfil2  25587  iscau4  25600  iscmet3lem2  25613  equivcfil  25620  equivcau  25621  caubl  25629  rrxdstprj1  25730  ovolshftlem2  25831  ovolicc2lem4  25841  uniioombl  25910  i1fmulclem  26023  mbfi1fseqlem6  26041  itg2const2  26062  itg2split  26070  bddiblnc  26162  ellimc2  26197  ellimc3  26199  limcflf  26201  dvmptfsum  26295  dvferm1  26305  dvferm2  26307  dvlip2  26315  c1lip1  26317  lhop1  26334  ftc1a  26357  ply1divex  26455  plyeq0lem  26529  plymullem1  26533  coemullem  26569  coemulc  26574  ulmshftlem  26716  ulmcaulem  26721  ulmbdd  26725  ulmcn  26726  ulmdvlem3  26729  mtestbdd  26732  pserulm  26749  pserdvlem2  26755  abelthlem8  26766  xrlimcnp  27296  jensen  27316  lgamucov  27365  logfac2  27544  dchrelbas3  27565  dchrpt  27594  gausslemma2dlem1a  27692  lgsquad3  27714  2sqb  27759  rpvmasumlem  27814  dchrisumlem1  27816  dchrisumlem3  27818  dchrmusum2  27821  dchrvmasumlem2  27825  dchrisum0flblem1  27835  dchrisum0lem1b  27842  dchrisum0lem1  27843  dchrisum0  27847  mulog2sumlem2  27862  pntlem3  27936  ostth3  27965  fltoprmgt3  27996  lesrec  28185  cofcutr  28310  remulscllem2  28887  istrkgcb  28918  tgbtwndiff  28969  iscgrglt  28977  tgcgrxfr  28981  motcgrg  29007  lnext  29030  tgbtwnconn1  29038  tgbtwnconn3  29040  legval  29047  legtrid  29054  legso  29062  hlcgreu  29084  tglnne  29096  tglineeltr  29099  tglnne0  29109  colline  29118  tglowdim2l  29119  tglowdim2ln  29120  mirreu3  29126  mirbtwnhl  29152  krippenlem  29162  midexlem  29164  perpcom  29188  perpneq  29189  footexALT  29193  footex  29196  colperpexlem3  29208  colperpex  29209  opphllem  29211  midex  29213  oppne3  29219  opptgdim2  29221  oppnid  29222  opphllem2  29224  opphllem5  29227  opphllem6  29228  oppperpex  29229  outpasch  29233  hlpasch  29234  lnopp2hpgb  29241  hpgerlem  29243  colopp  29247  colhp  29248  plngrnssp  29257  lnincplng  29262  plngrotlem1  29265  plngrotlem2  29266  plngrotlem3  29267  lnssplnglem  29269  lmieu  29289  lnperpex  29309  trgcopy  29311  trgcopyeulem  29312  iscgra1  29317  cgrane1  29319  cgrane2  29320  cgrane3  29321  cgrane4  29322  cgrahl1  29323  cgrahl2  29324  cgracgr  29325  cgraswap  29327  cgracom  29329  cgratr  29330  zerocgra  29331  flatcgra  29332  cgrabtwn  29334  cgrahl  29335  sacgr  29339  acopyeu  29342  ragcgra  29343  tgaaddcpbllem1  29349  tgaaddcpbllem3  29351  tgaaddcpbl  29352  cgrg3col4  29372  angmgmaddeu1  29379  angmgmaddeu2  29380  angmgmaddeu3  29381  angmgmaddeu4  29382  angmgmaddeu5  29383  angmgmaddeu6  29384  angmgmaddeu7  29385  angmgmaddov2lem  29387  angmgmaddcpbl  29390  angmgmaddrid  29393  angmgm  29397  tgasa1  29403  prlnghpg  29424  dfprlng2  29425  perpprlng  29428  prlngex  29429  prlngmolem1  29430  prlngmolem2  29431  prlngplngtr  29437  prlngmid2  29439  quadcgrprlng  29444  f1otrg  29448  f1otrge  29449  axeuclidlem  29540  axcontlem2  29543  umgrvad2edg  29794  usgredg2vlem2  29807  pthdepisspth  30321  clwwlkccatlem  30580  clwlkclwwlklem2  30591  3cycld  30779  eupth2lems  30839  eucrctshift  30844  frgr3vlem2  30875  n4cyclfrgr  30892  numclwwlk1lem2f1  30958  numclwwlk2lem1  30977  ubthlem3  31474  chirredlem1  32992  chirredlem3  32994  cdj1i  33035  fnpreimac  33264  xrge0infss  33352  nn0xmulclb  33363  hashxpe  33399  2exple2exp  33425  ccatws1f1o  33514  dfmgc2lem  33556  mgcf1o  33564  mndlactf1  33587  mndlactfo  33588  mndractf1  33589  mndractfo  33590  gsumfs2d  33622  gsumhashmul  33628  suppgsumssiun  33633  xrge0tsmsd  33634  gsumwun  33637  psgnfzto1stlem  33661  cycpmco2  33694  cycpmrn  33704  tocyccntz  33705  cycpmconjslem2  33716  cyc3conja  33718  conjga  33731  submarchi  33747  isarchiofld  33760  elrgspnlem1  33803  elrgspnlem2  33804  elrgspnlem3  33805  elrgspnlem4  33806  elrgspnsubrunlem1  33808  elrgspnsubrunlem2  33809  elrgspnsubrun  33810  erlval  33819  erler  33826  rloccring  33832  rlocf1  33835  rlocisunit  33837  domnprodn0  33839  domnprodeq0  33840  subrdom  33846  imaslmod  33914  znfermltl  33922  lindfpropd  33937  unitprodclb  33944  nsgmgc  33963  nsgqusf1olem1  33964  unitpidl1  33974  elrspunidl  33978  elrspunsn  33979  rhmimaidl  33982  mxidlprm  33995  mxidlirredi  33996  drngmxidlr  34002  qsdrngilem  34018  qsdrngi  34019  drnglring  34024  dflringlem2  34027  dflring3  34029  dflring4  34030  rsprprmprmidl  34054  rsprprmprmidlb  34055  rprmasso2  34058  rprmirred  34063  rprmirredb  34064  rprmdvdspow  34065  1arithidom  34069  pidufd  34075  1arithufdlem3  34078  dfufd2  34082  deg1prod  34115  ply1dg3rt0irred  34116  0mplrim  34146  mplidomlem  34159  extvfvcl  34168  mplvrpmga  34177  mplvrpmmhm  34178  mplvrpmrhm  34179  psrgsum  34180  psrmonprod  34184  esplymhp  34200  esplyfval3  34204  esplyfval1  34205  esplyfvaln  34206  esplyind  34207  exsslsb  34229  lbslelsp  34230  ply1degltdimlem  34254  lindsunlem  34256  lindsun  34257  lbsdiflsp0  34258  dimkerim  34259  fedgmul  34263  dimlssid  34264  assalactf1o  34267  extdg1id  34298  evls1fldgencl  34302  fldextrspunlsplem  34305  fldextrspunlsp  34306  extdgfialglem1  34324  minplyirred  34343  fldext2chn  34360  cos9thpiminplylem2  34415  smatrcl  34428  1smat1  34436  submateq  34441  mdetpmtr1  34455  madjusmdetlem2  34460  locfinreflem  34472  cmppcmp  34490  rhmpreimacn  34517  ordtrest2NEWlem  34554  ordtconnlem1  34556  lmdvg  34585  zrhcntr  34611  esumpcvgval  34710  esum2d  34725  sigapildsys  34795  ldgenpisyslem1  34796  fiunelros  34807  volmeas  34864  imambfm  34894  omssubadd  34932  carsggect  34950  carsgclctunlem3  34952  signsply0  35180  signstres  35204  actfunsnf1o  35233  actfunsnrndisj  35234  reprsuc  35244  reprinfz1  35251  breprexplema  35259  breprexplemc  35261  breprexp  35262  breprexpnat  35263  circlemeth  35269  hgt750lemb  35285  tgoldbachgtd  35291  erdszelem8  35963  pconnconn  35996  cvmlift2lem12  36079  cvmlift3lem5  36088  cvmlift3lem7  36090  cvmlift3lem8  36091  fmla1  36152  mrsubrn  36278  msrval  36303  msubff1  36321  btwnconn1lem13  36864  elicc3  37105  neibastop2lem  37148  weiunfr  37255  unbdqndv2  37377  irrdifflemf  38246  ltflcei  38531  poimirlem4  38542  poimirlem13  38551  poimirlem14  38552  poimirlem22  38560  poimirlem26  38564  poimirlem27  38565  heicant  38573  mblfinlem2  38576  mblfinlem3  38577  mblfinlem4  38578  cnambfre  38586  itg2addnclem  38589  itg2addnclem2  38590  itg2gt0cn  38593  ftc1cnnc  38610  ftc1anclem5  38615  ftc1anclem7  38617  ftc1anc  38619  equivtotbnd  38712  isbndx  38716  ssbnd  38722  heibor1lem  38743  rrncmslem  38766  islshpat  40074  lfl1dim  40178  lfl1dim2N  40179  lkrpssN  40220  glbconN  40434  hlhgt2  40446  3dim2  40525  3dim3  40526  islln3  40567  islvol5  40636  2lplnja  40676  dalem19  40739  isline4N  40834  2polssN  40972  lhpmatb  41088  4atex  41133  trlatn0  41229  cdlemf2  41619  dialss  42103  diaglbN  42112  diaintclN  42115  dibglbN  42223  dibintclN  42224  dihlsscpre  42291  dihglblem5aN  42349  dihglblem2aN  42350  dihglblem4  42354  dihatexv  42395  dihjat1lem  42485  lcfl6  42557  mapdval2N  42687  aks4d1p8  43137  fldhmf1  43140  primrootscoprmpow  43149  primrootscoprbij2  43153  primrootspoweq0  43156  evl1gprodd  43167  hashscontpow  43172  aks6d1c2lem4  43177  idomnnzgmulnz  43183  deg1gprod  43190  sticksstones8  43203  sticksstones12a  43207  aks6d1c6lem3  43222  aks6d1c6lem5  43227  aks6d1c7  43234  aks5lem5a  43241  unitscyglem2  43246  sn-0tie0  43515  imacrhmcl  43581  fiabv  43600  evlselv  43617  fsuppind  43618  prjspertr  43633  prjspreln0  43637  elrfi  43704  eldioph2  43772  diophin  43782  irrapxlem2  43829  irrapxlem3  43830  irrapxlem4  43831  irrapxlem5  43832  pell1234qrne0  43859  pell1234qrreccl  43860  pell1234qrmulcl  43861  pell14qrgt0  43865  pell14qrdich  43875  pell1qrge1  43876  pellfundex  43892  congabseq  43980  jm2.27b  44012  jm2.27  44014  kelac1  44064  lnrfg  44120  hbt  44131  omabs2  44333  nadd1suc  44393  rfovcnvf1od  45003  ntrneiiso  45090  ntrneikb  45093  ntrneixb  45094  ntrneik3  45095  ntrneix3  45096  ntrneik13  45097  ntrneix13  45098  cvgdvgrat  45296  binomcxplemnotnn0  45339  sineq0ALT  45918  fnchoice  46045  disjf1  46197  supxrgere  46344  supxrgelem  46348  supxrge  46349  suplesup  46350  xralrple2  46365  infxr  46377  infleinflem2  46381  infleinf  46382  uzub  46440  mccl  46609  limcrecl  46640  lptioo2  46642  lptioo1  46643  lptre2pt  46649  addlimc  46657  limsupmnflem  46729  climxrre  46759  liminflimsupclim  46816  climxlim2lem  46854  xlimliminflimsup  46871  icccncfext  46896  cncfiooicclem1  46902  cncfiooiccre  46904  dvbdfbdioolem2  46938  ioodvbdlimc1lem1  46940  dvnxpaek  46951  dvmptfprodlem  46953  dvmptfprod  46954  dvnprodlem3  46957  itgioocnicc  46986  itgspltprt  46988  stoweidlem31  47040  fourierdlem39  47155  fourierdlem42  47158  fourierdlem48  47163  fourierdlem49  47164  fourierdlem50  47165  fourierdlem51  47166  fourierdlem64  47179  fourierdlem65  47180  fourierdlem74  47189  fourierdlem75  47190  fourierdlem81  47196  fourierdlem82  47197  fourierdlem101  47216  etransclem23  47266  etransclem27  47270  etransclem32  47275  etransclem33  47276  etransclem35  47278  etransclem38  47281  sge0tsms  47389  sge0cl  47390  sge0f1o  47391  sge0split  47418  sge0rpcpnf  47430  sge0seq  47455  nnfoctbdjlem  47464  iundjiun  47469  meaiuninc3v  47493  meaiininclem  47495  omeiunltfirp  47528  carageniuncllem2  47531  carageniuncl  47532  hoicvr  47557  hoidmv1lelem1  47600  hoidmvlelem3  47606  hoidmvlelem5  47608  hoidmvle  47609  hoiqssbllem3  47633  iunhoiioolem  47684  pimdecfgtioo  47726  pimincfltioo  47727  preimageiingt  47729  preimaleiinlt  47730  smflimlem4  47783  iccpartigtl  48504  iccpartgt  48508  sprsymrelf1lem  48572  paireqne  48592  proththd  48698  requad2  48720  sbgoldbst  48875  bgoldbtbndlem4  48905  isuspgrim0lem  48990  isuspgrim0  48991  isuspgrimlem  48992  gricushgr  49014  grimedg  49032  grimgrtri  49046  isubgr3stgrlem7  49069  gpgusgralem  49153  pgn4cyclex  49223  2zrngmmgm  49348  cznrng  49357  rhmsubcALTVlem4  49380  srhmsubcALTV  49421  lincsum  49540  lcoss  49547  snlindsntor  49582  islindeps2  49594  line2x  49865  line2y  49866  itscnhlinecirc02p  49896  discsubc  50171  imasubc3  50263  uppropd  50288  swapfval  50369  fucofvalg  50425  fuco21  50443  precofvalALT  50475  2arwcat  50707  lanup  50748  ranup  50749