Theorem ad3antrrr 723

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

Syntax hints:   → wi 4   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  ad4antr  726  ad4antrOLD  727  ad4antlr  728  ad5ant12  768  simplll  793  simp-4r  805  fsnex  6794  oaabs  7992  oaabs2  7993  omabs  7995  undom  8318  sbthlem8  8347  findcard3  8473  cantnfle  8846  cantnfp1  8856  cantnflem1c  8862  sornom  9415  enfin2i  9459  ttukeylem6  9652  fpwwe2lem13  9780  fpwwe2  9781  winalim2  9834  wuncval2  9885  negf1o  10785  xlemul1a  12407  difreicc  12598  flflp1  12904  faclbnd  13371  swrdswrd  13785  swrdccatin12lem3  13831  swrdccat3blem  13842  ello12  14625  lo1bdd2  14633  elo12  14636  rlimclim1  14654  rlimcld2  14687  o1co  14695  o1of2  14721  o1rlimmul  14727  rlimsqzlem  14757  isercoll  14776  o1fsum  14920  supcvg  14963  dvds2ln  15392  lcmgcdlem  15693  cncongr2  15755  isprm5  15791  pcadd  15965  vdwlem2  16058  vdwlem11  16067  sbcie3s  16281  prdsval  16469  mreexexlem4d  16661  isacs2  16667  catcocl  16699  catass  16700  subccocl  16858  fullsubc  16863  funcco  16884  funcpropd  16913  fullpropd  16933  ffthiso  16942  isnat  16960  natpropd  16989  fucpropd  16990  xpcval  17171  evlf2  17212  curfpropd  17227  curfuncf  17232  uncfcurf  17233  curf2ndf  17241  hofcl  17253  hofpropd  17261  yonffthlem  17276  isacs3lem  17520  acsfiindd  17531  gsumpropd2lem  17627  resmhm2b  17715  mhmid  17891  mhmmnd  17892  ghmgrp  17894  conjnmzb  18047  pgpfi  18372  sylow3lem2  18395  efgredlem  18513  efgredlemOLD  18514  frgpnabllem1  18630  dprdfcntz  18769  ablfac1b  18824  pgpfac1lem3  18831  pgpfac1lem5  18833  pgpfaclem3  18837  ringinvnzdiv  18948  islmhm2  19398  lspsneleq  19475  psrval  19724  psrass1  19767  resspsrmul  19779  mplbas2  19832  coe1tmmul  20008  gsummoncoe1  20035  znunit  20272  psgndiflemB  20307  uvcff  20498  uvcf1  20499  lindfmm  20534  dmatsubcl  20673  scmatscm  20688  smatvscl  20699  marrepval  20737  mdetdiaglem  20773  mdetunilem8  20794  mdetunilem9  20795  pmatcoe1fsupp  20877  decpmatmulsumfsupp  20949  pmatcollpw2lem  20953  mp2pm2mplem4  20985  pm2mpmhmlem1  20994  pm2mpmhmlem2  20995  pm2mp  21001  fvmptnn04if  21025  cpmadugsumfi  21053  cpmidg2sum  21056  cpmadumatpoly  21059  cayhamlem4  21064  neiptoptop  21307  neitr  21356  ordtrest2lem  21379  cnpnei  21440  iscncl  21445  cncls  21450  cnntr  21451  cncnp  21456  lmcnp  21480  isreg2  21553  hauscmplem  21581  cmpfi  21583  1stcfb  21620  1stcrest  21628  2ndcctbss  21630  2ndcomap  21633  islly2  21659  cldllycmp  21670  lly1stc  21671  locfincmp  21701  llycmpkgen2  21725  1stckgenlem  21728  kgencn2  21732  kgencn3  21733  ptbasfi  21756  ptpjopn  21787  txdis1cn  21810  txlly  21811  txnlly  21812  txtube  21815  txcmplem2  21817  tx1stc  21825  txkgen  21827  xkopt  21830  xkoco2cn  21833  xkococnlem  21834  xkococn  21835  xkoinjcn  21862  tgqtop  21887  regr1lem  21914  kqreglem1  21916  nrmhmph  21969  rnelfmlem  22127  rnelfm  22128  fmfnfmlem4  22132  fmfnfm  22133  ufldom  22137  flimopn  22150  hauspwpwf1  22162  fclsopn  22189  fclsnei  22194  fclsrest  22199  alexsublem  22219  alexsubALTlem3  22224  ptcmplem2  22228  ptcmplem3  22229  cnextfun  22239  cnextcn  22242  symgtgp  22276  tgpt0  22293  qustgpopn  22294  tsmsxplem1  22327  trust  22404  utopsnneiplem  22422  utop3cls  22426  utopreg  22427  isucn2  22454  cstucnd  22459  ucncn  22460  fmucnd  22467  cfilufg  22468  neipcfilu  22471  met2ndci  22698  prdsxmslem2  22705  metcnp3  22716  metustid  22730  metustexhalf  22732  metust  22734  psmetutop  22743  nmoleub  22906  reconnlem2  23001  xrge0tsms  23008  cncfco  23081  lebnumlem3  23133  lebnum  23134  nmoleub2lem2  23286  nmoleub3  23289  iscfil2  23435  iscau4  23448  iscmet3lem2  23461  equivcfil  23468  equivcau  23469  caubl  23477  rrxdstprj1  23578  ovolshftlem2  23677  ovolicc2lem4  23687  uniioombl  23756  i1fmulclem  23869  mbfi1fseqlem6  23887  itg2const2  23908  itg2split  23916  ellimc2  24041  ellimc3  24043  limcflf  24045  dvmptfsum  24138  dvferm1  24148  dvferm2  24150  dvlip2  24158  c1lip1  24160  lhop1  24177  ftc1a  24200  ply1divex  24296  plyeq0lem  24366  plymullem1  24370  coemullem  24406  coemulc  24411  ulmshftlem  24543  ulmcaulem  24548  ulmbdd  24552  ulmcn  24553  ulmdvlem3  24556  mtestbdd  24559  pserulm  24576  pserdvlem2  24582  abelthlem8  24593  xrlimcnp  25109  jensen  25129  lgamucov  25178  logfac2  25356  dchrelbas3  25377  dchrpt  25406  gausslemma2dlem1a  25504  lgsquad3  25526  2sqb  25571  rpvmasumlem  25590  dchrisumlem1  25592  dchrisumlem3  25594  dchrmusum2  25597  dchrvmasumlem2  25601  dchrisum0flblem1  25611  dchrisum0lem1b  25618  dchrisum0lem1  25619  dchrisum0  25623  mulog2sumlem2  25638  pntlem3  25712  ostth3  25741  istrkgcb  25769  tgbtwndiff  25819  iscgrglt  25827  tgcgrxfr  25831  motcgrg  25857  lnext  25880  tgbtwnconn1  25888  tgbtwnconn3  25890  legval  25897  legtrid  25904  legso  25912  hlcgreu  25931  tglnne  25941  tglineeltr  25944  tglnne0  25953  colline  25962  tglowdim2l  25963  tglowdim2ln  25964  mirreu3  25967  mirbtwnhl  25993  krippenlem  26003  midexlem  26005  perpcom  26026  perpneq  26027  footex  26031  colperpexlem3  26042  colperpex  26043  opphllem  26045  midex  26047  oppne3  26053  opptgdim2  26055  oppnid  26056  opphllem2  26058  opphllem5  26061  opphllem6  26062  oppperpex  26063  outpasch  26065  hlpasch  26066  lnopp2hpgb  26073  hpgerlem  26075  colopp  26079  colhp  26080  lmieu  26094  lnperpex  26113  trgcopy  26114  trgcopyeulem  26115  iscgra1  26120  cgrane1  26122  cgrane2  26123  cgrane3  26124  cgrane4  26125  cgrahl1  26126  cgrahl2  26127  cgracgr  26128  cgraswap  26130  cgracom  26132  cgratr  26133  cgrabtwn  26135  cgrahl  26136  sacgr  26140  sacgrOLD  26141  acopyeu  26144  cgrg3col4  26153  tgasa1  26158  f1otrg  26171  f1otrge  26172  axeuclidlem  26262  axcontlem2  26265  umgrvad2edg  26510  usgredg2vlem2  26523  pthdepisspth  27038  clwwlkccatlem  27319  clwlkclwwlklem2  27330  clwlksf1clwwlkOLD  27446  3cycld  27555  eupth2lems  27616  eucrctshift  27621  frgr3vlem2  27656  n4cyclfrgr  27673  numclwwlk1lem2f1  27749  numclwwlk1lem2f1OLD  27754  numclwwlk2lem1  27780  numclwwlk2lem1OLD  27791  ubthlem3  28284  chirredlem1  29805  chirredlem3  29807  cdj1i  29848  xrge0infss  30073  omndmul2  30258  submarchi  30286  gsumle  30325  xrge0tsmsd  30331  suborng  30361  isarchiofld  30363  psgnfzto1stlem  30396  fzto1st1  30398  smatrcl  30408  1smat1  30416  submateq  30421  mdetpmtr1  30435  madjusmdetlem2  30440  fimaproj  30446  locfinreflem  30453  cmppcmp  30471  ordtrest2NEWlem  30514  ordtconnlem1  30516  lmdvg  30545  esumpcvgval  30686  esum2d  30701  sigapildsys  30771  ldgenpisyslem1  30772  fiunelros  30783  volmeas  30840  imambfm  30870  omssubadd  30908  carsggect  30926  carsgclctunlem3  30928  sgnmul  31151  signsply0  31176  signstres  31201  actfunsnf1o  31232  actfunsnrndisj  31233  reprsuc  31243  reprinfz1  31250  breprexplema  31258  breprexplemc  31260  breprexp  31261  breprexpnat  31262  circlemeth  31268  hgt750lemb  31284  tgoldbachgtd  31290  erdszelem8  31727  pconnconn  31760  cvmlift2lem12  31843  cvmlift3lem5  31852  cvmlift3lem7  31854  cvmlift3lem8  31855  mrsubrn  31957  msrval  31982  msubff1  32000  slerec  32463  btwnconn1lem13  32746  elicc3  32851  neibastop2lem  32894  unbdqndv2  33035  ltflcei  33941  lindsenlbs  33949  matunitlindflem1  33950  matunitlindflem2  33951  poimirlem4  33958  poimirlem13  33967  poimirlem14  33968  poimirlem22  33976  poimirlem26  33980  poimirlem27  33981  heicant  33989  mblfinlem2  33992  mblfinlem3  33993  mblfinlem4  33994  cnambfre  34002  itg2addnclem  34005  itg2addnclem2  34006  itg2gt0cn  34009  bddiblnc  34024  ftc1cnnc  34028  ftc1anclem5  34033  ftc1anclem7  34035  ftc1anc  34037  equivtotbnd  34120  isbndx  34124  ssbnd  34130  heibor1lem  34151  rrncmslem  34174  islshpat  35093  lfl1dim  35197  lfl1dim2N  35198  lkrpssN  35239  glbconN  35453  hlhgt2  35465  3dim2  35544  3dim3  35545  islln3  35586  islvol5  35655  2lplnja  35695  dalem19  35758  isline4N  35853  2polssN  35991  lhpmatb  36107  4atex  36152  trlatn0  36248  cdlemf2  36638  dialss  37122  diaglbN  37131  diaintclN  37134  dibglbN  37242  dibintclN  37243  dihlsscpre  37310  dihglblem5aN  37368  dihglblem2aN  37369  dihglblem4  37373  dihatexv  37414  dihjat1lem  37504  lcfl6  37576  mapdval2N  37706  elrfi  38102  eldioph2  38170  diophin  38181  irrapxlem2  38232  irrapxlem3  38233  irrapxlem4  38234  irrapxlem5  38235  pell1234qrne0  38262  pell1234qrreccl  38263  pell1234qrmulcl  38264  pell14qrgt0  38268  pell14qrdich  38278  pell1qrge1  38279  pellfundex  38295  congabseq  38385  jm2.27b  38417  jm2.27  38419  fnwe2lem2  38465  kelac1  38477  lnrfg  38533  hbt  38544  cntzsdrg  38616  rfovcnvf1od  39139  ntrneiiso  39230  ntrneikb  39233  ntrneixb  39234  ntrneik3  39235  ntrneix3  39236  ntrneik13  39237  ntrneix13  39238  cvgdvgrat  39353  binomcxplemnotnn0  39396  sineq0ALT  39992  disjf1  40178  supxrgere  40347  supxrgelem  40351  supxrge  40352  suplesup  40353  xralrple2  40368  infxr  40381  infleinflem2  40385  infleinf  40386  uzub  40454  mccl  40626  limcrecl  40657  lptioo2  40659  lptioo1  40660  lptre2pt  40668  addlimc  40676  limsupmnflem  40748  climxrre  40778  liminflimsupclim  40835  climxlim2lem  40867  icccncfext  40896  cncfiooicclem1  40902  cncfiooiccre  40904  dvbdfbdioolem2  40940  ioodvbdlimc1lem1  40942  dvnxpaek  40953  dvmptfprodlem  40955  dvmptfprod  40956  dvnprodlem3  40959  itgioocnicc  40988  itgspltprt  40990  stoweidlem31  41043  fourierdlem39  41158  fourierdlem42  41161  fourierdlem48  41166  fourierdlem49  41167  fourierdlem50  41168  fourierdlem51  41169  fourierdlem64  41182  fourierdlem65  41183  fourierdlem74  41192  fourierdlem75  41193  fourierdlem81  41199  fourierdlem82  41200  fourierdlem101  41219  etransclem23  41269  etransclem27  41273  etransclem32  41278  etransclem33  41279  etransclem35  41281  etransclem38  41284  sge0tsms  41389  sge0cl  41390  sge0f1o  41391  sge0split  41418  sge0rpcpnf  41430  sge0seq  41455  nnfoctbdjlem  41464  iundjiun  41469  meaiuninc3v  41493  meaiininclem  41495  omeiunltfirp  41528  carageniuncllem2  41531  carageniuncl  41532  hoidmv1lelem1  41600  hoidmvlelem3  41606  hoidmvlelem5  41608  hoidmvle  41609  hoiqssbllem3  41633  iunhoiioolem  41684  pimdecfgtioo  41722  pimincfltioo  41723  preimageiingt  41725  preimaleiinlt  41726  smflimlem4  41777  iccpartigtl  42248  iccpartgt  42252  proththd  42362  sbgoldbst  42497  bgoldbtbndlem4  42527  isomushgr  42545  isomuspgrlem2d  42550  sprsymrelf1lem  42589  resmgmhm2b  42648  2zrngmmgm  42794  cznrng  42803  rnghmsubcsetclem2  42824  rhmsubcsetclem2  42870  srhmsubc  42924  rhmsubclem4  42937  srhmsubcALTV  42942  rhmsubcALTVlem4  42955  lincsum  43066  lcoss  43073  snlindsntor  43108  islindeps2  43120  line2x  43307  line2y  43308