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  7261  fimaproj  8117  frxp3  8133  oaabs  8615  oaabs2  8616  omabs  8618  cofon1  8639  undomOLD  9034  sbthlem8  9064  findcard3OLD  9237  cantnfle  9631  cantnfp1  9641  cantnflem1c  9647  sornom  10237  enfin2i  10281  ttukeylem6  10474  fpwwe2lem12  10602  fpwwe2  10603  winalim2  10656  wuncval2  10707  negf1o  11615  xlemul1a  13255  difreicc  13452  flflp1  13776  faclbnd  14262  swrdswrd  14677  swrdccatin1  14697  pfxccatin12lem3  14704  swrdccat3blem  14711  ello12  15489  lo1bdd2  15497  elo12  15500  rlimclim1  15518  rlimcld2  15551  o1co  15559  o1of2  15586  o1rlimmul  15592  rlimsqzlem  15622  isercoll  15641  o1fsum  15786  supcvg  15829  dvds2ln  16266  lcmgcdlem  16583  cncongr2  16645  isprm5  16684  prmdvdsncoprmbd  16704  pcadd  16867  vdwlem2  16960  vdwlem11  16969  sbcie3s  17139  prdsval  17425  mreexexlem4d  17615  isacs2  17621  catcocl  17653  catass  17654  subccocl  17814  fullsubc  17819  funcco  17840  funcpropd  17871  fullpropd  17891  ffthiso  17900  isnat  17919  natpropd  17948  fucpropd  17949  xpcval  18145  evlf2  18186  curfpropd  18201  curfuncf  18206  uncfcurf  18207  curf2ndf  18215  hofcl  18227  hofpropd  18235  yonffthlem  18250  isacs3lem  18508  acsfiindd  18519  gsumpropd2lem  18613  resmgmhm2b  18647  resmhm2b  18756  mhmid  19002  mhmmnd  19003  ghmgrp  19005  conjnmzb  19192  ghmqusnsg  19221  ghmquskerlem3  19225  ghmqusker  19226  pgpfi  19542  sylow3lem2  19565  efgredlem  19684  frgpnabllem1  19810  imasabl  19813  dprdfcntz  19954  ablfac1b  20009  pgpfac1lem3  20016  pgpfac1lem5  20018  pgpfaclem3  20022  ringinvnzdiv  20217  rnghmsubcsetclem2  20548  rhmsubcsetclem2  20577  srhmsubc  20596  rhmsubclem4  20604  imadrhmcl  20713  cntzsdrg  20718  islmhm2  20952  lspsneleq  21032  rhmpreimaidl  21194  znunit  21480  psgndiflemB  21516  uvcff  21707  uvcf1  21708  lindfmm  21743  sraassab  21784  psrval  21831  psrass1  21880  resspsrmul  21892  mplbas2  21956  mhpmulcl  22043  psdmul  22060  coe1tmmul  22170  gsummoncoe1  22202  evls1fpws  22263  dmatsubcl  22392  scmatscm  22407  smatvscl  22418  marrepval  22456  mdetdiaglem  22492  mdetunilem8  22513  mdetunilem9  22514  pmatcoe1fsupp  22595  decpmatmulsumfsupp  22667  pmatcollpw2lem  22671  mp2pm2mplem4  22703  pm2mpmhmlem1  22712  pm2mpmhmlem2  22713  pm2mp  22719  fvmptnn04if  22743  cpmadugsumfi  22771  cpmidg2sum  22774  cpmadumatpoly  22777  cayhamlem4  22782  neiptoptop  23025  neitr  23074  ordtrest2lem  23097  cnpnei  23158  iscncl  23163  cncls  23168  cnntr  23169  cncnp  23174  lmcnp  23198  isreg2  23271  hauscmplem  23300  cmpfi  23302  1stcfb  23339  1stcrest  23347  2ndcctbss  23349  2ndcomap  23352  islly2  23378  cldllycmp  23389  lly1stc  23390  locfincmp  23420  llycmpkgen2  23444  1stckgenlem  23447  kgencn2  23451  kgencn3  23452  ptbasfi  23475  ptpjopn  23506  txdis1cn  23529  txlly  23530  txnlly  23531  txtube  23534  txcmplem2  23536  tx1stc  23544  txkgen  23546  xkopt  23549  xkoco2cn  23552  xkococnlem  23553  xkococn  23554  xkoinjcn  23581  tgqtop  23606  regr1lem  23633  kqreglem1  23635  nrmhmph  23688  rnelfmlem  23846  rnelfm  23847  fmfnfmlem4  23851  fmfnfm  23852  ufldom  23856  flimopn  23869  hauspwpwf1  23881  fclsopn  23908  fclsnei  23913  fclsrest  23918  alexsublem  23938  alexsubALTlem3  23943  ptcmplem2  23947  ptcmplem3  23948  cnextfun  23958  cnextcn  23961  symgtgp  24000  tgpt0  24013  qustgpopn  24014  tsmsxplem1  24047  trust  24124  utopsnneiplem  24142  utop3cls  24146  utopreg  24147  isucn2  24173  cstucnd  24178  ucncn  24179  fmucnd  24186  cfilufg  24187  neipcfilu  24190  met2ndci  24417  prdsxmslem2  24424  metcnp3  24435  metustid  24449  metustexhalf  24451  metust  24453  psmetutop  24462  nmoleub  24626  reconnlem2  24723  xrge0tsms  24730  cncfco  24807  lebnumlem3  24869  lebnum  24870  nmoleub2lem2  25023  nmoleub3  25026  iscfil2  25173  iscau4  25186  iscmet3lem2  25199  equivcfil  25206  equivcau  25207  caubl  25215  rrxdstprj1  25316  ovolshftlem2  25418  ovolicc2lem4  25428  uniioombl  25497  i1fmulclem  25610  mbfi1fseqlem6  25628  itg2const2  25649  itg2split  25657  bddiblnc  25750  ellimc2  25785  ellimc3  25787  limcflf  25789  dvmptfsum  25886  dvferm1  25896  dvferm2  25898  dvlip2  25907  c1lip1  25909  lhop1  25926  ftc1a  25951  ply1divex  26049  plyeq0lem  26122  plymullem1  26126  coemullem  26162  coemulc  26167  ulmshftlem  26305  ulmcaulem  26310  ulmbdd  26314  ulmcn  26315  ulmdvlem3  26318  mtestbdd  26321  pserulm  26338  pserdvlem2  26345  abelthlem8  26356  xrlimcnp  26885  jensen  26906  lgamucov  26955  logfac2  27135  dchrelbas3  27156  dchrpt  27185  gausslemma2dlem1a  27283  lgsquad3  27305  2sqb  27350  rpvmasumlem  27405  dchrisumlem1  27407  dchrisumlem3  27409  dchrmusum2  27412  dchrvmasumlem2  27416  dchrisum0flblem1  27426  dchrisum0lem1b  27433  dchrisum0lem1  27434  dchrisum0  27438  mulog2sumlem2  27453  pntlem3  27527  ostth3  27556  slerec  27738  cofcutr  27839  remulscllem2  28359  istrkgcb  28390  tgbtwndiff  28440  iscgrglt  28448  tgcgrxfr  28452  motcgrg  28478  lnext  28501  tgbtwnconn1  28509  tgbtwnconn3  28511  legval  28518  legtrid  28525  legso  28533  hlcgreu  28552  tglnne  28562  tglineeltr  28565  tglnne0  28574  colline  28583  tglowdim2l  28584  tglowdim2ln  28585  mirreu3  28588  mirbtwnhl  28614  krippenlem  28624  midexlem  28626  perpcom  28647  perpneq  28648  footexALT  28652  footex  28655  colperpexlem3  28666  colperpex  28667  opphllem  28669  midex  28671  oppne3  28677  opptgdim2  28679  oppnid  28680  opphllem2  28682  opphllem5  28685  opphllem6  28686  oppperpex  28687  outpasch  28689  hlpasch  28690  lnopp2hpgb  28697  hpgerlem  28699  colopp  28703  colhp  28704  lmieu  28718  lnperpex  28737  trgcopy  28738  trgcopyeulem  28739  iscgra1  28744  cgrane1  28746  cgrane2  28747  cgrane3  28748  cgrane4  28749  cgrahl1  28750  cgrahl2  28751  cgracgr  28752  cgraswap  28754  cgracom  28756  cgratr  28757  flatcgra  28758  cgrabtwn  28760  cgrahl  28761  sacgr  28765  acopyeu  28768  cgrg3col4  28787  tgasa1  28792  f1otrg  28805  f1otrge  28806  axeuclidlem  28896  axcontlem2  28899  umgrvad2edg  29147  usgredg2vlem2  29160  pthdepisspth  29672  clwwlkccatlem  29925  clwlkclwwlklem2  29936  3cycld  30114  eupth2lems  30174  eucrctshift  30179  frgr3vlem2  30210  n4cyclfrgr  30227  numclwwlk1lem2f1  30293  numclwwlk2lem1  30312  ubthlem3  30808  chirredlem1  32326  chirredlem3  32328  cdj1i  32369  fnpreimac  32602  xrge0infss  32690  nn0xmulclb  32701  hashxpe  32739  sgnmul  32767  2exple2exp  32777  ccatf1  32877  ccatws1f1o  32880  swrdf1  32885  dfmgc2lem  32928  mgcf1o  32936  chnind  32944  mndlactf1  32974  mndlactfo  32975  mndractf1  32976  mndractfo  32977  gsumfs2d  33002  gsumhashmul  33008  xrge0tsmsd  33009  gsumwun  33012  omndmul2  33033  gsumle  33045  psgnfzto1stlem  33064  cycpmco2  33097  cycpmrn  33107  tocyccntz  33108  cycpmconjslem2  33119  cyc3conja  33121  conjga  33134  submarchi  33147  elrgspnlem1  33200  elrgspnlem2  33201  elrgspnlem3  33202  elrgspnlem4  33203  elrgspnsubrunlem1  33205  elrgspnsubrunlem2  33206  elrgspnsubrun  33207  erlval  33216  erler  33223  rloccring  33228  rlocf1  33231  domnprodn0  33233  subrdom  33242  suborng  33300  isarchiofld  33302  imaslmod  33331  znfermltl  33344  lindfpropd  33360  unitprodclb  33367  nsgmgc  33390  nsgqusf1olem1  33391  unitpidl1  33402  elrspunidl  33406  elrspunsn  33407  rhmimaidl  33410  drngidl  33411  qsidomlem1  33430  mxidlprm  33448  mxidlirredi  33449  drngmxidlr  33456  qsdrngilem  33472  qsdrngi  33473  rsprprmprmidl  33500  rsprprmprmidlb  33501  rprmasso2  33504  rprmirred  33509  rprmirredb  33510  rprmdvdspow  33511  1arithidom  33515  pidufd  33521  1arithufdlem3  33524  dfufd2  33528  ply1dg3rt0irred  33558  exsslsb  33599  lbslelsp  33600  ply1degltdimlem  33625  lindsunlem  33627  lindsun  33628  lbsdiflsp0  33629  dimkerim  33630  fedgmul  33634  dimlssid  33635  assalactf1o  33638  extdg1id  33668  evls1fldgencl  33672  fldextrspunlsplem  33675  fldextrspunlsp  33676  minplyirred  33708  fldext2chn  33725  cos9thpiminplylem2  33780  smatrcl  33793  1smat1  33801  submateq  33806  mdetpmtr1  33820  madjusmdetlem2  33825  locfinreflem  33837  cmppcmp  33855  rhmpreimacn  33882  ordtrest2NEWlem  33919  ordtconnlem1  33921  lmdvg  33950  zrhcntr  33976  esumpcvgval  34075  esum2d  34090  sigapildsys  34159  ldgenpisyslem1  34160  fiunelros  34171  volmeas  34228  imambfm  34260  omssubadd  34298  carsggect  34316  carsgclctunlem3  34318  signsply0  34549  signstres  34573  actfunsnf1o  34602  actfunsnrndisj  34603  reprsuc  34613  reprinfz1  34620  breprexplema  34628  breprexplemc  34630  breprexp  34631  breprexpnat  34632  circlemeth  34638  hgt750lemb  34654  tgoldbachgtd  34660  erdszelem8  35192  pconnconn  35225  cvmlift2lem12  35308  cvmlift3lem5  35317  cvmlift3lem7  35319  cvmlift3lem8  35320  fmla1  35381  mrsubrn  35507  msrval  35532  msubff1  35550  btwnconn1lem13  36094  elicc3  36312  neibastop2lem  36355  weiunfr  36462  unbdqndv2  36506  irrdifflemf  37320  ltflcei  37609  lindsenlbs  37616  matunitlindflem1  37617  matunitlindflem2  37618  poimirlem4  37625  poimirlem13  37634  poimirlem14  37635  poimirlem22  37643  poimirlem26  37647  poimirlem27  37648  heicant  37656  mblfinlem2  37659  mblfinlem3  37660  mblfinlem4  37661  cnambfre  37669  itg2addnclem  37672  itg2addnclem2  37673  itg2gt0cn  37676  ftc1cnnc  37693  ftc1anclem5  37698  ftc1anclem7  37700  ftc1anc  37702  equivtotbnd  37779  isbndx  37783  ssbnd  37789  heibor1lem  37810  rrncmslem  37833  islshpat  39017  lfl1dim  39121  lfl1dim2N  39122  lkrpssN  39163  glbconN  39377  glbconNOLD  39378  hlhgt2  39390  3dim2  39469  3dim3  39470  islln3  39511  islvol5  39580  2lplnja  39620  dalem19  39683  isline4N  39778  2polssN  39916  lhpmatb  40032  4atex  40077  trlatn0  40173  cdlemf2  40563  dialss  41047  diaglbN  41056  diaintclN  41059  dibglbN  41167  dibintclN  41168  dihlsscpre  41235  dihglblem5aN  41293  dihglblem2aN  41294  dihglblem4  41298  dihatexv  41339  dihjat1lem  41429  lcfl6  41501  mapdval2N  41631  aks4d1p8  42082  fldhmf1  42085  primrootscoprmpow  42094  primrootscoprbij2  42098  primrootspoweq0  42101  evl1gprodd  42112  hashscontpow  42117  aks6d1c2lem4  42122  idomnnzgmulnz  42128  deg1gprod  42135  sticksstones8  42148  sticksstones12a  42152  aks6d1c6lem3  42167  aks6d1c6lem5  42172  aks6d1c7  42179  aks5lem5a  42186  unitscyglem2  42191  sn-0tie0  42446  imacrhmcl  42509  fiabv  42531  evlsvvval  42558  evlselv  42582  fsuppind  42585  prjspertr  42600  prjspreln0  42604  prjspner1  42621  elrfi  42689  eldioph2  42757  diophin  42767  irrapxlem2  42818  irrapxlem3  42819  irrapxlem4  42820  irrapxlem5  42821  pell1234qrne0  42848  pell1234qrreccl  42849  pell1234qrmulcl  42850  pell14qrgt0  42854  pell14qrdich  42864  pell1qrge1  42865  pellfundex  42881  congabseq  42970  jm2.27b  43002  jm2.27  43004  fnwe2lem2  43047  kelac1  43059  lnrfg  43115  hbt  43126  omabs2  43328  nadd1suc  43388  rfovcnvf1od  44000  ntrneiiso  44087  ntrneikb  44090  ntrneixb  44091  ntrneik3  44092  ntrneix3  44093  ntrneik13  44094  ntrneix13  44095  cvgdvgrat  44309  binomcxplemnotnn0  44352  sineq0ALT  44933  fnchoice  45030  disjf1  45184  supxrgere  45336  supxrgelem  45340  supxrge  45341  suplesup  45342  xralrple2  45357  infxr  45370  infleinflem2  45374  infleinf  45375  uzub  45434  mccl  45603  limcrecl  45634  lptioo2  45636  lptioo1  45637  lptre2pt  45645  addlimc  45653  limsupmnflem  45725  climxrre  45755  liminflimsupclim  45812  climxlim2lem  45850  xlimliminflimsup  45867  icccncfext  45892  cncfiooicclem1  45898  cncfiooiccre  45900  dvbdfbdioolem2  45934  ioodvbdlimc1lem1  45936  dvnxpaek  45947  dvmptfprodlem  45949  dvmptfprod  45950  dvnprodlem3  45953  itgioocnicc  45982  itgspltprt  45984  stoweidlem31  46036  fourierdlem39  46151  fourierdlem42  46154  fourierdlem48  46159  fourierdlem49  46160  fourierdlem50  46161  fourierdlem51  46162  fourierdlem64  46175  fourierdlem65  46176  fourierdlem74  46185  fourierdlem75  46186  fourierdlem81  46192  fourierdlem82  46193  fourierdlem101  46212  etransclem23  46262  etransclem27  46266  etransclem32  46271  etransclem33  46272  etransclem35  46274  etransclem38  46277  sge0tsms  46385  sge0cl  46386  sge0f1o  46387  sge0split  46414  sge0rpcpnf  46426  sge0seq  46451  nnfoctbdjlem  46460  iundjiun  46465  meaiuninc3v  46489  meaiininclem  46491  omeiunltfirp  46524  carageniuncllem2  46527  carageniuncl  46528  hoidmv1lelem1  46596  hoidmvlelem3  46602  hoidmvlelem5  46604  hoidmvle  46605  hoiqssbllem3  46629  iunhoiioolem  46680  pimdecfgtioo  46722  pimincfltioo  46723  preimageiingt  46725  preimaleiinlt  46726  smflimlem4  46779  iccpartigtl  47428  iccpartgt  47432  sprsymrelf1lem  47496  paireqne  47516  proththd  47619  requad2  47628  sbgoldbst  47783  bgoldbtbndlem4  47813  isuspgrim0lem  47897  isuspgrim0  47898  isuspgrimlem  47899  gricushgr  47921  grimedg  47939  grimgrtri  47952  isubgr3stgrlem7  47975  gpgusgralem  48051  pgn4cyclex  48120  2zrngmmgm  48244  cznrng  48253  rhmsubcALTVlem4  48276  srhmsubcALTV  48317  lincsum  48422  lcoss  48429  snlindsntor  48464  islindeps2  48476  line2x  48747  line2y  48748  itscnhlinecirc02p  48778  discsubc  49057  imasubc3  49149  uppropd  49174  swapfval  49255  fucofvalg  49311  fuco21  49329  precofvalALT  49361  2arwcat  49593  lanup  49634  ranup  49635