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  simplll  774  fsnex  7217  fimaproj  8065  frxp3  8081  oaabs  8563  oaabs2  8564  omabs  8566  cofon1  8587  sbthlem8  9007  cantnfle  9561  cantnfp1  9571  cantnflem1c  9577  sornom  10165  enfin2i  10209  ttukeylem6  10402  fpwwe2lem12  10530  fpwwe2  10531  winalim2  10584  wuncval2  10635  negf1o  11544  xlemul1a  13184  difreicc  13381  flflp1  13708  faclbnd  14194  swrdswrd  14609  swrdccatin1  14629  pfxccatin12lem3  14636  swrdccat3blem  14643  ello12  15420  lo1bdd2  15428  elo12  15431  rlimclim1  15449  rlimcld2  15482  o1co  15490  o1of2  15517  o1rlimmul  15523  rlimsqzlem  15553  isercoll  15572  o1fsum  15717  supcvg  15760  dvds2ln  16197  lcmgcdlem  16514  cncongr2  16576  isprm5  16615  prmdvdsncoprmbd  16635  pcadd  16798  vdwlem2  16891  vdwlem11  16900  sbcie3s  17070  prdsval  17356  mreexexlem4d  17550  isacs2  17556  catcocl  17588  catass  17589  subccocl  17749  fullsubc  17754  funcco  17775  funcpropd  17806  fullpropd  17826  ffthiso  17835  isnat  17854  natpropd  17883  fucpropd  17884  xpcval  18080  evlf2  18121  curfpropd  18136  curfuncf  18141  uncfcurf  18142  curf2ndf  18150  hofcl  18162  hofpropd  18170  yonffthlem  18185  isacs3lem  18445  acsfiindd  18456  chnind  18524  gsumpropd2lem  18584  resmgmhm2b  18618  resmhm2b  18727  mhmid  18973  mhmmnd  18974  ghmgrp  18976  conjnmzb  19163  ghmqusnsg  19192  ghmquskerlem3  19196  ghmqusker  19197  pgpfi  19515  sylow3lem2  19538  efgredlem  19657  frgpnabllem1  19783  imasabl  19786  dprdfcntz  19927  ablfac1b  19982  pgpfac1lem3  19989  pgpfac1lem5  19991  pgpfaclem3  19995  omndmul2  20043  gsumle  20055  ringinvnzdiv  20217  rnghmsubcsetclem2  20545  rhmsubcsetclem2  20574  srhmsubc  20593  rhmsubclem4  20601  imadrhmcl  20710  cntzsdrg  20715  suborng  20789  islmhm2  20970  lspsneleq  21050  rhmpreimaidl  21212  znunit  21498  psgndiflemB  21535  uvcff  21726  uvcf1  21727  lindfmm  21762  sraassab  21803  psrval  21850  psrass1  21899  resspsrmul  21911  mplbas2  21975  mhpmulcl  22062  psdmul  22079  coe1tmmul  22189  gsummoncoe1  22221  evls1fpws  22282  dmatsubcl  22411  scmatscm  22426  smatvscl  22437  marrepval  22475  mdetdiaglem  22511  mdetunilem8  22532  mdetunilem9  22533  pmatcoe1fsupp  22614  decpmatmulsumfsupp  22686  pmatcollpw2lem  22690  mp2pm2mplem4  22722  pm2mpmhmlem1  22731  pm2mpmhmlem2  22732  pm2mp  22738  fvmptnn04if  22762  cpmadugsumfi  22790  cpmidg2sum  22793  cpmadumatpoly  22796  cayhamlem4  22801  neiptoptop  23044  neitr  23093  ordtrest2lem  23116  cnpnei  23177  iscncl  23182  cncls  23187  cnntr  23188  cncnp  23193  lmcnp  23217  isreg2  23290  hauscmplem  23319  cmpfi  23321  1stcfb  23358  1stcrest  23366  2ndcctbss  23368  2ndcomap  23371  islly2  23397  cldllycmp  23408  lly1stc  23409  locfincmp  23439  llycmpkgen2  23463  1stckgenlem  23466  kgencn2  23470  kgencn3  23471  ptbasfi  23494  ptpjopn  23525  txdis1cn  23548  txlly  23549  txnlly  23550  txtube  23553  txcmplem2  23555  tx1stc  23563  txkgen  23565  xkopt  23568  xkoco2cn  23571  xkococnlem  23572  xkococn  23573  xkoinjcn  23600  tgqtop  23625  regr1lem  23652  kqreglem1  23654  nrmhmph  23707  rnelfmlem  23865  rnelfm  23866  fmfnfmlem4  23870  fmfnfm  23871  ufldom  23875  flimopn  23888  hauspwpwf1  23900  fclsopn  23927  fclsnei  23932  fclsrest  23937  alexsublem  23957  alexsubALTlem3  23962  ptcmplem2  23966  ptcmplem3  23967  cnextfun  23977  cnextcn  23980  symgtgp  24019  tgpt0  24032  qustgpopn  24033  tsmsxplem1  24066  trust  24142  utopsnneiplem  24160  utop3cls  24164  utopreg  24165  isucn2  24191  cstucnd  24196  ucncn  24197  fmucnd  24204  cfilufg  24205  neipcfilu  24208  met2ndci  24435  prdsxmslem2  24442  metcnp3  24453  metustid  24467  metustexhalf  24469  metust  24471  psmetutop  24480  nmoleub  24644  reconnlem2  24741  xrge0tsms  24748  cncfco  24825  lebnumlem3  24887  lebnum  24888  nmoleub2lem2  25041  nmoleub3  25044  iscfil2  25191  iscau4  25204  iscmet3lem2  25217  equivcfil  25224  equivcau  25225  caubl  25233  rrxdstprj1  25334  ovolshftlem2  25436  ovolicc2lem4  25446  uniioombl  25515  i1fmulclem  25628  mbfi1fseqlem6  25646  itg2const2  25667  itg2split  25675  bddiblnc  25768  ellimc2  25803  ellimc3  25805  limcflf  25807  dvmptfsum  25904  dvferm1  25914  dvferm2  25916  dvlip2  25925  c1lip1  25927  lhop1  25944  ftc1a  25969  ply1divex  26067  plyeq0lem  26140  plymullem1  26144  coemullem  26180  coemulc  26185  ulmshftlem  26323  ulmcaulem  26328  ulmbdd  26332  ulmcn  26333  ulmdvlem3  26336  mtestbdd  26339  pserulm  26356  pserdvlem2  26363  abelthlem8  26374  xrlimcnp  26903  jensen  26924  lgamucov  26973  logfac2  27153  dchrelbas3  27174  dchrpt  27203  gausslemma2dlem1a  27301  lgsquad3  27323  2sqb  27368  rpvmasumlem  27423  dchrisumlem1  27425  dchrisumlem3  27427  dchrmusum2  27430  dchrvmasumlem2  27434  dchrisum0flblem1  27444  dchrisum0lem1b  27451  dchrisum0lem1  27452  dchrisum0  27456  mulog2sumlem2  27471  pntlem3  27545  ostth3  27574  slerec  27758  cofcutr  27866  remulscllem2  28401  istrkgcb  28432  tgbtwndiff  28482  iscgrglt  28490  tgcgrxfr  28494  motcgrg  28520  lnext  28543  tgbtwnconn1  28551  tgbtwnconn3  28553  legval  28560  legtrid  28567  legso  28575  hlcgreu  28594  tglnne  28604  tglineeltr  28607  tglnne0  28616  colline  28625  tglowdim2l  28626  tglowdim2ln  28627  mirreu3  28630  mirbtwnhl  28656  krippenlem  28666  midexlem  28668  perpcom  28689  perpneq  28690  footexALT  28694  footex  28697  colperpexlem3  28708  colperpex  28709  opphllem  28711  midex  28713  oppne3  28719  opptgdim2  28721  oppnid  28722  opphllem2  28724  opphllem5  28727  opphllem6  28728  oppperpex  28729  outpasch  28731  hlpasch  28732  lnopp2hpgb  28739  hpgerlem  28741  colopp  28745  colhp  28746  lmieu  28760  lnperpex  28779  trgcopy  28780  trgcopyeulem  28781  iscgra1  28786  cgrane1  28788  cgrane2  28789  cgrane3  28790  cgrane4  28791  cgrahl1  28792  cgrahl2  28793  cgracgr  28794  cgraswap  28796  cgracom  28798  cgratr  28799  flatcgra  28800  cgrabtwn  28802  cgrahl  28803  sacgr  28807  acopyeu  28810  cgrg3col4  28829  tgasa1  28834  f1otrg  28847  f1otrge  28848  axeuclidlem  28938  axcontlem2  28941  umgrvad2edg  29189  usgredg2vlem2  29202  pthdepisspth  29711  clwwlkccatlem  29964  clwlkclwwlklem2  29975  3cycld  30153  eupth2lems  30213  eucrctshift  30218  frgr3vlem2  30249  n4cyclfrgr  30266  numclwwlk1lem2f1  30332  numclwwlk2lem1  30351  ubthlem3  30847  chirredlem1  32365  chirredlem3  32367  cdj1i  32408  fnpreimac  32648  xrge0infss  32738  nn0xmulclb  32749  hashxpe  32784  sgnmul  32813  2exple2exp  32823  ccatf1  32925  ccatws1f1o  32927  swrdf1  32932  dfmgc2lem  32971  mgcf1o  32979  mndlactf1  33002  mndlactfo  33003  mndractf1  33004  mndractfo  33005  gsumfs2d  33030  gsumhashmul  33036  xrge0tsmsd  33037  gsumwun  33040  psgnfzto1stlem  33064  cycpmco2  33097  cycpmrn  33107  tocyccntz  33108  cycpmconjslem2  33119  cyc3conja  33121  conjga  33134  submarchi  33150  isarchiofld  33163  elrgspnlem1  33204  elrgspnlem2  33205  elrgspnlem3  33206  elrgspnlem4  33207  elrgspnsubrunlem1  33209  elrgspnsubrunlem2  33210  elrgspnsubrun  33211  erlval  33220  erler  33227  rloccring  33232  rlocf1  33235  domnprodn0  33237  subrdom  33246  imaslmod  33313  znfermltl  33326  lindfpropd  33342  unitprodclb  33349  nsgmgc  33372  nsgqusf1olem1  33373  unitpidl1  33384  elrspunidl  33388  elrspunsn  33389  rhmimaidl  33392  drngidl  33393  qsidomlem1  33412  mxidlprm  33430  mxidlirredi  33431  drngmxidlr  33438  qsdrngilem  33454  qsdrngi  33455  rsprprmprmidl  33482  rsprprmprmidlb  33483  rprmasso2  33486  rprmirred  33491  rprmirredb  33492  rprmdvdspow  33493  1arithidom  33497  pidufd  33503  1arithufdlem3  33506  dfufd2  33510  ply1dg3rt0irred  33541  mplvrpmga  33570  mplvrpmmhm  33571  mplvrpmrhm  33572  esplymhp  33584  exsslsb  33604  lbslelsp  33605  ply1degltdimlem  33630  lindsunlem  33632  lindsun  33633  lbsdiflsp0  33634  dimkerim  33635  fedgmul  33639  dimlssid  33640  assalactf1o  33643  extdg1id  33674  evls1fldgencl  33678  fldextrspunlsplem  33681  fldextrspunlsp  33682  extdgfialglem1  33700  minplyirred  33719  fldext2chn  33736  cos9thpiminplylem2  33791  smatrcl  33804  1smat1  33812  submateq  33817  mdetpmtr1  33831  madjusmdetlem2  33836  locfinreflem  33848  cmppcmp  33866  rhmpreimacn  33893  ordtrest2NEWlem  33930  ordtconnlem1  33932  lmdvg  33961  zrhcntr  33987  esumpcvgval  34086  esum2d  34101  sigapildsys  34170  ldgenpisyslem1  34171  fiunelros  34182  volmeas  34239  imambfm  34270  omssubadd  34308  carsggect  34326  carsgclctunlem3  34328  signsply0  34559  signstres  34583  actfunsnf1o  34612  actfunsnrndisj  34613  reprsuc  34623  reprinfz1  34630  breprexplema  34638  breprexplemc  34640  breprexp  34641  breprexpnat  34642  circlemeth  34648  hgt750lemb  34664  tgoldbachgtd  34670  erdszelem8  35230  pconnconn  35263  cvmlift2lem12  35346  cvmlift3lem5  35355  cvmlift3lem7  35357  cvmlift3lem8  35358  fmla1  35419  mrsubrn  35545  msrval  35570  msubff1  35588  btwnconn1lem13  36132  elicc3  36350  neibastop2lem  36393  weiunfr  36500  unbdqndv2  36544  irrdifflemf  37358  ltflcei  37647  lindsenlbs  37654  matunitlindflem1  37655  matunitlindflem2  37656  poimirlem4  37663  poimirlem13  37672  poimirlem14  37673  poimirlem22  37681  poimirlem26  37685  poimirlem27  37686  heicant  37694  mblfinlem2  37697  mblfinlem3  37698  mblfinlem4  37699  cnambfre  37707  itg2addnclem  37710  itg2addnclem2  37711  itg2gt0cn  37714  ftc1cnnc  37731  ftc1anclem5  37736  ftc1anclem7  37738  ftc1anc  37740  equivtotbnd  37817  isbndx  37821  ssbnd  37827  heibor1lem  37848  rrncmslem  37871  islshpat  39055  lfl1dim  39159  lfl1dim2N  39160  lkrpssN  39201  glbconN  39415  hlhgt2  39427  3dim2  39506  3dim3  39507  islln3  39548  islvol5  39617  2lplnja  39657  dalem19  39720  isline4N  39815  2polssN  39953  lhpmatb  40069  4atex  40114  trlatn0  40210  cdlemf2  40600  dialss  41084  diaglbN  41093  diaintclN  41096  dibglbN  41204  dibintclN  41205  dihlsscpre  41272  dihglblem5aN  41330  dihglblem2aN  41331  dihglblem4  41335  dihatexv  41376  dihjat1lem  41466  lcfl6  41538  mapdval2N  41668  aks4d1p8  42119  fldhmf1  42122  primrootscoprmpow  42131  primrootscoprbij2  42135  primrootspoweq0  42138  evl1gprodd  42149  hashscontpow  42154  aks6d1c2lem4  42159  idomnnzgmulnz  42165  deg1gprod  42172  sticksstones8  42185  sticksstones12a  42189  aks6d1c6lem3  42204  aks6d1c6lem5  42209  aks6d1c7  42216  aks5lem5a  42223  unitscyglem2  42228  sn-0tie0  42483  imacrhmcl  42546  fiabv  42568  evlsvvval  42595  evlselv  42619  fsuppind  42622  prjspertr  42637  prjspreln0  42641  prjspner1  42658  elrfi  42726  eldioph2  42794  diophin  42804  irrapxlem2  42855  irrapxlem3  42856  irrapxlem4  42857  irrapxlem5  42858  pell1234qrne0  42885  pell1234qrreccl  42886  pell1234qrmulcl  42887  pell14qrgt0  42891  pell14qrdich  42901  pell1qrge1  42902  pellfundex  42918  congabseq  43006  jm2.27b  43038  jm2.27  43040  fnwe2lem2  43083  kelac1  43095  lnrfg  43151  hbt  43162  omabs2  43364  nadd1suc  43424  rfovcnvf1od  44036  ntrneiiso  44123  ntrneikb  44126  ntrneixb  44127  ntrneik3  44128  ntrneix3  44129  ntrneik13  44130  ntrneix13  44131  cvgdvgrat  44345  binomcxplemnotnn0  44388  sineq0ALT  44968  fnchoice  45065  disjf1  45219  supxrgere  45371  supxrgelem  45375  supxrge  45376  suplesup  45377  xralrple2  45392  infxr  45404  infleinflem2  45408  infleinf  45409  uzub  45468  mccl  45637  limcrecl  45668  lptioo2  45670  lptioo1  45671  lptre2pt  45677  addlimc  45685  limsupmnflem  45757  climxrre  45787  liminflimsupclim  45844  climxlim2lem  45882  xlimliminflimsup  45899  icccncfext  45924  cncfiooicclem1  45930  cncfiooiccre  45932  dvbdfbdioolem2  45966  ioodvbdlimc1lem1  45968  dvnxpaek  45979  dvmptfprodlem  45981  dvmptfprod  45982  dvnprodlem3  45985  itgioocnicc  46014  itgspltprt  46016  stoweidlem31  46068  fourierdlem39  46183  fourierdlem42  46186  fourierdlem48  46191  fourierdlem49  46192  fourierdlem50  46193  fourierdlem51  46194  fourierdlem64  46207  fourierdlem65  46208  fourierdlem74  46217  fourierdlem75  46218  fourierdlem81  46224  fourierdlem82  46225  fourierdlem101  46244  etransclem23  46294  etransclem27  46298  etransclem32  46303  etransclem33  46304  etransclem35  46306  etransclem38  46309  sge0tsms  46417  sge0cl  46418  sge0f1o  46419  sge0split  46446  sge0rpcpnf  46458  sge0seq  46483  nnfoctbdjlem  46492  iundjiun  46497  meaiuninc3v  46521  meaiininclem  46523  omeiunltfirp  46556  carageniuncllem2  46559  carageniuncl  46560  hoidmv1lelem1  46628  hoidmvlelem3  46634  hoidmvlelem5  46636  hoidmvle  46637  hoiqssbllem3  46661  iunhoiioolem  46712  pimdecfgtioo  46754  pimincfltioo  46755  preimageiingt  46757  preimaleiinlt  46758  smflimlem4  46811  iccpartigtl  47453  iccpartgt  47457  sprsymrelf1lem  47521  paireqne  47541  proththd  47644  requad2  47653  sbgoldbst  47808  bgoldbtbndlem4  47838  isuspgrim0lem  47923  isuspgrim0  47924  isuspgrimlem  47925  gricushgr  47947  grimedg  47965  grimgrtri  47979  isubgr3stgrlem7  48002  gpgusgralem  48086  pgn4cyclex  48156  2zrngmmgm  48282  cznrng  48291  rhmsubcALTVlem4  48314  srhmsubcALTV  48355  lincsum  48460  lcoss  48467  snlindsntor  48502  islindeps2  48514  line2x  48785  line2y  48786  itscnhlinecirc02p  48816  discsubc  49095  imasubc3  49187  uppropd  49212  swapfval  49293  fucofvalg  49349  fuco21  49367  precofvalALT  49399  2arwcat  49631  lanup  49672  ranup  49673