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  ad5ant12  756  simplll  775  fsnex  7302  fimaproj  8158  frxp3  8174  oaabs  8684  oaabs2  8685  omabs  8687  cofon1  8708  undomOLD  9098  sbthlem8  9128  findcard3OLD  9316  cantnfle  9708  cantnfp1  9718  cantnflem1c  9724  sornom  10314  enfin2i  10358  ttukeylem6  10551  fpwwe2lem12  10679  winalim2  10733  wuncval2  10784  negf1o  11690  xlemul1a  13326  difreicc  13520  flflp1  13843  faclbnd  14325  swrdswrd  14739  pfxccatin12lem3  14766  swrdccat3blem  14773  ello12  15548  elo12  15559  rlimclim1  15577  rlimcld2  15610  o1co  15618  o1of2  15645  o1rlimmul  15651  rlimsqzlem  15681  isercoll  15700  o1fsum  15845  supcvg  15888  dvds2ln  16322  lcmgcdlem  16639  cncongr2  16701  isprm5  16740  prmdvdsncoprmbd  16760  pcadd  16922  vdwlem2  17015  vdwlem11  17024  sbcie3s  17195  prdsval  17501  mreexexlem4d  17691  isacs2  17697  catcocl  17729  catass  17730  subccocl  17895  fullsubc  17900  funcco  17921  fullpropd  17973  ffthiso  17982  isnat  18001  natpropd  18032  fucpropd  18033  xpcval  18232  evlf2  18274  curfpropd  18289  curfuncf  18294  uncfcurf  18295  hofcl  18315  hofpropd  18323  yonffthlem  18338  isacs3lem  18599  acsfiindd  18610  gsumpropd2lem  18704  resmgmhm2b  18738  resmhm2b  18847  mhmid  19093  mhmmnd  19094  ghmgrp  19096  conjnmzb  19283  ghmqusnsg  19312  ghmquskerlem3  19316  ghmqusker  19317  pgpfi  19637  sylow3lem2  19660  efgredlem  19779  frgpnabllem1  19905  imasabl  19908  dprdfcntz  20049  ablfac1b  20104  pgpfac1lem3  20111  pgpfac1lem5  20113  pgpfaclem3  20117  ringinvnzdiv  20314  rnghmsubcsetclem2  20648  rhmsubcsetclem2  20677  srhmsubc  20696  rhmsubclem4  20704  imadrhmcl  20814  cntzsdrg  20819  islmhm2  21054  lspsneleq  21134  rhmpreimaidl  21304  znunit  21599  psgndiflemB  21635  uvcff  21828  uvcf1  21829  lindfmm  21864  sraassab  21905  psrval  21952  psrass1  22001  resspsrmul  22013  mplbas2  22077  mhpmulcl  22170  psdmul  22187  coe1tmmul  22295  gsummoncoe1  22327  evls1fpws  22388  dmatsubcl  22519  scmatscm  22534  smatvscl  22545  marrepval  22583  mdetdiaglem  22619  mdetunilem8  22640  mdetunilem9  22641  pmatcoe1fsupp  22722  decpmatmulsumfsupp  22794  pmatcollpw2lem  22798  mp2pm2mplem4  22830  pm2mpmhmlem1  22839  pm2mpmhmlem2  22840  pm2mp  22846  fvmptnn04if  22870  cpmadugsumfi  22898  cpmidg2sum  22901  cpmadumatpoly  22904  cayhamlem4  22909  neiptoptop  23154  neitr  23203  ordtrest2lem  23226  cnpnei  23287  iscncl  23292  cncls  23297  cnntr  23298  cncnp  23303  lmcnp  23327  isreg2  23400  hauscmplem  23429  cmpfi  23431  1stcfb  23468  1stcrest  23476  2ndcctbss  23478  2ndcomap  23481  islly2  23507  cldllycmp  23518  lly1stc  23519  locfincmp  23549  llycmpkgen2  23573  1stckgenlem  23576  kgencn2  23580  kgencn3  23581  ptbasfi  23604  ptpjopn  23635  txdis1cn  23658  txlly  23659  txnlly  23660  txtube  23663  txcmplem2  23665  tx1stc  23673  txkgen  23675  xkopt  23678  xkoco2cn  23681  xkococnlem  23682  xkococn  23683  xkoinjcn  23710  tgqtop  23735  regr1lem  23762  kqreglem1  23764  nrmhmph  23817  rnelfmlem  23975  rnelfm  23976  fmfnfmlem4  23980  fmfnfm  23981  ufldom  23985  flimopn  23998  hauspwpwf1  24010  fclsopn  24037  fclsnei  24042  fclsrest  24047  alexsublem  24067  alexsubALTlem3  24072  ptcmplem2  24076  ptcmplem3  24077  cnextfun  24087  cnextcn  24090  symgtgp  24129  tgpt0  24142  qustgpopn  24143  tsmsxplem1  24176  trust  24253  utopsnneiplem  24271  utop3cls  24275  utopreg  24276  isucn2  24303  cstucnd  24308  ucncn  24309  fmucnd  24316  cfilufg  24317  neipcfilu  24320  met2ndci  24550  prdsxmslem2  24557  metustid  24582  metustexhalf  24584  metust  24586  psmetutop  24595  nmoleub  24767  reconnlem2  24862  xrge0tsms  24869  cncfco  24946  lebnumlem3  25008  lebnum  25009  nmoleub2lem2  25162  nmoleub3  25165  iscfil2  25313  iscau4  25326  iscmet3lem2  25339  equivcfil  25346  equivcau  25347  caubl  25355  rrxdstprj1  25456  ovolshftlem2  25558  ovolicc2lem4  25568  uniioombl  25637  i1fmulclem  25751  mbfi1fseqlem6  25769  itg2const2  25790  itg2split  25798  bddiblnc  25891  ellimc2  25926  ellimc3  25928  limcflf  25930  dvmptfsum  26027  dvferm1  26037  dvferm2  26039  dvlip2  26048  c1lip1  26050  lhop1  26067  ftc1a  26092  ply1divex  26190  plyeq0lem  26263  plymullem1  26267  coemullem  26303  coemulc  26308  ulmshftlem  26446  ulmcaulem  26451  ulmbdd  26455  ulmcn  26456  ulmdvlem3  26459  mtestbdd  26462  pserulm  26479  pserdvlem2  26486  abelthlem8  26497  xrlimcnp  27025  jensen  27046  lgamucov  27095  logfac2  27275  dchrelbas3  27296  dchrpt  27325  gausslemma2dlem1a  27423  lgsquad3  27445  2sqb  27490  rpvmasumlem  27545  dchrisumlem1  27547  dchrisumlem3  27549  dchrmusum2  27552  dchrvmasumlem2  27556  dchrisum0flblem1  27566  dchrisum0lem1b  27573  dchrisum0lem1  27574  dchrisum0  27578  mulog2sumlem2  27593  pntlem3  27667  ostth3  27696  slerec  27878  cofcutr  27972  remulscllem2  28447  istrkgcb  28478  tgbtwndiff  28528  iscgrglt  28536  tgcgrxfr  28540  motcgrg  28566  lnext  28589  tgbtwnconn1  28597  tgbtwnconn3  28599  legval  28606  legtrid  28613  legso  28621  hlcgreu  28640  tglnne  28650  tglineeltr  28653  tglnne0  28662  colline  28671  tglowdim2l  28672  tglowdim2ln  28673  mirreu3  28676  mirbtwnhl  28702  krippenlem  28712  midexlem  28714  perpcom  28735  footexALT  28740  footex  28743  colperpexlem3  28754  colperpex  28755  opphllem  28757  midex  28759  oppne3  28765  opptgdim2  28767  oppnid  28768  opphllem2  28770  opphllem5  28773  opphllem6  28774  oppperpex  28775  outpasch  28777  hlpasch  28778  lnopp2hpgb  28785  hpgerlem  28787  colopp  28791  colhp  28792  lmieu  28806  lnperpex  28825  trgcopy  28826  trgcopyeulem  28827  iscgra1  28832  cgrane1  28834  cgrane2  28835  cgrane3  28836  cgrane4  28837  cgrahl1  28838  cgrahl2  28839  cgracgr  28840  cgraswap  28842  cgracom  28844  cgratr  28845  flatcgra  28846  cgrabtwn  28848  cgrahl  28849  sacgr  28853  acopyeu  28856  cgrg3col4  28875  tgasa1  28880  f1otrg  28893  f1otrge  28894  axeuclidlem  28991  axcontlem2  28994  umgrvad2edg  29244  usgredg2vlem2  29257  pthdepisspth  29767  clwwlkccatlem  30017  clwlkclwwlklem2  30028  3cycld  30206  eupth2lems  30266  eucrctshift  30271  frgr3vlem2  30302  n4cyclfrgr  30319  numclwwlk1lem2f1  30385  numclwwlk2lem1  30404  ubthlem3  30900  chirredlem1  32418  chirredlem3  32420  cdj1i  32461  fnpreimac  32687  xrge0infss  32770  nn0xmulclb  32781  hashxpe  32816  ccatf1  32917  ccatws1f1o  32920  swrdf1  32925  dfmgc2lem  32969  mgcf1o  32977  chnind  32984  mndlactf1  33013  mndlactfo  33014  mndractf1  33015  mndractfo  33016  gsumfs2d  33040  gsumhashmul  33046  xrge0tsmsd  33047  gsumwun  33050  omndmul2  33071  gsumle  33083  psgnfzto1stlem  33102  cycpmco2  33135  cycpmrn  33145  tocyccntz  33146  cycpmconjslem2  33157  cyc3conja  33159  submarchi  33175  elrgspnlem1  33231  elrgspnlem2  33232  elrgspnlem3  33233  elrgspnlem4  33234  erlval  33244  erler  33251  rlocf1  33259  domnprodn0  33261  subrdom  33268  suborng  33324  isarchiofld  33326  imaslmod  33360  znfermltl  33373  lindfpropd  33389  unitprodclb  33396  nsgqusf1olem1  33420  unitpidl1  33431  elrspunidl  33435  elrspunsn  33436  rhmimaidl  33439  drngidl  33440  qsidomlem1  33459  mxidlprm  33477  mxidlirredi  33478  qsdrngilem  33501  qsdrngi  33502  rsprprmprmidl  33529  rsprprmprmidlb  33530  rprmasso2  33533  rprmirred  33538  rprmirredb  33539  rprmdvdspow  33540  1arithidom  33544  pidufd  33550  1arithufdlem3  33553  dfufd2  33557  ply1dg3rt0irred  33586  ply1degltdimlem  33649  lindsunlem  33651  lindsun  33652  lbsdiflsp0  33653  dimkerim  33654  fedgmul  33658  dimlssid  33659  assalactf1o  33662  extdg1id  33690  evls1fldgencl  33694  minplyirred  33718  fldext2chn  33733  smatrcl  33756  1smat1  33764  submateq  33769  mdetpmtr1  33783  madjusmdetlem2  33788  locfinreflem  33800  cmppcmp  33818  rhmpreimacn  33845  ordtrest2NEWlem  33882  ordtconnlem1  33884  lmdvg  33913  zrhcntr  33941  esumpcvgval  34058  esum2d  34073  sigapildsys  34142  ldgenpisyslem1  34143  fiunelros  34154  volmeas  34211  imambfm  34243  omssubadd  34281  carsggect  34299  carsgclctunlem3  34301  sgnmul  34523  signsply0  34544  signstres  34568  actfunsnf1o  34597  actfunsnrndisj  34598  reprsuc  34608  reprinfz1  34615  breprexplema  34623  breprexplemc  34625  breprexp  34626  breprexpnat  34627  circlemeth  34633  hgt750lemb  34649  tgoldbachgtd  34655  erdszelem8  35182  pconnconn  35215  cvmlift2lem12  35298  cvmlift3lem5  35307  cvmlift3lem7  35309  cvmlift3lem8  35310  mrsubrn  35497  msrval  35522  msubff1  35540  btwnconn1lem13  36080  elicc3  36299  neibastop2lem  36342  weiunfr  36449  unbdqndv2  36493  irrdifflemf  37307  ltflcei  37594  lindsenlbs  37601  matunitlindflem1  37602  matunitlindflem2  37603  poimirlem4  37610  poimirlem13  37619  poimirlem14  37620  poimirlem22  37628  poimirlem26  37632  poimirlem27  37633  heicant  37641  mblfinlem2  37644  mblfinlem3  37645  mblfinlem4  37646  cnambfre  37654  itg2addnclem  37657  itg2addnclem2  37658  itg2gt0cn  37661  ftc1cnnc  37678  ftc1anclem5  37683  ftc1anclem7  37685  ftc1anc  37687  equivtotbnd  37764  isbndx  37768  ssbnd  37774  heibor1lem  37795  rrncmslem  37818  islshpat  38998  lfl1dim  39102  lfl1dim2N  39103  lkrpssN  39144  glbconN  39358  glbconNOLD  39359  hlhgt2  39371  3dim2  39450  3dim3  39451  islln3  39492  islvol5  39561  2lplnja  39601  dalem19  39664  isline4N  39759  2polssN  39897  lhpmatb  40013  4atex  40058  trlatn0  40154  cdlemf2  40544  dialss  41028  diaglbN  41037  diaintclN  41040  dibglbN  41148  dibintclN  41149  dihlsscpre  41216  dihglblem5aN  41274  dihglblem2aN  41275  dihglblem4  41279  dihatexv  41320  dihjat1lem  41410  lcfl6  41482  mapdval2N  41612  aks4d1p8  42068  fldhmf1  42071  primrootscoprmpow  42080  primrootscoprbij2  42084  primrootspoweq0  42087  evl1gprodd  42098  hashscontpow  42103  aks6d1c2lem4  42108  idomnnzgmulnz  42114  deg1gprod  42121  sticksstones8  42134  sticksstones12a  42138  aks6d1c6lem3  42153  aks6d1c6lem5  42158  aks6d1c7  42165  aks5lem5a  42172  unitscyglem2  42177  sn-0tie0  42445  imacrhmcl  42500  fiabv  42522  evlsvvval  42549  evlselv  42573  fsuppind  42576  prjspertr  42591  prjspreln0  42595  prjspner1  42612  elrfi  42681  eldioph2  42749  diophin  42759  irrapxlem2  42810  irrapxlem3  42811  irrapxlem4  42812  irrapxlem5  42813  pell1234qrne0  42840  pell1234qrreccl  42841  pell1234qrmulcl  42842  pell14qrgt0  42846  pell14qrdich  42856  pell1qrge1  42857  pellfundex  42873  congabseq  42962  jm2.27b  42994  jm2.27  42996  fnwe2lem2  43039  kelac1  43051  lnrfg  43107  hbt  43118  nadd1suc  43381  rfovcnvf1od  43993  ntrneiiso  44080  ntrneikb  44083  ntrneixb  44084  ntrneik3  44085  ntrneix3  44086  ntrneik13  44087  ntrneix13  44088  cvgdvgrat  44308  binomcxplemnotnn0  44351  sineq0ALT  44934  disjf1  45125  supxrgere  45282  supxrgelem  45286  supxrge  45287  suplesup  45288  xralrple2  45303  infxr  45316  infleinflem2  45320  infleinf  45321  uzub  45380  mccl  45553  limcrecl  45584  lptioo2  45586  lptioo1  45587  lptre2pt  45595  addlimc  45603  limsupmnflem  45675  climxrre  45705  liminflimsupclim  45762  climxlim2lem  45800  xlimliminflimsup  45817  icccncfext  45842  cncfiooicclem1  45848  cncfiooiccre  45850  dvbdfbdioolem2  45884  ioodvbdlimc1lem1  45886  dvnxpaek  45897  dvmptfprodlem  45899  dvmptfprod  45900  dvnprodlem3  45903  itgioocnicc  45932  itgspltprt  45934  stoweidlem31  45986  fourierdlem39  46101  fourierdlem42  46104  fourierdlem48  46109  fourierdlem49  46110  fourierdlem50  46111  fourierdlem51  46112  fourierdlem64  46125  fourierdlem65  46126  fourierdlem74  46135  fourierdlem75  46136  fourierdlem81  46142  fourierdlem82  46143  fourierdlem101  46162  etransclem23  46212  etransclem27  46216  etransclem32  46221  etransclem33  46222  etransclem35  46224  etransclem38  46227  sge0tsms  46335  sge0cl  46336  sge0f1o  46337  sge0split  46364  sge0rpcpnf  46376  sge0seq  46401  nnfoctbdjlem  46410  iundjiun  46415  meaiuninc3v  46439  meaiininclem  46441  omeiunltfirp  46474  carageniuncllem2  46477  carageniuncl  46478  hoidmv1lelem1  46546  hoidmvlelem3  46552  hoidmvlelem5  46554  hoidmvle  46555  hoiqssbllem3  46579  iunhoiioolem  46630  pimdecfgtioo  46672  pimincfltioo  46673  preimageiingt  46675  preimaleiinlt  46676  smflimlem4  46729  iccpartigtl  47347  iccpartgt  47351  sprsymrelf1lem  47415  paireqne  47435  proththd  47538  requad2  47547  sbgoldbst  47702  bgoldbtbndlem4  47732  isuspgrim0lem  47808  isuspgrim0  47809  gricushgr  47823  grimedg  47840  grimgrtri  47851  isubgr3stgrlem7  47874  gpgusgralem  47945  2zrngmmgm  48095  cznrng  48104  rhmsubcALTVlem4  48127  srhmsubcALTV  48168  lincsum  48274  lcoss  48281  snlindsntor  48316  islindeps2  48328  line2x  48603  line2y  48604  itscnhlinecirc02p  48634