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  7314  fnwe2lem3  8174  fimaproj  8179  frxp3  8195  oaabs  8685  oaabs2  8686  omabs  8688  cofon1  8709  sbthlem8  9141  cantnfle  9699  cantnfp1  9709  cantnflem1c  9715  sornom  10382  enfin2i  10426  ttukeylem6  10619  fpwwe2lem12  10754  fpwwe2  10755  winalim2  10808  wuncval2  10859  negf1o  11773  xlemul1a  13445  difreicc  13642  flflp1  13974  faclbnd  14461  ccatf1  14763  swrdf1  14827  swrdswrd  14882  swrdccatin1  14902  pfxccatin12lem3  14909  swrdccat3blem  14916  sgnmul  15289  ello12  15712  lo1bdd2  15720  elo12  15723  rlimclim1  15741  rlimcld2  15774  o1co  15782  o1of2  15809  o1rlimmul  15815  rlimsqzlem  15845  isercoll  15864  o1fsum  16009  supcvg  16054  dvds2ln  16488  lcmgcdlem  16810  cncongr2  16872  isprm5  16912  prmdvdsncoprmbd  16932  pcadd  17096  vdwlem2  17189  vdwlem11  17198  sbcie3s  17369  prdsval  17655  mreexexlem4d  17850  isacs2  17856  catcocl  17888  catass  17889  subccocl  18049  fullsubc  18054  funcco  18075  funcpropd  18106  fullpropd  18126  ffthiso  18135  isnat  18154  natpropd  18183  fucpropd  18184  xpcval  18380  evlf2  18421  curfpropd  18436  curfuncf  18441  uncfcurf  18442  curf2ndf  18450  hofcl  18462  hofpropd  18470  yonffthlem  18485  isacs3lem  18745  acsfiindd  18756  chnind  18824  gsumpropd2lem  18897  resmgmhm2b  18931  resmhm2b  19047  mhmid  19302  mhmmnd  19303  ghmgrp  19305  conjnmzb  19496  ghmqusnsg  19526  ghmquskerlem3  19530  ghmqusker  19531  pgpfi  19849  sylow3lem2  19872  efgredlem  19991  frgpnabllem1  20117  imasabl  20120  dprdfcntz  20261  ablfac1b  20316  pgpfac1lem3  20323  pgpfac1lem5  20325  pgpfaclem3  20329  omndmul2  20377  gsumle  20389  ringinvnzdiv  20562  rnghmsubcsetclem2  20914  rhmsubcsetclem2  20943  srhmsubc  20962  rhmsubclem4  20970  imadrhmcl  21084  cntzsdrg  21089  suborng  21163  islmhm2  21343  lspsneleq  21423  drngidl  21569  rhmpreimaidl  21601  qsidomlem1  21666  prmidlsubm  21673  znunit  21899  psgndiflemB  21936  uvcff  22127  uvcf1  22128  lindfmm  22163  lindsenlbs  22187  sraassab  22206  psrval  22253  psrass1  22301  resspsrmul  22313  mplbas2  22381  evlsvvval  22432  mhpmulcl  22500  psdmul  22517  coe1tmmul  22626  gsummoncoe1  22656  evls1fpws  22717  dmatsubcl  22843  scmatscm  22858  smatvscl  22869  marrepval  22907  mdetdiaglem  22943  mdetunilem8  22964  mdetunilem9  22965  matunitlindflem1  23024  matunitlindflem2  23025  pmatcoe1fsupp  23049  decpmatmulsumfsupp  23121  pmatcollpw2lem  23125  mp2pm2mplem4  23157  pm2mpmhmlem1  23166  pm2mpmhmlem2  23167  pm2mp  23173  fvmptnn04if  23197  cpmadugsumfi  23225  cpmidg2sum  23228  cpmadumatpoly  23231  cayhamlem4  23236  neiptoptop  23479  neitr  23528  ordtrest2lem  23551  cnpnei  23612  iscncl  23617  cncls  23622  cnntr  23623  cncnp  23628  lmcnp  23652  isreg2  23725  hauscmplem  23754  cmpfi  23756  1stcfb  23793  1stcrest  23801  2ndcctbss  23804  2ndcomap  23807  islly2  23833  cldllycmp  23844  lly1stc  23845  locfincmp  23875  llycmpkgen2  23899  1stckgenlem  23902  kgencn2  23906  kgencn3  23907  ptbasfi  23930  ptpjopn  23961  txdis1cn  23984  txlly  23985  txnlly  23986  txtube  23989  txcmplem2  23991  tx1stc  23999  txkgen  24001  xkopt  24004  xkoco2cn  24007  xkococnlem  24008  xkococn  24009  xkoinjcn  24036  tgqtop  24061  regr1lem  24088  kqreglem1  24090  nrmhmph  24143  rnelfmlem  24301  rnelfm  24302  fmfnfmlem4  24306  fmfnfm  24307  ufldom  24311  flimopn  24324  hauspwpwf1  24336  fclsopn  24363  fclsnei  24368  fclsrest  24373  alexsublem  24393  alexsubALTlem3  24398  ptcmplem2  24402  ptcmplem3  24403  cnextfun  24413  cnextcn  24416  symgtgp  24455  tgpt0  24468  qustgpopn  24469  tsmsxplem1  24502  trust  24578  utopsnneiplem  24596  utop3cls  24600  utopreg  24601  isucn2  24627  cstucnd  24632  ucncn  24633  fmucnd  24640  cfilufg  24641  neipcfilu  24644  met2ndci  24871  prdsxmslem2  24878  metcnp3  24889  metustid  24903  metustexhalf  24905  metust  24907  psmetutop  24916  nmoleub  25080  reconnlem2  25177  xrge0tsms  25184  cncfco  25258  lebnumlem3  25314  lebnum  25315  nmoleub2lem2  25467  nmoleub3  25470  iscfil2  25617  iscau4  25630  iscmet3lem2  25643  equivcfil  25650  equivcau  25651  caubl  25659  rrxdstprj1  25760  ovolshftlem2  25861  ovolicc2lem4  25871  uniioombl  25940  i1fmulclem  26053  mbfi1fseqlem6  26071  itg2const2  26092  itg2split  26100  bddiblnc  26192  ellimc2  26227  ellimc3  26229  limcflf  26231  dvmptfsum  26325  dvferm1  26335  dvferm2  26337  dvlip2  26345  c1lip1  26347  lhop1  26364  ftc1a  26387  ply1divex  26485  plyeq0lem  26559  plymullem1  26563  coemullem  26599  coemulc  26604  ulmshftlem  26746  ulmcaulem  26751  ulmbdd  26755  ulmcn  26756  ulmdvlem3  26759  mtestbdd  26762  pserulm  26779  pserdvlem2  26785  abelthlem8  26796  xrlimcnp  27326  jensen  27346  lgamucov  27395  logfac2  27574  dchrelbas3  27595  dchrpt  27624  gausslemma2dlem1a  27722  lgsquad3  27744  2sqb  27789  rpvmasumlem  27844  dchrisumlem1  27846  dchrisumlem3  27848  dchrmusum2  27851  dchrvmasumlem2  27855  dchrisum0flblem1  27865  dchrisum0lem1b  27872  dchrisum0lem1  27873  dchrisum0  27877  mulog2sumlem2  27892  pntlem3  27966  ostth3  27995  fltoprmgt3  28026  lesrec  28215  cofcutr  28340  remulscllem2  28917  istrkgcb  28948  tgbtwndiff  28999  iscgrglt  29007  tgcgrxfr  29011  motcgrg  29037  lnext  29060  tgbtwnconn1  29068  tgbtwnconn3  29070  legval  29077  legtrid  29084  legso  29092  hlcgreu  29114  tglnne  29126  tglineeltr  29129  tglnne0  29139  colline  29148  tglowdim2l  29149  tglowdim2ln  29150  mirreu3  29156  mirbtwnhl  29182  krippenlem  29192  midexlem  29194  perpcom  29218  perpneq  29219  footexALT  29223  footex  29226  colperpexlem3  29238  colperpex  29239  opphllem  29241  midex  29243  oppne3  29249  opptgdim2  29251  oppnid  29252  opphllem2  29254  opphllem5  29257  opphllem6  29258  oppperpex  29259  outpasch  29263  hlpasch  29264  lnopp2hpgb  29271  hpgerlem  29273  colopp  29277  colhp  29278  plngrnssp  29287  lnincplng  29292  plngrotlem1  29295  plngrotlem2  29296  plngrotlem3  29297  lnssplnglem  29299  lmieu  29319  lnperpex  29339  trgcopy  29341  trgcopyeulem  29342  iscgra1  29347  cgrane1  29349  cgrane2  29350  cgrane3  29351  cgrane4  29352  cgrahl1  29353  cgrahl2  29354  cgracgr  29355  cgraswap  29357  cgracom  29359  cgratr  29360  zerocgra  29361  flatcgra  29362  cgrabtwn  29364  cgrahl  29365  sacgr  29369  acopyeu  29372  ragcgra  29373  tgaaddcpbllem1  29379  tgaaddcpbllem3  29381  tgaaddcpbl  29382  cgrg3col4  29402  angmgmaddeu1  29409  angmgmaddeu2  29410  angmgmaddeu3  29411  angmgmaddeu4  29412  angmgmaddeu5  29413  angmgmaddeu6  29414  angmgmaddeu7  29415  angmgmaddov2lem  29417  angmgmaddcpbl  29420  angmgmaddrid  29423  angmgm  29427  tgasa1  29433  prlnghpg  29454  dfprlng2  29455  perpprlng  29458  prlngex  29459  prlngmolem1  29460  prlngmolem2  29461  prlngplngtr  29467  prlngmid2  29469  quadcgrprlng  29474  f1otrg  29478  f1otrge  29479  axeuclidlem  29570  axcontlem2  29573  umgrvad2edg  29824  usgredg2vlem2  29837  pthdepisspth  30351  clwwlkccatlem  30610  clwlkclwwlklem2  30621  3cycld  30809  eupth2lems  30869  eucrctshift  30874  frgr3vlem2  30905  n4cyclfrgr  30922  numclwwlk1lem2f1  30988  numclwwlk2lem1  31007  ubthlem3  31504  chirredlem1  33022  chirredlem3  33024  cdj1i  33065  fnpreimac  33336  xrge0infss  33422  nn0xmulclb  33433  hashxpe  33469  2exple2exp  33495  ccatws1f1o  33584  dfmgc2lem  33626  mgcf1o  33634  mndlactf1  33657  mndlactfo  33658  mndractf1  33659  mndractfo  33660  gsumfs2d  33692  gsumhashmul  33698  suppgsumssiun  33703  xrge0tsmsd  33704  gsumwun  33707  psgnfzto1stlem  33731  cycpmco2  33764  cycpmrn  33774  tocyccntz  33775  cycpmconjslem2  33786  cyc3conja  33788  conjga  33801  submarchi  33817  isarchiofld  33830  elrgspnlem1  33873  elrgspnlem2  33874  elrgspnlem3  33875  elrgspnlem4  33876  elrgspnsubrunlem1  33878  elrgspnsubrunlem2  33879  elrgspnsubrun  33880  erlval  33889  erler  33896  rloccring  33902  rlocf1  33905  rlocisunit  33907  domnprodn0  33909  domnprodeq0  33910  subrdom  33916  imaslmod  33984  znfermltl  33992  lindfpropd  34007  unitprodclb  34014  nsgmgc  34033  nsgqusf1olem1  34034  unitpidl1  34044  elrspunidl  34048  elrspunsn  34049  rhmimaidl  34052  mxidlprm  34065  mxidlirredi  34066  drngmxidlr  34072  qsdrngilem  34088  qsdrngi  34089  drnglring  34094  dflringlem2  34097  dflring3  34099  dflring4  34100  rsprprmprmidl  34124  rsprprmprmidlb  34125  rprmasso2  34128  rprmirred  34133  rprmirredb  34134  rprmdvdspow  34135  1arithidom  34139  pidufd  34145  1arithufdlem3  34148  dfufd2  34152  deg1prod  34185  ply1dg3rt0irred  34186  0mplrim  34216  mplidomlem  34229  extvfvcl  34238  mplvrpmga  34247  mplvrpmmhm  34248  mplvrpmrhm  34249  psrgsum  34250  psrmonprod  34254  esplymhp  34270  esplyfval3  34274  esplyfval1  34275  esplyfvaln  34276  esplyind  34277  exsslsb  34299  lbslelsp  34300  ply1degltdimlem  34324  lindsunlem  34326  lindsun  34327  lbsdiflsp0  34328  dimkerim  34329  fedgmul  34333  dimlssid  34334  assalactf1o  34337  extdg1id  34368  evls1fldgencl  34372  fldextrspunlsplem  34375  fldextrspunlsp  34376  extdgfialglem1  34394  minplyirred  34413  fldext2chn  34430  cos9thpiminplylem2  34485  smatrcl  34498  1smat1  34506  submateq  34511  mdetpmtr1  34525  madjusmdetlem2  34530  locfinreflem  34542  cmppcmp  34560  rhmpreimacn  34587  ordtrest2NEWlem  34624  ordtconnlem1  34626  lmdvg  34655  zrhcntr  34681  esumpcvgval  34780  esum2d  34795  sigapildsys  34865  ldgenpisyslem1  34866  fiunelros  34877  volmeas  34934  imambfm  34964  omssubadd  35002  carsggect  35020  carsgclctunlem3  35022  signsply0  35250  signstres  35274  actfunsnf1o  35303  actfunsnrndisj  35304  reprsuc  35314  reprinfz1  35321  breprexplema  35329  breprexplemc  35331  breprexp  35332  breprexpnat  35333  circlemeth  35339  hgt750lemb  35355  tgoldbachgtd  35361  erdszelem8  36130  pconnconn  36163  cvmlift2lem12  36246  cvmlift3lem5  36255  cvmlift3lem7  36257  cvmlift3lem8  36258  fmla1  36319  mrsubrn  36445  msrval  36470  msubff1  36488  btwnconn1lem13  37042  elicc3  37283  neibastop2lem  37326  weiunfr  37433  unbdqndv2  37555  irrdifflemf  38438  ltflcei  38723  poimirlem4  38734  poimirlem13  38743  poimirlem14  38744  poimirlem22  38752  poimirlem26  38756  poimirlem27  38757  heicant  38765  mblfinlem2  38768  mblfinlem3  38769  mblfinlem4  38770  cnambfre  38778  itg2addnclem  38781  itg2addnclem2  38782  itg2gt0cn  38785  ftc1cnnc  38802  ftc1anclem5  38807  ftc1anclem7  38809  ftc1anc  38811  equivtotbnd  38904  isbndx  38908  ssbnd  38914  heibor1lem  38935  rrncmslem  38958  islshpat  40266  lfl1dim  40370  lfl1dim2N  40371  lkrpssN  40412  glbconN  40626  hlhgt2  40638  3dim2  40717  3dim3  40718  islln3  40759  islvol5  40828  2lplnja  40868  dalem19  40931  isline4N  41026  2polssN  41164  lhpmatb  41280  4atex  41325  trlatn0  41421  cdlemf2  41811  dialss  42295  diaglbN  42304  diaintclN  42307  dibglbN  42415  dibintclN  42416  dihlsscpre  42483  dihglblem5aN  42541  dihglblem2aN  42542  dihglblem4  42546  dihatexv  42587  dihjat1lem  42677  lcfl6  42749  mapdval2N  42879  aks4d1p8  43329  fldhmf1  43332  primrootscoprmpow  43341  primrootscoprbij2  43345  primrootspoweq0  43348  evl1gprodd  43359  hashscontpow  43364  aks6d1c2lem4  43369  idomnnzgmulnz  43375  deg1gprod  43382  sticksstones8  43395  sticksstones12a  43399  aks6d1c6lem3  43414  aks6d1c6lem5  43419  aks6d1c7  43426  aks5lem5a  43433  unitscyglem2  43438  sn-0tie0  43708  imacrhmcl  43774  fiabv  43793  evlselv  43810  fsuppind  43811  prjspertr  43826  prjspreln0  43830  elrfi  43898  eldioph2  43966  diophin  43976  irrapxlem2  44023  irrapxlem3  44024  irrapxlem4  44025  irrapxlem5  44026  pell1234qrne0  44053  pell1234qrreccl  44054  pell1234qrmulcl  44055  pell14qrgt0  44059  pell14qrdich  44069  pell1qrge1  44070  pellfundex  44086  congabseq  44174  jm2.27b  44206  jm2.27  44208  kelac1  44258  lnrfg  44313  hbt  44324  omabs2  44526  nadd1suc  44586  rfovcnvf1od  45196  ntrneiiso  45283  ntrneikb  45286  ntrneixb  45287  ntrneik3  45288  ntrneix3  45289  ntrneik13  45290  ntrneix13  45291  cvgdvgrat  45489  binomcxplemnotnn0  45532  sineq0ALT  46110  fnchoice  46251  disjf1  46403  supxrgere  46550  supxrgelem  46554  supxrge  46555  suplesup  46556  xralrple2  46571  infxr  46583  infleinflem2  46587  infleinf  46588  uzub  46646  mccl  46815  limcrecl  46846  lptioo2  46848  lptioo1  46849  lptre2pt  46855  addlimc  46863  limsupmnflem  46935  climxrre  46965  liminflimsupclim  47022  climxlim2lem  47060  xlimliminflimsup  47077  icccncfext  47102  cncfiooicclem1  47108  cncfiooiccre  47110  dvbdfbdioolem2  47144  ioodvbdlimc1lem1  47146  dvnxpaek  47157  dvmptfprodlem  47159  dvmptfprod  47160  dvnprodlem3  47163  itgioocnicc  47192  itgspltprt  47194  stoweidlem31  47246  fourierdlem39  47361  fourierdlem42  47364  fourierdlem48  47369  fourierdlem49  47370  fourierdlem50  47371  fourierdlem51  47372  fourierdlem64  47385  fourierdlem65  47386  fourierdlem74  47395  fourierdlem75  47396  fourierdlem81  47402  fourierdlem82  47403  fourierdlem101  47422  etransclem23  47472  etransclem27  47476  etransclem32  47481  etransclem33  47482  etransclem35  47484  etransclem38  47487  sge0tsms  47595  sge0cl  47596  sge0f1o  47597  sge0split  47624  sge0rpcpnf  47636  sge0seq  47661  nnfoctbdjlem  47670  iundjiun  47675  meaiuninc3v  47699  meaiininclem  47701  omeiunltfirp  47734  carageniuncllem2  47737  carageniuncl  47738  hoicvr  47763  hoidmv1lelem1  47806  hoidmvlelem3  47812  hoidmvlelem5  47814  hoidmvle  47815  hoiqssbllem3  47839  iunhoiioolem  47890  pimdecfgtioo  47932  pimincfltioo  47933  preimageiingt  47935  preimaleiinlt  47936  smflimlem4  47989  iccpartigtl  48710  iccpartgt  48714  sprsymrelf1lem  48778  paireqne  48798  proththd  48904  requad2  48926  sbgoldbst  49081  bgoldbtbndlem4  49111  isuspgrim0lem  49196  isuspgrim0  49197  isuspgrimlem  49198  gricushgr  49220  grimedg  49238  grimgrtri  49252  isubgr3stgrlem7  49275  gpgusgralem  49359  pgn4cyclex  49429  2zrngmmgm  49554  cznrng  49563  rhmsubcALTVlem4  49586  srhmsubcALTV  49627  lincsum  49746  lcoss  49753  snlindsntor  49788  islindeps2  49800  line2x  50071  line2y  50072  itscnhlinecirc02p  50102  inlinecirc02plem  50103  discsubc  50383  imasubc3  50477  uppropd  50502  swapfval  50589  fucofvalg  50645  fuco21  50663  precofvalALT  50708  2arwcat  50943  lanup  51029  ranup  51030