Theorem ad3antrrr 728

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

Syntax hints:   → wi 4   ∧ wa 398

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 399

This theorem is referenced by:  ad4antr  730  ad4antlr  731  ad5ant12  754  simplll  773  fsnex  7039  fimaproj  7829  oaabs  8271  oaabs2  8272  omabs  8274  undom  8605  sbthlem8  8634  findcard3  8761  cantnfle  9134  cantnfp1  9144  cantnflem1c  9150  sornom  9699  enfin2i  9743  ttukeylem6  9936  fpwwe2lem13  10064  winalim2  10118  wuncval2  10169  negf1o  11070  xlemul1a  12682  difreicc  12871  flflp1  13178  faclbnd  13651  swrdswrd  14067  pfxccatin12lem3  14094  swrdccat3blem  14101  ello12  14873  elo12  14884  rlimclim1  14902  rlimcld2  14935  o1co  14943  o1of2  14969  o1rlimmul  14975  rlimsqzlem  15005  isercoll  15024  o1fsum  15168  supcvg  15211  dvds2ln  15642  lcmgcdlem  15950  cncongr2  16012  isprm5  16051  pcadd  16225  vdwlem2  16318  vdwlem11  16327  sbcie3s  16541  prdsval  16728  mreexexlem4d  16918  isacs2  16924  catcocl  16956  catass  16957  subccocl  17115  fullsubc  17120  funcco  17141  fullpropd  17190  ffthiso  17199  isnat  17217  natpropd  17246  fucpropd  17247  xpcval  17427  evlf2  17468  curfpropd  17483  curfuncf  17488  uncfcurf  17489  hofcl  17509  hofpropd  17517  yonffthlem  17532  isacs3lem  17776  acsfiindd  17787  gsumpropd2lem  17889  resmhm2b  17987  mhmid  18220  mhmmnd  18221  ghmgrp  18223  conjnmzb  18393  pgpfi  18730  sylow3lem2  18753  efgredlem  18873  frgpnabllem1  18993  dprdfcntz  19137  ablfac1b  19192  pgpfac1lem3  19199  pgpfac1lem5  19201  pgpfaclem3  19205  ringinvnzdiv  19343  cntzsdrg  19581  islmhm2  19810  lspsneleq  19887  psrval  20142  psrass1  20185  resspsrmul  20197  mplbas2  20251  coe1tmmul  20445  gsummoncoe1  20472  znunit  20710  psgndiflemB  20744  uvcff  20935  uvcf1  20936  lindfmm  20971  dmatsubcl  21107  scmatscm  21122  smatvscl  21133  marrepval  21171  mdetdiaglem  21207  mdetunilem8  21228  mdetunilem9  21229  pmatcoe1fsupp  21309  decpmatmulsumfsupp  21381  pmatcollpw2lem  21385  mp2pm2mplem4  21417  pm2mpmhmlem1  21426  pm2mpmhmlem2  21427  pm2mp  21433  fvmptnn04if  21457  cpmadugsumfi  21485  cpmidg2sum  21488  cpmadumatpoly  21491  cayhamlem4  21496  neiptoptop  21739  neitr  21788  ordtrest2lem  21811  cnpnei  21872  iscncl  21877  cncls  21882  cnntr  21883  cncnp  21888  lmcnp  21912  isreg2  21985  hauscmplem  22014  cmpfi  22016  1stcfb  22053  1stcrest  22061  2ndcctbss  22063  2ndcomap  22066  islly2  22092  cldllycmp  22103  lly1stc  22104  locfincmp  22134  llycmpkgen2  22158  1stckgenlem  22161  kgencn2  22165  kgencn3  22166  ptbasfi  22189  ptpjopn  22220  txdis1cn  22243  txlly  22244  txnlly  22245  txtube  22248  txcmplem2  22250  tx1stc  22258  txkgen  22260  xkopt  22263  xkoco2cn  22266  xkococnlem  22267  xkococn  22268  xkoinjcn  22295  tgqtop  22320  regr1lem  22347  kqreglem1  22349  nrmhmph  22402  rnelfmlem  22560  rnelfm  22561  fmfnfmlem4  22565  fmfnfm  22566  ufldom  22570  flimopn  22583  hauspwpwf1  22595  fclsopn  22622  fclsnei  22627  fclsrest  22632  alexsublem  22652  alexsubALTlem3  22657  ptcmplem2  22661  ptcmplem3  22662  cnextfun  22672  cnextcn  22675  symgtgp  22714  tgpt0  22727  qustgpopn  22728  tsmsxplem1  22761  trust  22838  utopsnneiplem  22856  utop3cls  22860  utopreg  22861  isucn2  22888  cstucnd  22893  ucncn  22894  fmucnd  22901  cfilufg  22902  neipcfilu  22905  met2ndci  23132  prdsxmslem2  23139  metustid  23164  metustexhalf  23166  metust  23168  psmetutop  23177  nmoleub  23340  reconnlem2  23435  xrge0tsms  23442  cncfco  23515  lebnumlem3  23567  lebnum  23568  nmoleub2lem2  23720  nmoleub3  23723  iscfil2  23869  iscau4  23882  iscmet3lem2  23895  equivcfil  23902  equivcau  23903  caubl  23911  rrxdstprj1  24012  ovolshftlem2  24111  ovolicc2lem4  24121  uniioombl  24190  i1fmulclem  24303  mbfi1fseqlem6  24321  itg2const2  24342  itg2split  24350  ellimc2  24475  ellimc3  24477  limcflf  24479  dvmptfsum  24572  dvferm1  24582  dvferm2  24584  dvlip2  24592  c1lip1  24594  lhop1  24611  ftc1a  24634  ply1divex  24730  plyeq0lem  24800  plymullem1  24804  coemullem  24840  coemulc  24845  ulmshftlem  24977  ulmcaulem  24982  ulmbdd  24986  ulmcn  24987  ulmdvlem3  24990  mtestbdd  24993  pserulm  25010  pserdvlem2  25016  abelthlem8  25027  xrlimcnp  25546  jensen  25566  lgamucov  25615  logfac2  25793  dchrelbas3  25814  dchrpt  25843  gausslemma2dlem1a  25941  lgsquad3  25963  2sqb  26008  rpvmasumlem  26063  dchrisumlem1  26065  dchrisumlem3  26067  dchrmusum2  26070  dchrvmasumlem2  26074  dchrisum0flblem1  26084  dchrisum0lem1b  26091  dchrisum0lem1  26092  dchrisum0  26096  mulog2sumlem2  26111  pntlem3  26185  ostth3  26214  istrkgcb  26242  tgbtwndiff  26292  iscgrglt  26300  tgcgrxfr  26304  motcgrg  26330  lnext  26353  tgbtwnconn1  26361  tgbtwnconn3  26363  legval  26370  legtrid  26377  legso  26385  hlcgreu  26404  tglnne  26414  tglineeltr  26417  tglnne0  26426  colline  26435  tglowdim2l  26436  tglowdim2ln  26437  mirreu3  26440  mirbtwnhl  26466  krippenlem  26476  midexlem  26478  perpcom  26499  footexALT  26504  footex  26507  colperpexlem3  26518  colperpex  26519  opphllem  26521  midex  26523  oppne3  26529  opptgdim2  26531  oppnid  26532  opphllem2  26534  opphllem5  26537  opphllem6  26538  oppperpex  26539  outpasch  26541  hlpasch  26542  lnopp2hpgb  26549  hpgerlem  26551  colopp  26555  colhp  26556  lmieu  26570  lnperpex  26589  trgcopy  26590  trgcopyeulem  26591  iscgra1  26596  cgrane1  26598  cgrane2  26599  cgrane3  26600  cgrane4  26601  cgrahl1  26602  cgrahl2  26603  cgracgr  26604  cgraswap  26606  cgracom  26608  cgratr  26609  flatcgra  26610  cgrabtwn  26612  cgrahl  26613  sacgr  26617  acopyeu  26620  cgrg3col4  26639  tgasa1  26644  f1otrg  26657  f1otrge  26658  axeuclidlem  26748  axcontlem2  26751  umgrvad2edg  26995  usgredg2vlem2  27008  pthdepisspth  27516  clwwlkccatlem  27767  clwlkclwwlklem2  27778  3cycld  27957  eupth2lems  28017  eucrctshift  28022  frgr3vlem2  28053  n4cyclfrgr  28070  numclwwlk1lem2f1  28136  numclwwlk2lem1  28155  ubthlem3  28649  chirredlem1  30167  chirredlem3  30169  cdj1i  30210  fnpreimac  30416  xrge0infss  30484  nn0xmulclb  30496  hashxpe  30529  ccatf1  30625  swrdf1  30630  xrge0tsmsd  30692  omndmul2  30713  gsumle  30725  psgnfzto1stlem  30742  cycpmco2  30775  cycpmrn  30785  tocyccntz  30786  cycpmconjslem2  30797  cyc3conja  30799  submarchi  30815  suborng  30888  isarchiofld  30890  imaslmod  30922  lindfpropd  30942  qsidomlem1  30965  mxidlprm  30977  lindsunlem  31020  lindsun  31021  lbsdiflsp0  31022  dimkerim  31023  fedgmul  31027  extdg1id  31053  smatrcl  31061  1smat1  31069  submateq  31074  mdetpmtr1  31088  madjusmdetlem2  31093  locfinreflem  31104  cmppcmp  31122  ordtrest2NEWlem  31165  ordtconnlem1  31167  lmdvg  31196  esumpcvgval  31337  esum2d  31352  sigapildsys  31421  ldgenpisyslem1  31422  fiunelros  31433  volmeas  31490  imambfm  31520  omssubadd  31558  carsggect  31576  carsgclctunlem3  31578  sgnmul  31800  signsply0  31821  signstres  31845  actfunsnf1o  31875  actfunsnrndisj  31876  reprsuc  31886  reprinfz1  31893  breprexplema  31901  breprexplemc  31903  breprexp  31904  breprexpnat  31905  circlemeth  31911  hgt750lemb  31927  tgoldbachgtd  31933  erdszelem8  32445  pconnconn  32478  cvmlift2lem12  32561  cvmlift3lem5  32570  cvmlift3lem7  32572  cvmlift3lem8  32573  mrsubrn  32760  msrval  32785  msubff1  32803  slerec  33277  btwnconn1lem13  33560  elicc3  33665  neibastop2lem  33708  unbdqndv2  33850  ltflcei  34895  lindsenlbs  34902  matunitlindflem1  34903  matunitlindflem2  34904  poimirlem4  34911  poimirlem13  34920  poimirlem14  34921  poimirlem22  34929  poimirlem26  34933  poimirlem27  34934  heicant  34942  mblfinlem2  34945  mblfinlem3  34946  mblfinlem4  34947  cnambfre  34955  itg2addnclem  34958  itg2addnclem2  34959  itg2gt0cn  34962  bddiblnc  34977  ftc1cnnc  34981  ftc1anclem5  34986  ftc1anclem7  34988  ftc1anc  34990  equivtotbnd  35071  isbndx  35075  ssbnd  35081  heibor1lem  35102  rrncmslem  35125  islshpat  36168  lfl1dim  36272  lfl1dim2N  36273  lkrpssN  36314  glbconN  36528  hlhgt2  36540  3dim2  36619  3dim3  36620  islln3  36661  islvol5  36730  2lplnja  36770  dalem19  36833  isline4N  36928  2polssN  37066  lhpmatb  37182  4atex  37227  trlatn0  37323  cdlemf2  37713  dialss  38197  diaglbN  38206  diaintclN  38209  dibglbN  38317  dibintclN  38318  dihlsscpre  38385  dihglblem5aN  38443  dihglblem2aN  38444  dihglblem4  38448  dihatexv  38489  dihjat1lem  38579  lcfl6  38651  mapdval2N  38781  prjspertr  39304  prjspreln0  39308  elrfi  39340  eldioph2  39408  diophin  39418  irrapxlem2  39469  irrapxlem3  39470  irrapxlem4  39471  irrapxlem5  39472  pell1234qrne0  39499  pell1234qrreccl  39500  pell1234qrmulcl  39501  pell14qrgt0  39505  pell14qrdich  39515  pell1qrge1  39516  pellfundex  39532  congabseq  39620  jm2.27b  39652  jm2.27  39654  fnwe2lem2  39700  kelac1  39712  lnrfg  39768  hbt  39779  rfovcnvf1od  40399  ntrneiiso  40490  ntrneikb  40493  ntrneixb  40494  ntrneik3  40495  ntrneix3  40496  ntrneik13  40497  ntrneix13  40498  cvgdvgrat  40694  binomcxplemnotnn0  40737  sineq0ALT  41320  disjf1  41492  supxrgere  41650  supxrgelem  41654  supxrge  41655  suplesup  41656  xralrple2  41671  infxr  41684  infleinflem2  41688  infleinf  41689  uzub  41754  mccl  41928  limcrecl  41959  lptioo2  41961  lptioo1  41962  lptre2pt  41970  addlimc  41978  limsupmnflem  42050  climxrre  42080  liminflimsupclim  42137  climxlim2lem  42175  xlimliminflimsup  42192  icccncfext  42219  cncfiooicclem1  42225  cncfiooiccre  42227  dvbdfbdioolem2  42263  ioodvbdlimc1lem1  42265  dvnxpaek  42276  dvmptfprodlem  42278  dvmptfprod  42279  dvnprodlem3  42282  itgioocnicc  42311  itgspltprt  42313  stoweidlem31  42365  fourierdlem39  42480  fourierdlem42  42483  fourierdlem48  42488  fourierdlem49  42489  fourierdlem50  42490  fourierdlem51  42491  fourierdlem64  42504  fourierdlem65  42505  fourierdlem74  42514  fourierdlem75  42515  fourierdlem81  42521  fourierdlem82  42522  fourierdlem101  42541  etransclem23  42591  etransclem27  42595  etransclem32  42600  etransclem33  42601  etransclem35  42603  etransclem38  42606  sge0tsms  42711  sge0cl  42712  sge0f1o  42713  sge0split  42740  sge0rpcpnf  42752  sge0seq  42777  nnfoctbdjlem  42786  iundjiun  42791  meaiuninc3v  42815  meaiininclem  42817  omeiunltfirp  42850  carageniuncllem2  42853  carageniuncl  42854  hoidmv1lelem1  42922  hoidmvlelem3  42928  hoidmvlelem5  42930  hoidmvle  42931  hoiqssbllem3  42955  iunhoiioolem  43006  pimdecfgtioo  43044  pimincfltioo  43045  preimageiingt  43047  preimaleiinlt  43048  smflimlem4  43099  iccpartigtl  43632  iccpartgt  43636  sprsymrelf1lem  43702  paireqne  43722  proththd  43828  requad2  43837  sbgoldbst  43992  bgoldbtbndlem4  44022  isomushgr  44040  isomuspgrlem2d  44045  resmgmhm2b  44116  2zrngmmgm  44266  cznrng  44275  rnghmsubcsetclem2  44296  rhmsubcsetclem2  44342  srhmsubc  44396  rhmsubclem4  44409  srhmsubcALTV  44414  rhmsubcALTVlem4  44427  lincsum  44533  lcoss  44540  snlindsntor  44575  islindeps2  44587  line2x  44790  line2y  44791  itscnhlinecirc02p  44821