Theorem ad3antrrr 729

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 725	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  731  ad4antlr  732  ad5ant12  755  simplll  774  fsnex  7319  fimaproj  8176  frxp3  8192  oaabs  8704  oaabs2  8705  omabs  8707  cofon1  8728  undomOLD  9126  sbthlem8  9156  findcard3OLD  9347  cantnfle  9740  cantnfp1  9750  cantnflem1c  9756  sornom  10346  enfin2i  10390  ttukeylem6  10583  fpwwe2lem12  10711  winalim2  10765  wuncval2  10816  negf1o  11720  xlemul1a  13350  difreicc  13544  flflp1  13858  faclbnd  14339  swrdswrd  14753  pfxccatin12lem3  14780  swrdccat3blem  14787  ello12  15562  elo12  15573  rlimclim1  15591  rlimcld2  15624  o1co  15632  o1of2  15659  o1rlimmul  15665  rlimsqzlem  15697  isercoll  15716  o1fsum  15861  supcvg  15904  dvds2ln  16337  lcmgcdlem  16653  cncongr2  16715  isprm5  16754  prmdvdsncoprmbd  16774  pcadd  16936  vdwlem2  17029  vdwlem11  17038  sbcie3s  17209  prdsval  17515  mreexexlem4d  17705  isacs2  17711  catcocl  17743  catass  17744  subccocl  17909  fullsubc  17914  funcco  17935  fullpropd  17987  ffthiso  17996  isnat  18015  natpropd  18046  fucpropd  18047  xpcval  18246  evlf2  18288  curfpropd  18303  curfuncf  18308  uncfcurf  18309  hofcl  18329  hofpropd  18337  yonffthlem  18352  isacs3lem  18612  acsfiindd  18623  gsumpropd2lem  18717  resmgmhm2b  18751  resmhm2b  18857  mhmid  19103  mhmmnd  19104  ghmgrp  19106  conjnmzb  19293  ghmqusnsg  19322  ghmquskerlem3  19326  ghmqusker  19327  pgpfi  19647  sylow3lem2  19670  efgredlem  19789  frgpnabllem1  19915  imasabl  19918  dprdfcntz  20059  ablfac1b  20114  pgpfac1lem3  20121  pgpfac1lem5  20123  pgpfaclem3  20127  ringinvnzdiv  20324  rnghmsubcsetclem2  20654  rhmsubcsetclem2  20683  srhmsubc  20702  rhmsubclem4  20710  imadrhmcl  20820  cntzsdrg  20825  islmhm2  21060  lspsneleq  21140  rhmpreimaidl  21310  znunit  21605  psgndiflemB  21641  uvcff  21834  uvcf1  21835  lindfmm  21870  sraassab  21911  psrval  21958  psrass1  22007  resspsrmul  22019  mplbas2  22083  mhpmulcl  22176  psdmul  22193  coe1tmmul  22301  gsummoncoe1  22333  evls1fpws  22394  dmatsubcl  22525  scmatscm  22540  smatvscl  22551  marrepval  22589  mdetdiaglem  22625  mdetunilem8  22646  mdetunilem9  22647  pmatcoe1fsupp  22728  decpmatmulsumfsupp  22800  pmatcollpw2lem  22804  mp2pm2mplem4  22836  pm2mpmhmlem1  22845  pm2mpmhmlem2  22846  pm2mp  22852  fvmptnn04if  22876  cpmadugsumfi  22904  cpmidg2sum  22907  cpmadumatpoly  22910  cayhamlem4  22915  neiptoptop  23160  neitr  23209  ordtrest2lem  23232  cnpnei  23293  iscncl  23298  cncls  23303  cnntr  23304  cncnp  23309  lmcnp  23333  isreg2  23406  hauscmplem  23435  cmpfi  23437  1stcfb  23474  1stcrest  23482  2ndcctbss  23484  2ndcomap  23487  islly2  23513  cldllycmp  23524  lly1stc  23525  locfincmp  23555  llycmpkgen2  23579  1stckgenlem  23582  kgencn2  23586  kgencn3  23587  ptbasfi  23610  ptpjopn  23641  txdis1cn  23664  txlly  23665  txnlly  23666  txtube  23669  txcmplem2  23671  tx1stc  23679  txkgen  23681  xkopt  23684  xkoco2cn  23687  xkococnlem  23688  xkococn  23689  xkoinjcn  23716  tgqtop  23741  regr1lem  23768  kqreglem1  23770  nrmhmph  23823  rnelfmlem  23981  rnelfm  23982  fmfnfmlem4  23986  fmfnfm  23987  ufldom  23991  flimopn  24004  hauspwpwf1  24016  fclsopn  24043  fclsnei  24048  fclsrest  24053  alexsublem  24073  alexsubALTlem3  24078  ptcmplem2  24082  ptcmplem3  24083  cnextfun  24093  cnextcn  24096  symgtgp  24135  tgpt0  24148  qustgpopn  24149  tsmsxplem1  24182  trust  24259  utopsnneiplem  24277  utop3cls  24281  utopreg  24282  isucn2  24309  cstucnd  24314  ucncn  24315  fmucnd  24322  cfilufg  24323  neipcfilu  24326  met2ndci  24556  prdsxmslem2  24563  metustid  24588  metustexhalf  24590  metust  24592  psmetutop  24601  nmoleub  24773  reconnlem2  24868  xrge0tsms  24875  cncfco  24952  lebnumlem3  25014  lebnum  25015  nmoleub2lem2  25168  nmoleub3  25171  iscfil2  25319  iscau4  25332  iscmet3lem2  25345  equivcfil  25352  equivcau  25353  caubl  25361  rrxdstprj1  25462  ovolshftlem2  25564  ovolicc2lem4  25574  uniioombl  25643  i1fmulclem  25757  mbfi1fseqlem6  25775  itg2const2  25796  itg2split  25804  bddiblnc  25897  ellimc2  25932  ellimc3  25934  limcflf  25936  dvmptfsum  26033  dvferm1  26043  dvferm2  26045  dvlip2  26054  c1lip1  26056  lhop1  26073  ftc1a  26098  ply1divex  26196  plyeq0lem  26269  plymullem1  26273  coemullem  26309  coemulc  26314  ulmshftlem  26450  ulmcaulem  26455  ulmbdd  26459  ulmcn  26460  ulmdvlem3  26463  mtestbdd  26466  pserulm  26483  pserdvlem2  26490  abelthlem8  26501  xrlimcnp  27029  jensen  27050  lgamucov  27099  logfac2  27279  dchrelbas3  27300  dchrpt  27329  gausslemma2dlem1a  27427  lgsquad3  27449  2sqb  27494  rpvmasumlem  27549  dchrisumlem1  27551  dchrisumlem3  27553  dchrmusum2  27556  dchrvmasumlem2  27560  dchrisum0flblem1  27570  dchrisum0lem1b  27577  dchrisum0lem1  27578  dchrisum0  27582  mulog2sumlem2  27597  pntlem3  27671  ostth3  27700  slerec  27882  cofcutr  27976  remulscllem2  28451  istrkgcb  28482  tgbtwndiff  28532  iscgrglt  28540  tgcgrxfr  28544  motcgrg  28570  lnext  28593  tgbtwnconn1  28601  tgbtwnconn3  28603  legval  28610  legtrid  28617  legso  28625  hlcgreu  28644  tglnne  28654  tglineeltr  28657  tglnne0  28666  colline  28675  tglowdim2l  28676  tglowdim2ln  28677  mirreu3  28680  mirbtwnhl  28706  krippenlem  28716  midexlem  28718  perpcom  28739  footexALT  28744  footex  28747  colperpexlem3  28758  colperpex  28759  opphllem  28761  midex  28763  oppne3  28769  opptgdim2  28771  oppnid  28772  opphllem2  28774  opphllem5  28777  opphllem6  28778  oppperpex  28779  outpasch  28781  hlpasch  28782  lnopp2hpgb  28789  hpgerlem  28791  colopp  28795  colhp  28796  lmieu  28810  lnperpex  28829  trgcopy  28830  trgcopyeulem  28831  iscgra1  28836  cgrane1  28838  cgrane2  28839  cgrane3  28840  cgrane4  28841  cgrahl1  28842  cgrahl2  28843  cgracgr  28844  cgraswap  28846  cgracom  28848  cgratr  28849  flatcgra  28850  cgrabtwn  28852  cgrahl  28853  sacgr  28857  acopyeu  28860  cgrg3col4  28879  tgasa1  28884  f1otrg  28897  f1otrge  28898  axeuclidlem  28995  axcontlem2  28998  umgrvad2edg  29248  usgredg2vlem2  29261  pthdepisspth  29771  clwwlkccatlem  30021  clwlkclwwlklem2  30032  3cycld  30210  eupth2lems  30270  eucrctshift  30275  frgr3vlem2  30306  n4cyclfrgr  30323  numclwwlk1lem2f1  30389  numclwwlk2lem1  30408  ubthlem3  30904  chirredlem1  32422  chirredlem3  32424  cdj1i  32465  fnpreimac  32689  xrge0infss  32767  nn0xmulclb  32778  hashxpe  32814  ccatf1  32915  ccatws1f1o  32918  swrdf1  32923  dfmgc2lem  32968  mgcf1o  32976  chnind  32983  mndlactf1  33012  mndlactfo  33013  mndractf1  33014  mndractfo  33015  gsumhashmul  33040  xrge0tsmsd  33041  omndmul2  33062  gsumle  33074  psgnfzto1stlem  33093  cycpmco2  33126  cycpmrn  33136  tocyccntz  33137  cycpmconjslem2  33148  cyc3conja  33150  submarchi  33166  erlval  33230  erler  33237  rlocf1  33245  domnprodn0  33247  subrdom  33254  suborng  33310  isarchiofld  33312  imaslmod  33346  znfermltl  33359  lindfpropd  33375  unitprodclb  33382  nsgqusf1olem1  33406  unitpidl1  33417  elrspunidl  33421  elrspunsn  33422  rhmimaidl  33425  drngidl  33426  qsidomlem1  33445  mxidlprm  33463  mxidlirredi  33464  qsdrngilem  33487  qsdrngi  33488  rsprprmprmidl  33515  rsprprmprmidlb  33516  rprmasso2  33519  rprmirred  33524  rprmirredb  33525  rprmdvdspow  33526  1arithidom  33530  pidufd  33536  1arithufdlem3  33539  dfufd2  33543  ply1dg3rt0irred  33572  ply1degltdimlem  33635  lindsunlem  33637  lindsun  33638  lbsdiflsp0  33639  dimkerim  33640  fedgmul  33644  dimlssid  33645  assalactf1o  33648  extdg1id  33676  evls1fldgencl  33680  minplyirred  33704  fldext2chn  33719  smatrcl  33742  1smat1  33750  submateq  33755  mdetpmtr1  33769  madjusmdetlem2  33774  locfinreflem  33786  cmppcmp  33804  rhmpreimacn  33831  ordtrest2NEWlem  33868  ordtconnlem1  33870  lmdvg  33899  esumpcvgval  34042  esum2d  34057  sigapildsys  34126  ldgenpisyslem1  34127  fiunelros  34138  volmeas  34195  imambfm  34227  omssubadd  34265  carsggect  34283  carsgclctunlem3  34285  sgnmul  34507  signsply0  34528  signstres  34552  actfunsnf1o  34581  actfunsnrndisj  34582  reprsuc  34592  reprinfz1  34599  breprexplema  34607  breprexplemc  34609  breprexp  34610  breprexpnat  34611  circlemeth  34617  hgt750lemb  34633  tgoldbachgtd  34639  erdszelem8  35166  pconnconn  35199  cvmlift2lem12  35282  cvmlift3lem5  35291  cvmlift3lem7  35293  cvmlift3lem8  35294  mrsubrn  35481  msrval  35506  msubff1  35524  btwnconn1lem13  36063  elicc3  36283  neibastop2lem  36326  weiunfr  36433  unbdqndv2  36477  irrdifflemf  37291  ltflcei  37568  lindsenlbs  37575  matunitlindflem1  37576  matunitlindflem2  37577  poimirlem4  37584  poimirlem13  37593  poimirlem14  37594  poimirlem22  37602  poimirlem26  37606  poimirlem27  37607  heicant  37615  mblfinlem2  37618  mblfinlem3  37619  mblfinlem4  37620  cnambfre  37628  itg2addnclem  37631  itg2addnclem2  37632  itg2gt0cn  37635  ftc1cnnc  37652  ftc1anclem5  37657  ftc1anclem7  37659  ftc1anc  37661  equivtotbnd  37738  isbndx  37742  ssbnd  37748  heibor1lem  37769  rrncmslem  37792  islshpat  38973  lfl1dim  39077  lfl1dim2N  39078  lkrpssN  39119  glbconN  39333  glbconNOLD  39334  hlhgt2  39346  3dim2  39425  3dim3  39426  islln3  39467  islvol5  39536  2lplnja  39576  dalem19  39639  isline4N  39734  2polssN  39872  lhpmatb  39988  4atex  40033  trlatn0  40129  cdlemf2  40519  dialss  41003  diaglbN  41012  diaintclN  41015  dibglbN  41123  dibintclN  41124  dihlsscpre  41191  dihglblem5aN  41249  dihglblem2aN  41250  dihglblem4  41254  dihatexv  41295  dihjat1lem  41385  lcfl6  41457  mapdval2N  41587  aks4d1p8  42044  fldhmf1  42047  primrootscoprmpow  42056  primrootscoprbij2  42060  primrootspoweq0  42063  evl1gprodd  42074  hashscontpow  42079  aks6d1c2lem4  42084  idomnnzgmulnz  42090  deg1gprod  42097  sticksstones8  42110  sticksstones12a  42114  aks6d1c6lem3  42129  aks6d1c6lem5  42134  aks6d1c7  42141  aks5lem5a  42148  unitscyglem2  42153  sn-0tie0  42415  imacrhmcl  42469  fiabv  42491  evlsvvval  42518  evlselv  42542  fsuppind  42545  prjspertr  42560  prjspreln0  42564  prjspner1  42581  elrfi  42650  eldioph2  42718  diophin  42728  irrapxlem2  42779  irrapxlem3  42780  irrapxlem4  42781  irrapxlem5  42782  pell1234qrne0  42809  pell1234qrreccl  42810  pell1234qrmulcl  42811  pell14qrgt0  42815  pell14qrdich  42825  pell1qrge1  42826  pellfundex  42842  congabseq  42931  jm2.27b  42963  jm2.27  42965  fnwe2lem2  43008  kelac1  43020  lnrfg  43076  hbt  43087  nadd1suc  43354  rfovcnvf1od  43966  ntrneiiso  44053  ntrneikb  44056  ntrneixb  44057  ntrneik3  44058  ntrneix3  44059  ntrneik13  44060  ntrneix13  44061  cvgdvgrat  44282  binomcxplemnotnn0  44325  sineq0ALT  44908  disjf1  45090  supxrgere  45248  supxrgelem  45252  supxrge  45253  suplesup  45254  xralrple2  45269  infxr  45282  infleinflem2  45286  infleinf  45287  uzub  45346  mccl  45519  limcrecl  45550  lptioo2  45552  lptioo1  45553  lptre2pt  45561  addlimc  45569  limsupmnflem  45641  climxrre  45671  liminflimsupclim  45728  climxlim2lem  45766  xlimliminflimsup  45783  icccncfext  45808  cncfiooicclem1  45814  cncfiooiccre  45816  dvbdfbdioolem2  45850  ioodvbdlimc1lem1  45852  dvnxpaek  45863  dvmptfprodlem  45865  dvmptfprod  45866  dvnprodlem3  45869  itgioocnicc  45898  itgspltprt  45900  stoweidlem31  45952  fourierdlem39  46067  fourierdlem42  46070  fourierdlem48  46075  fourierdlem49  46076  fourierdlem50  46077  fourierdlem51  46078  fourierdlem64  46091  fourierdlem65  46092  fourierdlem74  46101  fourierdlem75  46102  fourierdlem81  46108  fourierdlem82  46109  fourierdlem101  46128  etransclem23  46178  etransclem27  46182  etransclem32  46187  etransclem33  46188  etransclem35  46190  etransclem38  46193  sge0tsms  46301  sge0cl  46302  sge0f1o  46303  sge0split  46330  sge0rpcpnf  46342  sge0seq  46367  nnfoctbdjlem  46376  iundjiun  46381  meaiuninc3v  46405  meaiininclem  46407  omeiunltfirp  46440  carageniuncllem2  46443  carageniuncl  46444  hoidmv1lelem1  46512  hoidmvlelem3  46518  hoidmvlelem5  46520  hoidmvle  46521  hoiqssbllem3  46545  iunhoiioolem  46596  pimdecfgtioo  46638  pimincfltioo  46639  preimageiingt  46641  preimaleiinlt  46642  smflimlem4  46695  iccpartigtl  47297  iccpartgt  47301  sprsymrelf1lem  47365  paireqne  47385  proththd  47488  requad2  47497  sbgoldbst  47652  bgoldbtbndlem4  47682  isuspgrim0lem  47755  isuspgrim0  47756  gricushgr  47770  grimedg  47787  grimgrtri  47798  2zrngmmgm  47975  cznrng  47984  rhmsubcALTVlem4  48007  srhmsubcALTV  48048  lincsum  48158  lcoss  48165  snlindsntor  48200  islindeps2  48212  line2x  48488  line2y  48489  itscnhlinecirc02p  48519