Theorem ad3antrrr 743

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ad4antr  745  ad4antlr  746  simplll  787  fsnex  7291  fnwe2lem3  8149  fimaproj  8154  frxp3  8170  oaabs  8660  oaabs2  8661  omabs  8663  cofon1  8684  sbthlem8  9116  cantnfle  9675  cantnfp1  9685  cantnflem1c  9691  sornom  10358  enfin2i  10402  ttukeylem6  10595  fpwwe2lem12  10730  fpwwe2  10731  winalim2  10784  wuncval2  10835  negf1o  11749  xlemul1a  13421  difreicc  13618  flflp1  13950  faclbnd  14437  ccatf1  14739  swrdf1  14803  swrdswrd  14858  swrdccatin1  14878  pfxccatin12lem3  14885  swrdccat3blem  14892  sgnmul  15265  ello12  15688  lo1bdd2  15696  elo12  15699  rlimclim1  15717  rlimcld2  15750  o1co  15758  o1of2  15785  o1rlimmul  15791  rlimsqzlem  15821  isercoll  15840  o1fsum  15985  supcvg  16030  dvds2ln  16464  lcmgcdlem  16786  cncongr2  16848  isprm5  16888  prmdvdsncoprmbd  16908  pcadd  17072  vdwlem2  17165  vdwlem11  17174  sbcie3s  17345  prdsval  17631  mreexexlem4d  17826  isacs2  17832  catcocl  17864  catass  17865  subccocl  18025  fullsubc  18030  funcco  18051  funcpropd  18082  fullpropd  18102  ffthiso  18111  isnat  18130  natpropd  18159  fucpropd  18160  xpcval  18356  evlf2  18397  curfpropd  18412  curfuncf  18417  uncfcurf  18418  curf2ndf  18426  hofcl  18438  hofpropd  18446  yonffthlem  18461  isacs3lem  18721  acsfiindd  18732  chnind  18800  gsumpropd2lem  18873  resmgmhm2b  18907  resmhm2b  19023  mhmid  19278  mhmmnd  19279  ghmgrp  19281  conjnmzb  19472  ghmqusnsg  19501  ghmquskerlem3  19505  ghmqusker  19506  pgpfi  19824  sylow3lem2  19847  efgredlem  19966  frgpnabllem1  20092  imasabl  20095  dprdfcntz  20236  ablfac1b  20291  pgpfac1lem3  20298  pgpfac1lem5  20300  pgpfaclem3  20304  omndmul2  20352  gsumle  20364  ringinvnzdiv  20537  rnghmsubcsetclem2  20889  rhmsubcsetclem2  20918  srhmsubc  20937  rhmsubclem4  20945  imadrhmcl  21059  cntzsdrg  21064  suborng  21138  islmhm2  21318  lspsneleq  21398  drngidl  21544  rhmpreimaidl  21576  qsidomlem1  21641  prmidlsubm  21648  znunit  21874  psgndiflemB  21911  uvcff  22102  uvcf1  22103  lindfmm  22138  lindsenlbs  22162  sraassab  22181  psrval  22228  psrass1  22276  resspsrmul  22288  mplbas2  22356  evlsvvval  22407  mhpmulcl  22475  psdmul  22492  coe1tmmul  22601  gsummoncoe1  22631  evls1fpws  22692  dmatsubcl  22818  scmatscm  22833  smatvscl  22844  marrepval  22882  mdetdiaglem  22918  mdetunilem8  22939  mdetunilem9  22940  matunitlindflem1  22999  matunitlindflem2  23000  pmatcoe1fsupp  23024  decpmatmulsumfsupp  23096  pmatcollpw2lem  23100  mp2pm2mplem4  23132  pm2mpmhmlem1  23141  pm2mpmhmlem2  23142  pm2mp  23148  fvmptnn04if  23172  cpmadugsumfi  23200  cpmidg2sum  23203  cpmadumatpoly  23206  cayhamlem4  23211  neiptoptop  23454  neitr  23503  ordtrest2lem  23526  cnpnei  23587  iscncl  23592  cncls  23597  cnntr  23598  cncnp  23603  lmcnp  23627  isreg2  23700  hauscmplem  23729  cmpfi  23731  1stcfb  23768  1stcrest  23776  2ndcctbss  23779  2ndcomap  23782  islly2  23808  cldllycmp  23819  lly1stc  23820  locfincmp  23850  llycmpkgen2  23874  1stckgenlem  23877  kgencn2  23881  kgencn3  23882  ptbasfi  23905  ptpjopn  23936  txdis1cn  23959  txlly  23960  txnlly  23961  txtube  23964  txcmplem2  23966  tx1stc  23974  txkgen  23976  xkopt  23979  xkoco2cn  23982  xkococnlem  23983  xkococn  23984  xkoinjcn  24011  tgqtop  24036  regr1lem  24063  kqreglem1  24065  nrmhmph  24118  rnelfmlem  24276  rnelfm  24277  fmfnfmlem4  24281  fmfnfm  24282  ufldom  24286  flimopn  24299  hauspwpwf1  24311  fclsopn  24338  fclsnei  24343  fclsrest  24348  alexsublem  24368  alexsubALTlem3  24373  ptcmplem2  24377  ptcmplem3  24378  cnextfun  24388  cnextcn  24391  symgtgp  24430  tgpt0  24443  qustgpopn  24444  tsmsxplem1  24477  trust  24553  utopsnneiplem  24571  utop3cls  24575  utopreg  24576  isucn2  24602  cstucnd  24607  ucncn  24608  fmucnd  24615  cfilufg  24616  neipcfilu  24619  met2ndci  24846  prdsxmslem2  24853  metcnp3  24864  metustid  24878  metustexhalf  24880  metust  24882  psmetutop  24891  nmoleub  25055  reconnlem2  25152  xrge0tsms  25159  cncfco  25233  lebnumlem3  25289  lebnum  25290  nmoleub2lem2  25442  nmoleub3  25445  iscfil2  25592  iscau4  25605  iscmet3lem2  25618  equivcfil  25625  equivcau  25626  caubl  25634  rrxdstprj1  25735  ovolshftlem2  25836  ovolicc2lem4  25846  uniioombl  25915  i1fmulclem  26028  mbfi1fseqlem6  26046  itg2const2  26067  itg2split  26075  bddiblnc  26167  ellimc2  26202  ellimc3  26204  limcflf  26206  dvmptfsum  26300  dvferm1  26310  dvferm2  26312  dvlip2  26320  c1lip1  26322  lhop1  26339  ftc1a  26362  ply1divex  26460  plyeq0lem  26534  plymullem1  26538  coemullem  26574  coemulc  26579  ulmshftlem  26721  ulmcaulem  26726  ulmbdd  26730  ulmcn  26731  ulmdvlem3  26734  mtestbdd  26737  pserulm  26754  pserdvlem2  26760  abelthlem8  26771  xrlimcnp  27301  jensen  27321  lgamucov  27370  logfac2  27549  dchrelbas3  27570  dchrpt  27599  gausslemma2dlem1a  27697  lgsquad3  27719  2sqb  27764  rpvmasumlem  27819  dchrisumlem1  27821  dchrisumlem3  27823  dchrmusum2  27826  dchrvmasumlem2  27830  dchrisum0flblem1  27840  dchrisum0lem1b  27847  dchrisum0lem1  27848  dchrisum0  27852  mulog2sumlem2  27867  pntlem3  27941  ostth3  27970  fltoprmgt3  28001  lesrec  28190  cofcutr  28315  remulscllem2  28892  istrkgcb  28923  tgbtwndiff  28974  iscgrglt  28982  tgcgrxfr  28986  motcgrg  29012  lnext  29035  tgbtwnconn1  29043  tgbtwnconn3  29045  legval  29052  legtrid  29059  legso  29067  hlcgreu  29089  tglnne  29101  tglineeltr  29104  tglnne0  29114  colline  29123  tglowdim2l  29124  tglowdim2ln  29125  mirreu3  29131  mirbtwnhl  29157  krippenlem  29167  midexlem  29169  perpcom  29193  perpneq  29194  footexALT  29198  footex  29201  colperpexlem3  29213  colperpex  29214  opphllem  29216  midex  29218  oppne3  29224  opptgdim2  29226  oppnid  29227  opphllem2  29229  opphllem5  29232  opphllem6  29233  oppperpex  29234  outpasch  29238  hlpasch  29239  lnopp2hpgb  29246  hpgerlem  29248  colopp  29252  colhp  29253  plngrnssp  29262  lnincplng  29267  plngrotlem1  29270  plngrotlem2  29271  plngrotlem3  29272  lnssplnglem  29274  lmieu  29294  lnperpex  29314  trgcopy  29316  trgcopyeulem  29317  iscgra1  29322  cgrane1  29324  cgrane2  29325  cgrane3  29326  cgrane4  29327  cgrahl1  29328  cgrahl2  29329  cgracgr  29330  cgraswap  29332  cgracom  29334  cgratr  29335  zerocgra  29336  flatcgra  29337  cgrabtwn  29339  cgrahl  29340  sacgr  29344  acopyeu  29347  ragcgra  29348  tgaaddcpbllem1  29354  tgaaddcpbllem3  29356  tgaaddcpbl  29357  cgrg3col4  29377  angmgmaddeu1  29384  angmgmaddeu2  29385  angmgmaddeu3  29386  angmgmaddeu4  29387  angmgmaddeu5  29388  angmgmaddeu6  29389  angmgmaddeu7  29390  angmgmaddov2lem  29392  angmgmaddcpbl  29395  angmgmaddrid  29398  angmgm  29402  tgasa1  29408  prlnghpg  29429  dfprlng2  29430  perpprlng  29433  prlngex  29434  prlngmolem1  29435  prlngmolem2  29436  prlngplngtr  29442  prlngmid2  29444  quadcgrprlng  29449  f1otrg  29453  f1otrge  29454  axeuclidlem  29545  axcontlem2  29548  umgrvad2edg  29799  usgredg2vlem2  29812  pthdepisspth  30326  clwwlkccatlem  30585  clwlkclwwlklem2  30596  3cycld  30784  eupth2lems  30844  eucrctshift  30849  frgr3vlem2  30880  n4cyclfrgr  30897  numclwwlk1lem2f1  30963  numclwwlk2lem1  30982  ubthlem3  31479  chirredlem1  32997  chirredlem3  32999  cdj1i  33040  fnpreimac  33311  xrge0infss  33398  nn0xmulclb  33409  hashxpe  33445  2exple2exp  33471  ccatws1f1o  33560  dfmgc2lem  33602  mgcf1o  33610  mndlactf1  33633  mndlactfo  33634  mndractf1  33635  mndractfo  33636  gsumfs2d  33668  gsumhashmul  33674  suppgsumssiun  33679  xrge0tsmsd  33680  gsumwun  33683  psgnfzto1stlem  33707  cycpmco2  33740  cycpmrn  33750  tocyccntz  33751  cycpmconjslem2  33762  cyc3conja  33764  conjga  33777  submarchi  33793  isarchiofld  33806  elrgspnlem1  33849  elrgspnlem2  33850  elrgspnlem3  33851  elrgspnlem4  33852  elrgspnsubrunlem1  33854  elrgspnsubrunlem2  33855  elrgspnsubrun  33856  erlval  33865  erler  33872  rloccring  33878  rlocf1  33881  rlocisunit  33883  domnprodn0  33885  domnprodeq0  33886  subrdom  33892  imaslmod  33960  znfermltl  33968  lindfpropd  33983  unitprodclb  33990  nsgmgc  34009  nsgqusf1olem1  34010  unitpidl1  34020  elrspunidl  34024  elrspunsn  34025  rhmimaidl  34028  mxidlprm  34041  mxidlirredi  34042  drngmxidlr  34048  qsdrngilem  34064  qsdrngi  34065  drnglring  34070  dflringlem2  34073  dflring3  34075  dflring4  34076  rsprprmprmidl  34100  rsprprmprmidlb  34101  rprmasso2  34104  rprmirred  34109  rprmirredb  34110  rprmdvdspow  34111  1arithidom  34115  pidufd  34121  1arithufdlem3  34124  dfufd2  34128  deg1prod  34161  ply1dg3rt0irred  34162  0mplrim  34192  mplidomlem  34205  extvfvcl  34214  mplvrpmga  34223  mplvrpmmhm  34224  mplvrpmrhm  34225  psrgsum  34226  psrmonprod  34230  esplymhp  34246  esplyfval3  34250  esplyfval1  34251  esplyfvaln  34252  esplyind  34253  exsslsb  34275  lbslelsp  34276  ply1degltdimlem  34300  lindsunlem  34302  lindsun  34303  lbsdiflsp0  34304  dimkerim  34305  fedgmul  34309  dimlssid  34310  assalactf1o  34313  extdg1id  34344  evls1fldgencl  34348  fldextrspunlsplem  34351  fldextrspunlsp  34352  extdgfialglem1  34370  minplyirred  34389  fldext2chn  34406  cos9thpiminplylem2  34461  smatrcl  34474  1smat1  34482  submateq  34487  mdetpmtr1  34501  madjusmdetlem2  34506  locfinreflem  34518  cmppcmp  34536  rhmpreimacn  34563  ordtrest2NEWlem  34600  ordtconnlem1  34602  lmdvg  34631  zrhcntr  34657  esumpcvgval  34756  esum2d  34771  sigapildsys  34841  ldgenpisyslem1  34842  fiunelros  34853  volmeas  34910  imambfm  34940  omssubadd  34978  carsggect  34996  carsgclctunlem3  34998  signsply0  35226  signstres  35250  actfunsnf1o  35279  actfunsnrndisj  35280  reprsuc  35290  reprinfz1  35297  breprexplema  35305  breprexplemc  35307  breprexp  35308  breprexpnat  35309  circlemeth  35315  hgt750lemb  35331  tgoldbachgtd  35337  erdszelem8  36049  pconnconn  36082  cvmlift2lem12  36165  cvmlift3lem5  36174  cvmlift3lem7  36176  cvmlift3lem8  36177  fmla1  36238  mrsubrn  36364  msrval  36389  msubff1  36407  btwnconn1lem13  36956  elicc3  37197  neibastop2lem  37240  weiunfr  37347  unbdqndv2  37469  irrdifflemf  38339  ltflcei  38624  poimirlem4  38635  poimirlem13  38644  poimirlem14  38645  poimirlem22  38653  poimirlem26  38657  poimirlem27  38658  heicant  38666  mblfinlem2  38669  mblfinlem3  38670  mblfinlem4  38671  cnambfre  38679  itg2addnclem  38682  itg2addnclem2  38683  itg2gt0cn  38686  ftc1cnnc  38703  ftc1anclem5  38708  ftc1anclem7  38710  ftc1anc  38712  equivtotbnd  38805  isbndx  38809  ssbnd  38815  heibor1lem  38836  rrncmslem  38859  islshpat  40167  lfl1dim  40271  lfl1dim2N  40272  lkrpssN  40313  glbconN  40527  hlhgt2  40539  3dim2  40618  3dim3  40619  islln3  40660  islvol5  40729  2lplnja  40769  dalem19  40832  isline4N  40927  2polssN  41065  lhpmatb  41181  4atex  41226  trlatn0  41322  cdlemf2  41712  dialss  42196  diaglbN  42205  diaintclN  42208  dibglbN  42316  dibintclN  42317  dihlsscpre  42384  dihglblem5aN  42442  dihglblem2aN  42443  dihglblem4  42447  dihatexv  42488  dihjat1lem  42578  lcfl6  42650  mapdval2N  42780  aks4d1p8  43230  fldhmf1  43233  primrootscoprmpow  43242  primrootscoprbij2  43246  primrootspoweq0  43249  evl1gprodd  43260  hashscontpow  43265  aks6d1c2lem4  43270  idomnnzgmulnz  43276  deg1gprod  43283  sticksstones8  43296  sticksstones12a  43300  aks6d1c6lem3  43315  aks6d1c6lem5  43320  aks6d1c7  43327  aks5lem5a  43334  unitscyglem2  43339  sn-0tie0  43608  imacrhmcl  43674  fiabv  43693  evlselv  43710  fsuppind  43711  prjspertr  43726  prjspreln0  43730  elrfi  43798  eldioph2  43866  diophin  43876  irrapxlem2  43923  irrapxlem3  43924  irrapxlem4  43925  irrapxlem5  43926  pell1234qrne0  43953  pell1234qrreccl  43954  pell1234qrmulcl  43955  pell14qrgt0  43959  pell14qrdich  43969  pell1qrge1  43970  pellfundex  43986  congabseq  44074  jm2.27b  44106  jm2.27  44108  kelac1  44158  lnrfg  44214  hbt  44225  omabs2  44427  nadd1suc  44487  rfovcnvf1od  45097  ntrneiiso  45184  ntrneikb  45187  ntrneixb  45188  ntrneik3  45189  ntrneix3  45190  ntrneik13  45191  ntrneix13  45192  cvgdvgrat  45390  binomcxplemnotnn0  45433  sineq0ALT  46012  fnchoice  46139  disjf1  46291  supxrgere  46438  supxrgelem  46442  supxrge  46443  suplesup  46444  xralrple2  46459  infxr  46471  infleinflem2  46475  infleinf  46476  uzub  46534  mccl  46703  limcrecl  46734  lptioo2  46736  lptioo1  46737  lptre2pt  46743  addlimc  46751  limsupmnflem  46823  climxrre  46853  liminflimsupclim  46910  climxlim2lem  46948  xlimliminflimsup  46965  icccncfext  46990  cncfiooicclem1  46996  cncfiooiccre  46998  dvbdfbdioolem2  47032  ioodvbdlimc1lem1  47034  dvnxpaek  47045  dvmptfprodlem  47047  dvmptfprod  47048  dvnprodlem3  47051  itgioocnicc  47080  itgspltprt  47082  stoweidlem31  47134  fourierdlem39  47249  fourierdlem42  47252  fourierdlem48  47257  fourierdlem49  47258  fourierdlem50  47259  fourierdlem51  47260  fourierdlem64  47273  fourierdlem65  47274  fourierdlem74  47283  fourierdlem75  47284  fourierdlem81  47290  fourierdlem82  47291  fourierdlem101  47310  etransclem23  47360  etransclem27  47364  etransclem32  47369  etransclem33  47370  etransclem35  47372  etransclem38  47375  sge0tsms  47483  sge0cl  47484  sge0f1o  47485  sge0split  47512  sge0rpcpnf  47524  sge0seq  47549  nnfoctbdjlem  47558  iundjiun  47563  meaiuninc3v  47587  meaiininclem  47589  omeiunltfirp  47622  carageniuncllem2  47625  carageniuncl  47626  hoicvr  47651  hoidmv1lelem1  47694  hoidmvlelem3  47700  hoidmvlelem5  47702  hoidmvle  47703  hoiqssbllem3  47727  iunhoiioolem  47778  pimdecfgtioo  47820  pimincfltioo  47821  preimageiingt  47823  preimaleiinlt  47824  smflimlem4  47877  iccpartigtl  48598  iccpartgt  48602  sprsymrelf1lem  48666  paireqne  48686  proththd  48792  requad2  48814  sbgoldbst  48969  bgoldbtbndlem4  48999  isuspgrim0lem  49084  isuspgrim0  49085  isuspgrimlem  49086  gricushgr  49108  grimedg  49126  grimgrtri  49140  isubgr3stgrlem7  49163  gpgusgralem  49247  pgn4cyclex  49317  2zrngmmgm  49442  cznrng  49451  rhmsubcALTVlem4  49474  srhmsubcALTV  49515  lincsum  49634  lcoss  49641  snlindsntor  49676  islindeps2  49688  line2x  49959  line2y  49960  itscnhlinecirc02p  49990  inlinecirc02plem  49991  discsubc  50271  imasubc3  50365  uppropd  50390  swapfval  50477  fucofvalg  50533  fuco21  50551  precofvalALT  50596  2arwcat  50831  lanup  50917  ranup  50918