Theorem ad3antrrr 740

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  ad4antr  742  ad4antlr  743  simplll  784  fsnex  7263  fimaproj  8110  frxp3  8126  oaabs  8613  oaabs2  8614  omabs  8616  cofon1  8637  sbthlem8  9062  cantnfle  9623  cantnfp1  9633  cantnflem1c  9639  sornom  10231  enfin2i  10275  ttukeylem6  10468  fpwwe2lem12  10597  fpwwe2  10598  winalim2  10651  wuncval2  10702  negf1o  11614  xlemul1a  13288  difreicc  13485  flflp1  13814  faclbnd  14300  swrdswrd  14715  swrdccatin1  14735  pfxccatin12lem3  14742  swrdccat3blem  14749  ello12  15526  lo1bdd2  15534  elo12  15537  rlimclim1  15555  rlimcld2  15588  o1co  15596  o1of2  15623  o1rlimmul  15629  rlimsqzlem  15659  isercoll  15678  o1fsum  15824  supcvg  15869  dvds2ln  16306  lcmgcdlem  16623  cncongr2  16685  isprm5  16725  prmdvdsncoprmbd  16745  pcadd  16908  vdwlem2  17001  vdwlem11  17010  sbcie3s  17181  prdsval  17467  mreexexlem4d  17662  isacs2  17668  catcocl  17700  catass  17701  subccocl  17861  fullsubc  17866  funcco  17887  funcpropd  17918  fullpropd  17938  ffthiso  17947  isnat  17966  natpropd  17995  fucpropd  17996  xpcval  18192  evlf2  18233  curfpropd  18248  curfuncf  18253  uncfcurf  18254  curf2ndf  18262  hofcl  18274  hofpropd  18282  yonffthlem  18297  isacs3lem  18557  acsfiindd  18568  chnind  18636  gsumpropd2lem  18696  resmgmhm2b  18730  resmhm2b  18839  mhmid  19088  mhmmnd  19089  ghmgrp  19091  conjnmzb  19276  ghmqusnsg  19305  ghmquskerlem3  19309  ghmqusker  19310  pgpfi  19628  sylow3lem2  19651  efgredlem  19770  frgpnabllem1  19896  imasabl  19899  dprdfcntz  20040  ablfac1b  20095  pgpfac1lem3  20102  pgpfac1lem5  20104  pgpfaclem3  20108  omndmul2  20156  gsumle  20168  ringinvnzdiv  20330  rnghmsubcsetclem2  20661  rhmsubcsetclem2  20690  srhmsubc  20709  rhmsubclem4  20717  imadrhmcl  20826  cntzsdrg  20831  suborng  20905  islmhm2  21085  lspsneleq  21165  rhmpreimaidl  21327  znunit  21595  psgndiflemB  21632  uvcff  21823  uvcf1  21824  lindfmm  21859  sraassab  21900  psrval  21947  psrass1  21995  resspsrmul  22007  mplbas2  22075  evlsvvval  22126  mhpmulcl  22194  psdmul  22211  coe1tmmul  22320  gsummoncoe1  22351  evls1fpws  22412  dmatsubcl  22538  scmatscm  22553  smatvscl  22564  marrepval  22602  mdetdiaglem  22638  mdetunilem8  22659  mdetunilem9  22660  pmatcoe1fsupp  22741  decpmatmulsumfsupp  22813  pmatcollpw2lem  22817  mp2pm2mplem4  22849  pm2mpmhmlem1  22858  pm2mpmhmlem2  22859  pm2mp  22865  fvmptnn04if  22889  cpmadugsumfi  22917  cpmidg2sum  22920  cpmadumatpoly  22923  cayhamlem4  22928  neiptoptop  23171  neitr  23220  ordtrest2lem  23243  cnpnei  23304  iscncl  23309  cncls  23314  cnntr  23315  cncnp  23320  lmcnp  23344  isreg2  23417  hauscmplem  23446  cmpfi  23448  1stcfb  23485  1stcrest  23493  2ndcctbss  23495  2ndcomap  23498  islly2  23524  cldllycmp  23535  lly1stc  23536  locfincmp  23566  llycmpkgen2  23590  1stckgenlem  23593  kgencn2  23597  kgencn3  23598  ptbasfi  23621  ptpjopn  23652  txdis1cn  23675  txlly  23676  txnlly  23677  txtube  23680  txcmplem2  23682  tx1stc  23690  txkgen  23692  xkopt  23695  xkoco2cn  23698  xkococnlem  23699  xkococn  23700  xkoinjcn  23727  tgqtop  23752  regr1lem  23779  kqreglem1  23781  nrmhmph  23834  rnelfmlem  23992  rnelfm  23993  fmfnfmlem4  23997  fmfnfm  23998  ufldom  24002  flimopn  24015  hauspwpwf1  24027  fclsopn  24054  fclsnei  24059  fclsrest  24064  alexsublem  24084  alexsubALTlem3  24089  ptcmplem2  24093  ptcmplem3  24094  cnextfun  24104  cnextcn  24107  symgtgp  24146  tgpt0  24159  qustgpopn  24160  tsmsxplem1  24193  trust  24269  utopsnneiplem  24287  utop3cls  24291  utopreg  24292  isucn2  24318  cstucnd  24323  ucncn  24324  fmucnd  24331  cfilufg  24332  neipcfilu  24335  met2ndci  24562  prdsxmslem2  24569  metcnp3  24580  metustid  24594  metustexhalf  24596  metust  24598  psmetutop  24607  nmoleub  24771  reconnlem2  24868  xrge0tsms  24875  cncfco  24949  lebnumlem3  25005  lebnum  25006  nmoleub2lem2  25158  nmoleub3  25161  iscfil2  25308  iscau4  25321  iscmet3lem2  25334  equivcfil  25341  equivcau  25342  caubl  25350  rrxdstprj1  25451  ovolshftlem2  25552  ovolicc2lem4  25562  uniioombl  25631  i1fmulclem  25744  mbfi1fseqlem6  25762  itg2const2  25783  itg2split  25791  bddiblnc  25884  ellimc2  25919  ellimc3  25921  limcflf  25923  dvmptfsum  26017  dvferm1  26027  dvferm2  26029  dvlip2  26037  c1lip1  26039  lhop1  26056  ftc1a  26079  ply1divex  26177  plyeq0lem  26250  plymullem1  26254  coemullem  26290  coemulc  26295  ulmshftlem  26429  ulmcaulem  26434  ulmbdd  26438  ulmcn  26439  ulmdvlem3  26442  mtestbdd  26445  pserulm  26462  pserdvlem2  26468  abelthlem8  26479  xrlimcnp  27010  jensen  27030  lgamucov  27079  logfac2  27258  dchrelbas3  27279  dchrpt  27308  gausslemma2dlem1a  27406  lgsquad3  27428  2sqb  27473  rpvmasumlem  27528  dchrisumlem1  27530  dchrisumlem3  27532  dchrmusum2  27535  dchrvmasumlem2  27539  dchrisum0flblem1  27549  dchrisum0lem1b  27556  dchrisum0lem1  27557  dchrisum0  27561  mulog2sumlem2  27576  pntlem3  27650  ostth3  27679  lesrec  27869  cofcutr  27994  remulscllem2  28571  istrkgcb  28602  tgbtwndiff  28652  iscgrglt  28660  tgcgrxfr  28664  motcgrg  28690  lnext  28713  tgbtwnconn1  28721  tgbtwnconn3  28723  legval  28730  legtrid  28737  legso  28745  hlcgreu  28764  tglnne  28774  tglineeltr  28777  tglnne0  28786  colline  28795  tglowdim2l  28796  tglowdim2ln  28797  mirreu3  28800  mirbtwnhl  28826  krippenlem  28836  midexlem  28838  perpcom  28859  perpneq  28860  footexALT  28864  footex  28867  colperpexlem3  28878  colperpex  28879  opphllem  28881  midex  28883  oppne3  28889  opptgdim2  28891  oppnid  28892  opphllem2  28894  opphllem5  28897  opphllem6  28898  oppperpex  28899  outpasch  28901  hlpasch  28902  lnopp2hpgb  28909  hpgerlem  28911  colopp  28915  colhp  28916  lmieu  28930  lnperpex  28949  trgcopy  28950  trgcopyeulem  28951  iscgra1  28956  cgrane1  28958  cgrane2  28959  cgrane3  28960  cgrane4  28961  cgrahl1  28962  cgrahl2  28963  cgracgr  28964  cgraswap  28966  cgracom  28968  cgratr  28969  flatcgra  28970  cgrabtwn  28972  cgrahl  28973  sacgr  28977  acopyeu  28980  cgrg3col4  28999  tgasa1  29004  f1otrg  29017  f1otrge  29018  axeuclidlem  29109  axcontlem2  29112  umgrvad2edg  29360  usgredg2vlem2  29373  pthdepisspth  29881  clwwlkccatlem  30137  clwlkclwwlklem2  30148  3cycld  30326  eupth2lems  30386  eucrctshift  30391  frgr3vlem2  30422  n4cyclfrgr  30439  numclwwlk1lem2f1  30505  numclwwlk2lem1  30524  ubthlem3  31021  chirredlem1  32539  chirredlem3  32541  cdj1i  32582  fnpreimac  32822  xrge0infss  32912  nn0xmulclb  32923  hashxpe  32959  sgnmul  32987  2exple2exp  32997  ccatf1  33088  ccatws1f1o  33090  swrdf1  33095  dfmgc2lem  33134  mgcf1o  33142  mndlactf1  33165  mndlactfo  33166  mndractf1  33167  mndractfo  33168  gsumfs2d  33202  gsumhashmul  33208  suppgsumssiun  33213  xrge0tsmsd  33214  gsumwun  33217  psgnfzto1stlem  33241  cycpmco2  33274  cycpmrn  33284  tocyccntz  33285  cycpmconjslem2  33296  cyc3conja  33298  conjga  33311  submarchi  33327  isarchiofld  33340  elrgspnlem1  33384  elrgspnlem2  33385  elrgspnlem3  33386  elrgspnlem4  33387  elrgspnsubrunlem1  33389  elrgspnsubrunlem2  33390  elrgspnsubrun  33391  erlval  33400  erler  33407  rloccring  33413  rlocf1  33416  rlocisunit  33418  domnprodn0  33420  domnprodeq0  33421  subrdom  33430  imaslmod  33500  znfermltl  33513  lindfpropd  33529  unitprodclb  33536  nsgmgc  33559  nsgqusf1olem1  33560  unitpidl1  33571  elrspunidl  33575  elrspunsn  33576  rhmimaidl  33579  drngidl  33580  qsidomlem1  33600  prmidlsubm  33607  mxidlprm  33619  mxidlirredi  33620  drngmxidlr  33627  qsdrngilem  33643  qsdrngi  33644  drnglring  33649  dflringlem2  33652  dflring3  33654  dflring4  33655  rsprprmprmidl  33679  rsprprmprmidlb  33680  rprmasso2  33683  rprmirred  33688  rprmirredb  33689  rprmdvdspow  33690  1arithidom  33694  pidufd  33700  1arithufdlem3  33703  dfufd2  33707  deg1prod  33740  ply1dg3rt0irred  33741  0mplrim  33772  mplidomlem  33785  extvfvcl  33794  mplvrpmga  33803  mplvrpmmhm  33804  mplvrpmrhm  33805  psrgsum  33806  psrmonprod  33810  esplymhp  33826  esplyfval3  33830  esplyfval1  33831  esplyfvaln  33832  esplyind  33833  exsslsb  33855  lbslelsp  33856  ply1degltdimlem  33880  lindsunlem  33882  lindsun  33883  lbsdiflsp0  33884  dimkerim  33885  fedgmul  33889  dimlssid  33890  assalactf1o  33893  extdg1id  33924  evls1fldgencl  33928  fldextrspunlsplem  33931  fldextrspunlsp  33932  extdgfialglem1  33950  minplyirred  33969  fldext2chn  33986  cos9thpiminplylem2  34041  smatrcl  34054  1smat1  34062  submateq  34067  mdetpmtr1  34081  madjusmdetlem2  34086  locfinreflem  34098  cmppcmp  34116  rhmpreimacn  34143  ordtrest2NEWlem  34180  ordtconnlem1  34182  lmdvg  34211  zrhcntr  34237  esumpcvgval  34336  esum2d  34351  sigapildsys  34420  ldgenpisyslem1  34421  fiunelros  34432  volmeas  34489  imambfm  34520  omssubadd  34558  carsggect  34576  carsgclctunlem3  34578  signsply0  34809  signstres  34833  actfunsnf1o  34862  actfunsnrndisj  34863  reprsuc  34873  reprinfz1  34880  breprexplema  34888  breprexplemc  34890  breprexp  34891  breprexpnat  34892  circlemeth  34898  hgt750lemb  34914  tgoldbachgtd  34920  erdszelem8  35512  pconnconn  35545  cvmlift2lem12  35628  cvmlift3lem5  35637  cvmlift3lem7  35639  cvmlift3lem8  35640  fmla1  35701  mrsubrn  35827  msrval  35852  msubff1  35870  btwnconn1lem13  36413  elicc3  36641  neibastop2lem  36684  weiunfr  36791  unbdqndv2  36913  irrdifflemf  37781  ltflcei  38071  lindsenlbs  38078  matunitlindflem1  38079  matunitlindflem2  38080  poimirlem4  38087  poimirlem13  38096  poimirlem14  38097  poimirlem22  38105  poimirlem26  38109  poimirlem27  38110  heicant  38118  mblfinlem2  38121  mblfinlem3  38122  mblfinlem4  38123  cnambfre  38131  itg2addnclem  38134  itg2addnclem2  38135  itg2gt0cn  38138  ftc1cnnc  38155  ftc1anclem5  38160  ftc1anclem7  38162  ftc1anc  38164  equivtotbnd  38241  isbndx  38245  ssbnd  38251  heibor1lem  38272  rrncmslem  38295  islshpat  39605  lfl1dim  39709  lfl1dim2N  39710  lkrpssN  39751  glbconN  39965  hlhgt2  39977  3dim2  40056  3dim3  40057  islln3  40098  islvol5  40167  2lplnja  40207  dalem19  40270  isline4N  40365  2polssN  40503  lhpmatb  40619  4atex  40664  trlatn0  40760  cdlemf2  41150  dialss  41634  diaglbN  41643  diaintclN  41646  dibglbN  41754  dibintclN  41755  dihlsscpre  41822  dihglblem5aN  41880  dihglblem2aN  41881  dihglblem4  41885  dihatexv  41926  dihjat1lem  42016  lcfl6  42088  mapdval2N  42218  aks4d1p8  42668  fldhmf1  42671  primrootscoprmpow  42680  primrootscoprbij2  42684  primrootspoweq0  42687  evl1gprodd  42698  hashscontpow  42703  aks6d1c2lem4  42708  idomnnzgmulnz  42714  deg1gprod  42721  sticksstones8  42734  sticksstones12a  42738  aks6d1c6lem3  42753  aks6d1c6lem5  42758  aks6d1c7  42765  aks5lem5a  42772  unitscyglem2  42777  sn-0tie0  43037  imacrhmcl  43100  fiabv  43118  evlselv  43135  fsuppind  43136  prjspertr  43151  prjspreln0  43155  prjspner1  43172  elrfi  43239  eldioph2  43307  diophin  43317  irrapxlem2  43364  irrapxlem3  43365  irrapxlem4  43366  irrapxlem5  43367  pell1234qrne0  43394  pell1234qrreccl  43395  pell1234qrmulcl  43396  pell14qrgt0  43400  pell14qrdich  43410  pell1qrge1  43411  pellfundex  43427  congabseq  43515  jm2.27b  43547  jm2.27  43549  fnwe2lem2  43592  kelac1  43604  lnrfg  43660  hbt  43671  omabs2  43873  nadd1suc  43933  rfovcnvf1od  44544  ntrneiiso  44631  ntrneikb  44634  ntrneixb  44635  ntrneik3  44636  ntrneix3  44637  ntrneik13  44638  ntrneix13  44639  cvgdvgrat  44853  binomcxplemnotnn0  44896  sineq0ALT  45476  fnchoice  45573  disjf1  45725  supxrgere  45873  supxrgelem  45877  supxrge  45878  suplesup  45879  xralrple2  45894  infxr  45906  infleinflem2  45910  infleinf  45911  uzub  45969  mccl  46138  limcrecl  46169  lptioo2  46171  lptioo1  46172  lptre2pt  46178  addlimc  46186  limsupmnflem  46258  climxrre  46288  liminflimsupclim  46345  climxlim2lem  46383  xlimliminflimsup  46400  icccncfext  46425  cncfiooicclem1  46431  cncfiooiccre  46433  dvbdfbdioolem2  46467  ioodvbdlimc1lem1  46469  dvnxpaek  46480  dvmptfprodlem  46482  dvmptfprod  46483  dvnprodlem3  46486  itgioocnicc  46515  itgspltprt  46517  stoweidlem31  46569  fourierdlem39  46684  fourierdlem42  46687  fourierdlem48  46692  fourierdlem49  46693  fourierdlem50  46694  fourierdlem51  46695  fourierdlem64  46708  fourierdlem65  46709  fourierdlem74  46718  fourierdlem75  46719  fourierdlem81  46725  fourierdlem82  46726  fourierdlem101  46745  etransclem23  46795  etransclem27  46799  etransclem32  46804  etransclem33  46805  etransclem35  46807  etransclem38  46810  sge0tsms  46918  sge0cl  46919  sge0f1o  46920  sge0split  46947  sge0rpcpnf  46959  sge0seq  46984  nnfoctbdjlem  46993  iundjiun  46998  meaiuninc3v  47022  meaiininclem  47024  omeiunltfirp  47057  carageniuncllem2  47060  carageniuncl  47061  hoicvr  47086  hoidmv1lelem1  47129  hoidmvlelem3  47135  hoidmvlelem5  47137  hoidmvle  47138  hoiqssbllem3  47162  iunhoiioolem  47213  pimdecfgtioo  47255  pimincfltioo  47256  preimageiingt  47258  preimaleiinlt  47259  smflimlem4  47312  chnerlem1  47422  iccpartigtl  47993  iccpartgt  47997  sprsymrelf1lem  48061  paireqne  48081  proththd  48187  requad2  48209  sbgoldbst  48364  bgoldbtbndlem4  48394  isuspgrim0lem  48479  isuspgrim0  48480  isuspgrimlem  48481  gricushgr  48503  grimedg  48521  grimgrtri  48535  isubgr3stgrlem7  48558  gpgusgralem  48642  pgn4cyclex  48712  2zrngmmgm  48838  cznrng  48847  rhmsubcALTVlem4  48870  srhmsubcALTV  48911  lincsum  49015  lcoss  49022  snlindsntor  49057  islindeps2  49069  line2x  49340  line2y  49341  itscnhlinecirc02p  49371  discsubc  49649  imasubc3  49741  uppropd  49766  swapfval  49847  fucofvalg  49903  fuco21  49921  precofvalALT  49953  2arwcat  50185  lanup  50226  ranup  50227