Theorem ad3antrrr 736

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  ad4antr  738  ad4antlr  739  simplll  780  fsnex  7234  fimaproj  8082  frxp3  8098  oaabs  8581  oaabs2  8582  omabs  8584  cofon1  8605  sbthlem8  9029  cantnfle  9590  cantnfp1  9600  cantnflem1c  9606  sornom  10197  enfin2i  10241  ttukeylem6  10434  fpwwe2lem12  10563  fpwwe2  10564  winalim2  10617  wuncval2  10668  negf1o  11578  xlemul1a  13238  difreicc  13435  flflp1  13764  faclbnd  14250  swrdswrd  14665  swrdccatin1  14685  pfxccatin12lem3  14692  swrdccat3blem  14699  ello12  15476  lo1bdd2  15484  elo12  15487  rlimclim1  15505  rlimcld2  15538  o1co  15546  o1of2  15573  o1rlimmul  15579  rlimsqzlem  15609  isercoll  15628  o1fsum  15774  supcvg  15819  dvds2ln  16256  lcmgcdlem  16573  cncongr2  16635  isprm5  16675  prmdvdsncoprmbd  16695  pcadd  16858  vdwlem2  16951  vdwlem11  16960  sbcie3s  17130  prdsval  17416  mreexexlem4d  17611  isacs2  17617  catcocl  17649  catass  17650  subccocl  17810  fullsubc  17815  funcco  17836  funcpropd  17867  fullpropd  17887  ffthiso  17896  isnat  17915  natpropd  17944  fucpropd  17945  xpcval  18141  evlf2  18182  curfpropd  18197  curfuncf  18202  uncfcurf  18203  curf2ndf  18211  hofcl  18223  hofpropd  18231  yonffthlem  18246  isacs3lem  18506  acsfiindd  18517  chnind  18585  gsumpropd2lem  18645  resmgmhm2b  18679  resmhm2b  18788  mhmid  19037  mhmmnd  19038  ghmgrp  19040  conjnmzb  19226  ghmqusnsg  19255  ghmquskerlem3  19259  ghmqusker  19260  pgpfi  19578  sylow3lem2  19601  efgredlem  19720  frgpnabllem1  19846  imasabl  19849  dprdfcntz  19990  ablfac1b  20045  pgpfac1lem3  20052  pgpfac1lem5  20054  pgpfaclem3  20058  omndmul2  20106  gsumle  20118  ringinvnzdiv  20280  rnghmsubcsetclem2  20611  rhmsubcsetclem2  20640  srhmsubc  20659  rhmsubclem4  20667  imadrhmcl  20776  cntzsdrg  20781  suborng  20855  islmhm2  21035  lspsneleq  21115  rhmpreimaidl  21277  znunit  21545  psgndiflemB  21582  uvcff  21773  uvcf1  21774  lindfmm  21809  sraassab  21850  psrval  21897  psrass1  21945  resspsrmul  21957  mplbas2  22025  evlsvvval  22076  mhpmulcl  22144  psdmul  22161  coe1tmmul  22270  gsummoncoe1  22301  evls1fpws  22362  dmatsubcl  22488  scmatscm  22503  smatvscl  22514  marrepval  22552  mdetdiaglem  22588  mdetunilem8  22609  mdetunilem9  22610  pmatcoe1fsupp  22691  decpmatmulsumfsupp  22763  pmatcollpw2lem  22767  mp2pm2mplem4  22799  pm2mpmhmlem1  22808  pm2mpmhmlem2  22809  pm2mp  22815  fvmptnn04if  22839  cpmadugsumfi  22867  cpmidg2sum  22870  cpmadumatpoly  22873  cayhamlem4  22878  neiptoptop  23121  neitr  23170  ordtrest2lem  23193  cnpnei  23254  iscncl  23259  cncls  23264  cnntr  23265  cncnp  23270  lmcnp  23294  isreg2  23367  hauscmplem  23396  cmpfi  23398  1stcfb  23435  1stcrest  23443  2ndcctbss  23445  2ndcomap  23448  islly2  23474  cldllycmp  23485  lly1stc  23486  locfincmp  23516  llycmpkgen2  23540  1stckgenlem  23543  kgencn2  23547  kgencn3  23548  ptbasfi  23571  ptpjopn  23602  txdis1cn  23625  txlly  23626  txnlly  23627  txtube  23630  txcmplem2  23632  tx1stc  23640  txkgen  23642  xkopt  23645  xkoco2cn  23648  xkococnlem  23649  xkococn  23650  xkoinjcn  23677  tgqtop  23702  regr1lem  23729  kqreglem1  23731  nrmhmph  23784  rnelfmlem  23942  rnelfm  23943  fmfnfmlem4  23947  fmfnfm  23948  ufldom  23952  flimopn  23965  hauspwpwf1  23977  fclsopn  24004  fclsnei  24009  fclsrest  24014  alexsublem  24034  alexsubALTlem3  24039  ptcmplem2  24043  ptcmplem3  24044  cnextfun  24054  cnextcn  24057  symgtgp  24096  tgpt0  24109  qustgpopn  24110  tsmsxplem1  24143  trust  24219  utopsnneiplem  24237  utop3cls  24241  utopreg  24242  isucn2  24268  cstucnd  24273  ucncn  24274  fmucnd  24281  cfilufg  24282  neipcfilu  24285  met2ndci  24512  prdsxmslem2  24519  metcnp3  24530  metustid  24544  metustexhalf  24546  metust  24548  psmetutop  24557  nmoleub  24721  reconnlem2  24818  xrge0tsms  24825  cncfco  24899  lebnumlem3  24955  lebnum  24956  nmoleub2lem2  25108  nmoleub3  25111  iscfil2  25258  iscau4  25271  iscmet3lem2  25284  equivcfil  25291  equivcau  25292  caubl  25300  rrxdstprj1  25401  ovolshftlem2  25502  ovolicc2lem4  25512  uniioombl  25581  i1fmulclem  25694  mbfi1fseqlem6  25712  itg2const2  25733  itg2split  25741  bddiblnc  25834  ellimc2  25869  ellimc3  25871  limcflf  25873  dvmptfsum  25967  dvferm1  25977  dvferm2  25979  dvlip2  25987  c1lip1  25989  lhop1  26006  ftc1a  26029  ply1divex  26127  plyeq0lem  26200  plymullem1  26204  coemullem  26240  coemulc  26245  ulmshftlem  26379  ulmcaulem  26384  ulmbdd  26388  ulmcn  26389  ulmdvlem3  26392  mtestbdd  26395  pserulm  26412  pserdvlem2  26418  abelthlem8  26429  xrlimcnp  26957  jensen  26977  lgamucov  27026  logfac2  27205  dchrelbas3  27226  dchrpt  27255  gausslemma2dlem1a  27353  lgsquad3  27375  2sqb  27420  rpvmasumlem  27475  dchrisumlem1  27477  dchrisumlem3  27479  dchrmusum2  27482  dchrvmasumlem2  27486  dchrisum0flblem1  27496  dchrisum0lem1b  27503  dchrisum0lem1  27504  dchrisum0  27508  mulog2sumlem2  27523  pntlem3  27597  ostth3  27626  lesrec  27816  cofcutr  27941  remulscllem2  28518  istrkgcb  28549  tgbtwndiff  28599  iscgrglt  28607  tgcgrxfr  28611  motcgrg  28637  lnext  28660  tgbtwnconn1  28668  tgbtwnconn3  28670  legval  28677  legtrid  28684  legso  28692  hlcgreu  28711  tglnne  28721  tglineeltr  28724  tglnne0  28733  colline  28742  tglowdim2l  28743  tglowdim2ln  28744  mirreu3  28747  mirbtwnhl  28773  krippenlem  28783  midexlem  28785  perpcom  28806  perpneq  28807  footexALT  28811  footex  28814  colperpexlem3  28825  colperpex  28826  opphllem  28828  midex  28830  oppne3  28836  opptgdim2  28838  oppnid  28839  opphllem2  28841  opphllem5  28844  opphllem6  28845  oppperpex  28846  outpasch  28848  hlpasch  28849  lnopp2hpgb  28856  hpgerlem  28858  colopp  28862  colhp  28863  lmieu  28877  lnperpex  28896  trgcopy  28897  trgcopyeulem  28898  iscgra1  28903  cgrane1  28905  cgrane2  28906  cgrane3  28907  cgrane4  28908  cgrahl1  28909  cgrahl2  28910  cgracgr  28911  cgraswap  28913  cgracom  28915  cgratr  28916  flatcgra  28917  cgrabtwn  28919  cgrahl  28920  sacgr  28924  acopyeu  28927  cgrg3col4  28946  tgasa1  28951  f1otrg  28964  f1otrge  28965  axeuclidlem  29056  axcontlem2  29059  umgrvad2edg  29307  usgredg2vlem2  29320  pthdepisspth  29828  clwwlkccatlem  30084  clwlkclwwlklem2  30095  3cycld  30273  eupth2lems  30333  eucrctshift  30338  frgr3vlem2  30369  n4cyclfrgr  30386  numclwwlk1lem2f1  30452  numclwwlk2lem1  30471  ubthlem3  30968  chirredlem1  32486  chirredlem3  32488  cdj1i  32529  fnpreimac  32769  xrge0infss  32859  nn0xmulclb  32870  hashxpe  32906  sgnmul  32934  2exple2exp  32944  ccatf1  33035  ccatws1f1o  33037  swrdf1  33042  dfmgc2lem  33081  mgcf1o  33089  mndlactf1  33112  mndlactfo  33113  mndractf1  33114  mndractfo  33115  gsumfs2d  33149  gsumhashmul  33155  suppgsumssiun  33160  xrge0tsmsd  33161  gsumwun  33164  psgnfzto1stlem  33188  cycpmco2  33221  cycpmrn  33231  tocyccntz  33232  cycpmconjslem2  33243  cyc3conja  33245  conjga  33258  submarchi  33274  isarchiofld  33287  elrgspnlem1  33330  elrgspnlem2  33331  elrgspnlem3  33332  elrgspnlem4  33333  elrgspnsubrunlem1  33335  elrgspnsubrunlem2  33336  elrgspnsubrun  33337  erlval  33346  erler  33353  rloccring  33358  rlocf1  33361  domnprodn0  33363  domnprodeq0  33364  subrdom  33373  imaslmod  33443  znfermltl  33456  lindfpropd  33472  unitprodclb  33479  nsgmgc  33502  nsgqusf1olem1  33503  unitpidl1  33514  elrspunidl  33518  elrspunsn  33519  rhmimaidl  33522  drngidl  33523  qsidomlem1  33542  mxidlprm  33560  mxidlirredi  33561  drngmxidlr  33568  qsdrngilem  33584  qsdrngi  33585  rsprprmprmidl  33612  rsprprmprmidlb  33613  rprmasso2  33616  rprmirred  33621  rprmirredb  33622  rprmdvdspow  33623  1arithidom  33627  pidufd  33633  1arithufdlem3  33636  dfufd2  33640  deg1prod  33673  ply1dg3rt0irred  33674  0mplrim  33705  mplidomlem  33718  extvfvcl  33727  mplvrpmga  33736  mplvrpmmhm  33737  mplvrpmrhm  33738  psrgsum  33739  psrmonprod  33743  esplymhp  33759  esplyfval3  33763  esplyfval1  33764  esplyfvaln  33765  esplyind  33766  exsslsb  33788  lbslelsp  33789  ply1degltdimlem  33813  lindsunlem  33815  lindsun  33816  lbsdiflsp0  33817  dimkerim  33818  fedgmul  33822  dimlssid  33823  assalactf1o  33826  extdg1id  33857  evls1fldgencl  33861  fldextrspunlsplem  33864  fldextrspunlsp  33865  extdgfialglem1  33883  minplyirred  33902  fldext2chn  33919  cos9thpiminplylem2  33974  smatrcl  33987  1smat1  33995  submateq  34000  mdetpmtr1  34014  madjusmdetlem2  34019  locfinreflem  34031  cmppcmp  34049  rhmpreimacn  34076  ordtrest2NEWlem  34113  ordtconnlem1  34115  lmdvg  34144  zrhcntr  34170  esumpcvgval  34269  esum2d  34284  sigapildsys  34353  ldgenpisyslem1  34354  fiunelros  34365  volmeas  34422  imambfm  34453  omssubadd  34491  carsggect  34509  carsgclctunlem3  34511  signsply0  34742  signstres  34766  actfunsnf1o  34795  actfunsnrndisj  34796  reprsuc  34806  reprinfz1  34813  breprexplema  34821  breprexplemc  34823  breprexp  34824  breprexpnat  34825  circlemeth  34831  hgt750lemb  34847  tgoldbachgtd  34853  erdszelem8  35433  pconnconn  35466  cvmlift2lem12  35549  cvmlift3lem5  35558  cvmlift3lem7  35560  cvmlift3lem8  35561  fmla1  35622  mrsubrn  35748  msrval  35773  msubff1  35791  btwnconn1lem13  36334  elicc3  36552  neibastop2lem  36595  weiunfr  36702  unbdqndv2  36824  irrdifflemf  37692  ltflcei  37982  lindsenlbs  37989  matunitlindflem1  37990  matunitlindflem2  37991  poimirlem4  37998  poimirlem13  38007  poimirlem14  38008  poimirlem22  38016  poimirlem26  38020  poimirlem27  38021  heicant  38029  mblfinlem2  38032  mblfinlem3  38033  mblfinlem4  38034  cnambfre  38042  itg2addnclem  38045  itg2addnclem2  38046  itg2gt0cn  38049  ftc1cnnc  38066  ftc1anclem5  38071  ftc1anclem7  38073  ftc1anc  38075  equivtotbnd  38152  isbndx  38156  ssbnd  38162  heibor1lem  38183  rrncmslem  38206  islshpat  39516  lfl1dim  39620  lfl1dim2N  39621  lkrpssN  39662  glbconN  39876  hlhgt2  39888  3dim2  39967  3dim3  39968  islln3  40009  islvol5  40078  2lplnja  40118  dalem19  40181  isline4N  40276  2polssN  40414  lhpmatb  40530  4atex  40575  trlatn0  40671  cdlemf2  41061  dialss  41545  diaglbN  41554  diaintclN  41557  dibglbN  41665  dibintclN  41666  dihlsscpre  41733  dihglblem5aN  41791  dihglblem2aN  41792  dihglblem4  41796  dihatexv  41837  dihjat1lem  41927  lcfl6  41999  mapdval2N  42129  aks4d1p8  42579  fldhmf1  42582  primrootscoprmpow  42591  primrootscoprbij2  42595  primrootspoweq0  42598  evl1gprodd  42609  hashscontpow  42614  aks6d1c2lem4  42619  idomnnzgmulnz  42625  deg1gprod  42632  sticksstones8  42645  sticksstones12a  42649  aks6d1c6lem3  42664  aks6d1c6lem5  42669  aks6d1c7  42676  aks5lem5a  42683  unitscyglem2  42688  sn-0tie0  42948  imacrhmcl  43011  fiabv  43029  evlselv  43046  fsuppind  43047  prjspertr  43062  prjspreln0  43066  prjspner1  43083  elrfi  43150  eldioph2  43218  diophin  43228  irrapxlem2  43275  irrapxlem3  43276  irrapxlem4  43277  irrapxlem5  43278  pell1234qrne0  43305  pell1234qrreccl  43306  pell1234qrmulcl  43307  pell14qrgt0  43311  pell14qrdich  43321  pell1qrge1  43322  pellfundex  43338  congabseq  43426  jm2.27b  43458  jm2.27  43460  fnwe2lem2  43503  kelac1  43515  lnrfg  43571  hbt  43582  omabs2  43784  nadd1suc  43844  rfovcnvf1od  44455  ntrneiiso  44542  ntrneikb  44545  ntrneixb  44546  ntrneik3  44547  ntrneix3  44548  ntrneik13  44549  ntrneix13  44550  cvgdvgrat  44764  binomcxplemnotnn0  44807  sineq0ALT  45387  fnchoice  45484  disjf1  45637  supxrgere  45785  supxrgelem  45789  supxrge  45790  suplesup  45791  xralrple2  45806  infxr  45818  infleinflem2  45822  infleinf  45823  uzub  45881  mccl  46050  limcrecl  46081  lptioo2  46083  lptioo1  46084  lptre2pt  46090  addlimc  46098  limsupmnflem  46170  climxrre  46200  liminflimsupclim  46257  climxlim2lem  46295  xlimliminflimsup  46312  icccncfext  46337  cncfiooicclem1  46343  cncfiooiccre  46345  dvbdfbdioolem2  46379  ioodvbdlimc1lem1  46381  dvnxpaek  46392  dvmptfprodlem  46394  dvmptfprod  46395  dvnprodlem3  46398  itgioocnicc  46427  itgspltprt  46429  stoweidlem31  46481  fourierdlem39  46596  fourierdlem42  46599  fourierdlem48  46604  fourierdlem49  46605  fourierdlem50  46606  fourierdlem51  46607  fourierdlem64  46620  fourierdlem65  46621  fourierdlem74  46630  fourierdlem75  46631  fourierdlem81  46637  fourierdlem82  46638  fourierdlem101  46657  etransclem23  46707  etransclem27  46711  etransclem32  46716  etransclem33  46717  etransclem35  46719  etransclem38  46722  sge0tsms  46830  sge0cl  46831  sge0f1o  46832  sge0split  46859  sge0rpcpnf  46871  sge0seq  46896  nnfoctbdjlem  46905  iundjiun  46910  meaiuninc3v  46934  meaiininclem  46936  omeiunltfirp  46969  carageniuncllem2  46972  carageniuncl  46973  hoicvr  46998  hoidmv1lelem1  47041  hoidmvlelem3  47047  hoidmvlelem5  47049  hoidmvle  47050  hoiqssbllem3  47074  iunhoiioolem  47125  pimdecfgtioo  47167  pimincfltioo  47168  preimageiingt  47170  preimaleiinlt  47171  smflimlem4  47224  chnerlem1  47334  iccpartigtl  47905  iccpartgt  47909  sprsymrelf1lem  47973  paireqne  47993  proththd  48099  requad2  48121  sbgoldbst  48276  bgoldbtbndlem4  48306  isuspgrim0lem  48391  isuspgrim0  48392  isuspgrimlem  48393  gricushgr  48415  grimedg  48433  grimgrtri  48447  isubgr3stgrlem7  48470  gpgusgralem  48554  pgn4cyclex  48624  2zrngmmgm  48750  cznrng  48759  rhmsubcALTVlem4  48782  srhmsubcALTV  48823  lincsum  48927  lcoss  48934  snlindsntor  48969  islindeps2  48981  line2x  49252  line2y  49253  itscnhlinecirc02p  49283  discsubc  49561  imasubc3  49653  uppropd  49678  swapfval  49759  fucofvalg  49815  fuco21  49833  precofvalALT  49865  2arwcat  50097  lanup  50138  ranup  50139