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  7283  fimaproj  8136  frxp3  8152  oaabs  8641  oaabs2  8642  omabs  8644  cofon1  8665  sbthlem8  9097  cantnfle  9656  cantnfp1  9666  cantnflem1c  9672  sornom  10336  enfin2i  10380  ttukeylem6  10573  fpwwe2lem12  10708  fpwwe2  10709  winalim2  10762  wuncval2  10813  negf1o  11727  xlemul1a  13399  difreicc  13596  flflp1  13927  faclbnd  14414  ccatf1  14716  swrdf1  14779  swrdswrd  14834  swrdccatin1  14854  pfxccatin12lem3  14861  swrdccat3blem  14868  sgnmul  15240  ello12  15663  lo1bdd2  15671  elo12  15674  rlimclim1  15692  rlimcld2  15725  o1co  15733  o1of2  15760  o1rlimmul  15766  rlimsqzlem  15796  isercoll  15815  o1fsum  15960  supcvg  16005  dvds2ln  16439  lcmgcdlem  16761  cncongr2  16823  isprm5  16863  prmdvdsncoprmbd  16883  pcadd  17047  vdwlem2  17140  vdwlem11  17149  sbcie3s  17320  prdsval  17606  mreexexlem4d  17801  isacs2  17807  catcocl  17839  catass  17840  subccocl  18000  fullsubc  18005  funcco  18026  funcpropd  18057  fullpropd  18077  ffthiso  18086  isnat  18105  natpropd  18134  fucpropd  18135  xpcval  18331  evlf2  18372  curfpropd  18387  curfuncf  18392  uncfcurf  18393  curf2ndf  18401  hofcl  18413  hofpropd  18421  yonffthlem  18436  isacs3lem  18696  acsfiindd  18707  chnind  18775  gsumpropd2lem  18848  resmgmhm2b  18882  resmhm2b  18998  mhmid  19253  mhmmnd  19254  ghmgrp  19256  conjnmzb  19447  ghmqusnsg  19476  ghmquskerlem3  19480  ghmqusker  19481  pgpfi  19799  sylow3lem2  19822  efgredlem  19941  frgpnabllem1  20067  imasabl  20070  dprdfcntz  20211  ablfac1b  20266  pgpfac1lem3  20273  pgpfac1lem5  20275  pgpfaclem3  20279  omndmul2  20327  gsumle  20339  ringinvnzdiv  20512  rnghmsubcsetclem2  20864  rhmsubcsetclem2  20893  srhmsubc  20912  rhmsubclem4  20920  imadrhmcl  21034  cntzsdrg  21039  suborng  21113  islmhm2  21293  lspsneleq  21373  drngidl  21519  rhmpreimaidl  21551  qsidomlem1  21616  prmidlsubm  21623  znunit  21849  psgndiflemB  21886  uvcff  22077  uvcf1  22078  lindfmm  22113  lindsenlbs  22137  sraassab  22156  psrval  22203  psrass1  22251  resspsrmul  22263  mplbas2  22331  evlsvvval  22382  mhpmulcl  22450  psdmul  22467  coe1tmmul  22576  gsummoncoe1  22606  evls1fpws  22667  dmatsubcl  22793  scmatscm  22808  smatvscl  22819  marrepval  22857  mdetdiaglem  22893  mdetunilem8  22914  mdetunilem9  22915  matunitlindflem1  22974  matunitlindflem2  22975  pmatcoe1fsupp  22999  decpmatmulsumfsupp  23071  pmatcollpw2lem  23075  mp2pm2mplem4  23107  pm2mpmhmlem1  23116  pm2mpmhmlem2  23117  pm2mp  23123  fvmptnn04if  23147  cpmadugsumfi  23175  cpmidg2sum  23178  cpmadumatpoly  23181  cayhamlem4  23186  neiptoptop  23429  neitr  23478  ordtrest2lem  23501  cnpnei  23562  iscncl  23567  cncls  23572  cnntr  23573  cncnp  23578  lmcnp  23602  isreg2  23675  hauscmplem  23704  cmpfi  23706  1stcfb  23743  1stcrest  23751  2ndcctbss  23754  2ndcomap  23757  islly2  23783  cldllycmp  23794  lly1stc  23795  locfincmp  23825  llycmpkgen2  23849  1stckgenlem  23852  kgencn2  23856  kgencn3  23857  ptbasfi  23880  ptpjopn  23911  txdis1cn  23934  txlly  23935  txnlly  23936  txtube  23939  txcmplem2  23941  tx1stc  23949  txkgen  23951  xkopt  23954  xkoco2cn  23957  xkococnlem  23958  xkococn  23959  xkoinjcn  23986  tgqtop  24011  regr1lem  24038  kqreglem1  24040  nrmhmph  24093  rnelfmlem  24251  rnelfm  24252  fmfnfmlem4  24256  fmfnfm  24257  ufldom  24261  flimopn  24274  hauspwpwf1  24286  fclsopn  24313  fclsnei  24318  fclsrest  24323  alexsublem  24343  alexsubALTlem3  24348  ptcmplem2  24352  ptcmplem3  24353  cnextfun  24363  cnextcn  24366  symgtgp  24405  tgpt0  24418  qustgpopn  24419  tsmsxplem1  24452  trust  24528  utopsnneiplem  24546  utop3cls  24550  utopreg  24551  isucn2  24577  cstucnd  24582  ucncn  24583  fmucnd  24590  cfilufg  24591  neipcfilu  24594  met2ndci  24821  prdsxmslem2  24828  metcnp3  24839  metustid  24853  metustexhalf  24855  metust  24857  psmetutop  24866  nmoleub  25030  reconnlem2  25127  xrge0tsms  25134  cncfco  25208  lebnumlem3  25264  lebnum  25265  nmoleub2lem2  25417  nmoleub3  25420  iscfil2  25567  iscau4  25580  iscmet3lem2  25593  equivcfil  25600  equivcau  25601  caubl  25609  rrxdstprj1  25710  ovolshftlem2  25811  ovolicc2lem4  25821  uniioombl  25890  i1fmulclem  26003  mbfi1fseqlem6  26021  itg2const2  26042  itg2split  26050  bddiblnc  26142  ellimc2  26177  ellimc3  26179  limcflf  26181  dvmptfsum  26275  dvferm1  26285  dvferm2  26287  dvlip2  26295  c1lip1  26297  lhop1  26314  ftc1a  26337  ply1divex  26435  plyeq0lem  26509  plymullem1  26513  coemullem  26549  coemulc  26554  ulmshftlem  26698  ulmcaulem  26703  ulmbdd  26707  ulmcn  26708  ulmdvlem3  26711  mtestbdd  26714  pserulm  26731  pserdvlem2  26737  abelthlem8  26748  xrlimcnp  27278  jensen  27298  lgamucov  27347  logfac2  27526  dchrelbas3  27547  dchrpt  27576  gausslemma2dlem1a  27674  lgsquad3  27696  2sqb  27741  rpvmasumlem  27796  dchrisumlem1  27798  dchrisumlem3  27800  dchrmusum2  27803  dchrvmasumlem2  27807  dchrisum0flblem1  27817  dchrisum0lem1b  27824  dchrisum0lem1  27825  dchrisum0  27829  mulog2sumlem2  27844  pntlem3  27918  ostth3  27947  fltoprmgt3  27978  lesrec  28167  cofcutr  28292  remulscllem2  28869  istrkgcb  28900  tgbtwndiff  28951  iscgrglt  28959  tgcgrxfr  28963  motcgrg  28989  lnext  29012  tgbtwnconn1  29020  tgbtwnconn3  29022  legval  29029  legtrid  29036  legso  29044  hlcgreu  29066  tglnne  29078  tglineeltr  29081  tglnne0  29091  colline  29100  tglowdim2l  29101  tglowdim2ln  29102  mirreu3  29108  mirbtwnhl  29134  krippenlem  29144  midexlem  29146  perpcom  29170  perpneq  29171  footexALT  29175  footex  29178  colperpexlem3  29190  colperpex  29191  opphllem  29193  midex  29195  oppne3  29201  opptgdim2  29203  oppnid  29204  opphllem2  29206  opphllem5  29209  opphllem6  29210  oppperpex  29211  outpasch  29215  hlpasch  29216  lnopp2hpgb  29223  hpgerlem  29225  colopp  29229  colhp  29230  plngrnssp  29239  lnincplng  29244  plngrotlem1  29247  plngrotlem2  29248  plngrotlem3  29249  lnssplnglem  29251  lmieu  29271  lnperpex  29291  trgcopy  29293  trgcopyeulem  29294  iscgra1  29299  cgrane1  29301  cgrane2  29302  cgrane3  29303  cgrane4  29304  cgrahl1  29305  cgrahl2  29306  cgracgr  29307  cgraswap  29309  cgracom  29311  cgratr  29312  zerocgra  29313  flatcgra  29314  cgrabtwn  29316  cgrahl  29317  sacgr  29321  acopyeu  29324  ragcgra  29325  tgaaddcpbllem1  29331  tgaaddcpbllem3  29333  tgaaddcpbl  29334  cgrg3col4  29354  angmgmaddeu1  29361  angmgmaddeu2  29362  angmgmaddeu3  29363  angmgmaddeu4  29364  angmgmaddeu5  29365  angmgmaddeu6  29366  angmgmaddeu7  29367  angmgmaddov2lem  29369  angmgmaddcpbl  29372  angmgmaddrid  29375  angmgm  29379  tgasa1  29385  prlnghpg  29406  dfprlng2  29407  perpprlng  29410  prlngex  29411  prlngmolem1  29412  prlngmolem2  29413  prlngplngtr  29419  prlngmid2  29421  quadcgrprlng  29426  f1otrg  29430  f1otrge  29431  axeuclidlem  29522  axcontlem2  29525  umgrvad2edg  29776  usgredg2vlem2  29789  pthdepisspth  30303  clwwlkccatlem  30562  clwlkclwwlklem2  30573  3cycld  30761  eupth2lems  30821  eucrctshift  30826  frgr3vlem2  30857  n4cyclfrgr  30874  numclwwlk1lem2f1  30940  numclwwlk2lem1  30959  ubthlem3  31456  chirredlem1  32974  chirredlem3  32976  cdj1i  33017  fnpreimac  33246  xrge0infss  33334  nn0xmulclb  33345  hashxpe  33381  2exple2exp  33407  ccatws1f1o  33496  dfmgc2lem  33538  mgcf1o  33546  mndlactf1  33569  mndlactfo  33570  mndractf1  33571  mndractfo  33572  gsumfs2d  33604  gsumhashmul  33610  suppgsumssiun  33615  xrge0tsmsd  33616  gsumwun  33619  psgnfzto1stlem  33643  cycpmco2  33676  cycpmrn  33686  tocyccntz  33687  cycpmconjslem2  33698  cyc3conja  33700  conjga  33713  submarchi  33729  isarchiofld  33742  elrgspnlem1  33785  elrgspnlem2  33786  elrgspnlem3  33787  elrgspnlem4  33788  elrgspnsubrunlem1  33790  elrgspnsubrunlem2  33791  elrgspnsubrun  33792  erlval  33801  erler  33808  rloccring  33814  rlocf1  33817  rlocisunit  33819  domnprodn0  33821  domnprodeq0  33822  subrdom  33828  imaslmod  33896  znfermltl  33904  lindfpropd  33919  unitprodclb  33926  nsgmgc  33945  nsgqusf1olem1  33946  unitpidl1  33956  elrspunidl  33960  elrspunsn  33961  rhmimaidl  33964  mxidlprm  33977  mxidlirredi  33978  drngmxidlr  33984  qsdrngilem  34000  qsdrngi  34001  drnglring  34006  dflringlem2  34009  dflring3  34011  dflring4  34012  rsprprmprmidl  34036  rsprprmprmidlb  34037  rprmasso2  34040  rprmirred  34045  rprmirredb  34046  rprmdvdspow  34047  1arithidom  34051  pidufd  34057  1arithufdlem3  34060  dfufd2  34064  deg1prod  34097  ply1dg3rt0irred  34098  0mplrim  34128  mplidomlem  34141  extvfvcl  34150  mplvrpmga  34159  mplvrpmmhm  34160  mplvrpmrhm  34161  psrgsum  34162  psrmonprod  34166  esplymhp  34182  esplyfval3  34186  esplyfval1  34187  esplyfvaln  34188  esplyind  34189  exsslsb  34211  lbslelsp  34212  ply1degltdimlem  34236  lindsunlem  34238  lindsun  34239  lbsdiflsp0  34240  dimkerim  34241  fedgmul  34245  dimlssid  34246  assalactf1o  34249  extdg1id  34280  evls1fldgencl  34284  fldextrspunlsplem  34287  fldextrspunlsp  34288  extdgfialglem1  34306  minplyirred  34325  fldext2chn  34342  cos9thpiminplylem2  34397  smatrcl  34410  1smat1  34418  submateq  34423  mdetpmtr1  34437  madjusmdetlem2  34442  locfinreflem  34454  cmppcmp  34472  rhmpreimacn  34499  ordtrest2NEWlem  34536  ordtconnlem1  34538  lmdvg  34567  zrhcntr  34593  esumpcvgval  34692  esum2d  34707  sigapildsys  34777  ldgenpisyslem1  34778  fiunelros  34789  volmeas  34846  imambfm  34877  omssubadd  34915  carsggect  34933  carsgclctunlem3  34935  signsply0  35163  signstres  35187  actfunsnf1o  35216  actfunsnrndisj  35217  reprsuc  35227  reprinfz1  35234  breprexplema  35242  breprexplemc  35244  breprexp  35245  breprexpnat  35246  circlemeth  35252  hgt750lemb  35268  tgoldbachgtd  35274  erdszelem8  35932  pconnconn  35965  cvmlift2lem12  36048  cvmlift3lem5  36057  cvmlift3lem7  36059  cvmlift3lem8  36060  fmla1  36121  mrsubrn  36247  msrval  36272  msubff1  36290  btwnconn1lem13  36834  elicc3  37075  neibastop2lem  37118  weiunfr  37225  unbdqndv2  37347  irrdifflemf  38214  ltflcei  38499  poimirlem4  38510  poimirlem13  38519  poimirlem14  38520  poimirlem22  38528  poimirlem26  38532  poimirlem27  38533  heicant  38541  mblfinlem2  38544  mblfinlem3  38545  mblfinlem4  38546  cnambfre  38554  itg2addnclem  38557  itg2addnclem2  38558  itg2gt0cn  38561  ftc1cnnc  38578  ftc1anclem5  38583  ftc1anclem7  38585  ftc1anc  38587  equivtotbnd  38680  isbndx  38684  ssbnd  38690  heibor1lem  38711  rrncmslem  38734  islshpat  40042  lfl1dim  40146  lfl1dim2N  40147  lkrpssN  40188  glbconN  40402  hlhgt2  40414  3dim2  40493  3dim3  40494  islln3  40535  islvol5  40604  2lplnja  40644  dalem19  40707  isline4N  40802  2polssN  40940  lhpmatb  41056  4atex  41101  trlatn0  41197  cdlemf2  41587  dialss  42071  diaglbN  42080  diaintclN  42083  dibglbN  42191  dibintclN  42192  dihlsscpre  42259  dihglblem5aN  42317  dihglblem2aN  42318  dihglblem4  42322  dihatexv  42363  dihjat1lem  42453  lcfl6  42525  mapdval2N  42655  aks4d1p8  43105  fldhmf1  43108  primrootscoprmpow  43117  primrootscoprbij2  43121  primrootspoweq0  43124  evl1gprodd  43135  hashscontpow  43140  aks6d1c2lem4  43145  idomnnzgmulnz  43151  deg1gprod  43158  sticksstones8  43171  sticksstones12a  43175  aks6d1c6lem3  43190  aks6d1c6lem5  43195  aks6d1c7  43202  aks5lem5a  43209  unitscyglem2  43214  sn-0tie0  43483  imacrhmcl  43546  fiabv  43562  evlselv  43579  fsuppind  43580  prjspertr  43595  prjspreln0  43599  prjspner1  43616  elrfi  43658  eldioph2  43726  diophin  43736  irrapxlem2  43783  irrapxlem3  43784  irrapxlem4  43785  irrapxlem5  43786  pell1234qrne0  43813  pell1234qrreccl  43814  pell1234qrmulcl  43815  pell14qrgt0  43819  pell14qrdich  43829  pell1qrge1  43830  pellfundex  43846  congabseq  43934  jm2.27b  43966  jm2.27  43968  fnwe2lem2  44011  kelac1  44023  lnrfg  44079  hbt  44090  omabs2  44292  nadd1suc  44352  rfovcnvf1od  44963  ntrneiiso  45050  ntrneikb  45053  ntrneixb  45054  ntrneik3  45055  ntrneix3  45056  ntrneik13  45057  ntrneix13  45058  cvgdvgrat  45256  binomcxplemnotnn0  45299  sineq0ALT  45878  fnchoice  45989  disjf1  46141  supxrgere  46289  supxrgelem  46293  supxrge  46294  suplesup  46295  xralrple2  46310  infxr  46322  infleinflem2  46326  infleinf  46327  uzub  46385  mccl  46554  limcrecl  46585  lptioo2  46587  lptioo1  46588  lptre2pt  46594  addlimc  46602  limsupmnflem  46674  climxrre  46704  liminflimsupclim  46761  climxlim2lem  46799  xlimliminflimsup  46816  icccncfext  46841  cncfiooicclem1  46847  cncfiooiccre  46849  dvbdfbdioolem2  46883  ioodvbdlimc1lem1  46885  dvnxpaek  46896  dvmptfprodlem  46898  dvmptfprod  46899  dvnprodlem3  46902  itgioocnicc  46931  itgspltprt  46933  stoweidlem31  46985  fourierdlem39  47100  fourierdlem42  47103  fourierdlem48  47108  fourierdlem49  47109  fourierdlem50  47110  fourierdlem51  47111  fourierdlem64  47124  fourierdlem65  47125  fourierdlem74  47134  fourierdlem75  47135  fourierdlem81  47141  fourierdlem82  47142  fourierdlem101  47161  etransclem23  47211  etransclem27  47215  etransclem32  47220  etransclem33  47221  etransclem35  47223  etransclem38  47226  sge0tsms  47334  sge0cl  47335  sge0f1o  47336  sge0split  47363  sge0rpcpnf  47375  sge0seq  47400  nnfoctbdjlem  47409  iundjiun  47414  meaiuninc3v  47438  meaiininclem  47440  omeiunltfirp  47473  carageniuncllem2  47476  carageniuncl  47477  hoicvr  47502  hoidmv1lelem1  47545  hoidmvlelem3  47551  hoidmvlelem5  47553  hoidmvle  47554  hoiqssbllem3  47578  iunhoiioolem  47629  pimdecfgtioo  47671  pimincfltioo  47672  preimageiingt  47674  preimaleiinlt  47675  smflimlem4  47728  iccpartigtl  48449  iccpartgt  48453  sprsymrelf1lem  48517  paireqne  48537  proththd  48643  requad2  48665  sbgoldbst  48820  bgoldbtbndlem4  48850  isuspgrim0lem  48935  isuspgrim0  48936  isuspgrimlem  48937  gricushgr  48959  grimedg  48977  grimgrtri  48991  isubgr3stgrlem7  49014  gpgusgralem  49098  pgn4cyclex  49168  2zrngmmgm  49293  cznrng  49302  rhmsubcALTVlem4  49325  srhmsubcALTV  49366  lincsum  49485  lcoss  49492  snlindsntor  49527  islindeps2  49539  line2x  49810  line2y  49811  itscnhlinecirc02p  49841  discsubc  50116  imasubc3  50208  uppropd  50233  swapfval  50314  fucofvalg  50370  fuco21  50388  precofvalALT  50420  2arwcat  50652  lanup  50693  ranup  50694