Theorem adantr 270

Description: Inference adding a conjunct to the right of an antecedent. (Contributed by NM, 30-Aug-1993.)

Hypothesis

Ref	Expression
adantr.1	|- ( ph -> ps )

Assertion

Ref	Expression
adantr	|- ( ( ph /\ ch ) -> ps )

Proof of Theorem adantr

Step	Hyp	Ref	Expression
1		adantr.1	. . 3 |- ( ph -> ps )
2	1	a1d 22	. 2 |- ( ph -> ( ch -> ps ) )
3	2	imp 122	1 |- ( ( ph /\ ch ) -> ps )

Syntax hints:   -> wi 4   /\ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105

This theorem is referenced by:  adantl  271  anim12ii  335  sylan9bb  449  ad2antrr  471  ad2antlr  472  ad2antrl  473  ad3antrrr  475  ad3antlr  476  ad4antr  477  ad4antlr  478  ad5antr  479  ad5antlr  480  ad6antr  481  ad6antlr  482  ad7antr  483  ad7antlr  484  ad8antr  485  ad8antlr  486  ad9antr  487  ad9antlr  488  ad10antr  489  ad10antlr  490  simp-4l  507  simp-4r  508  simp-5l  509  simp-5r  510  simp-6l  511  simp-6r  512  simp-7l  513  simp-7r  514  simp-8l  515  simp-8r  516  simp-9l  517  simp-9r  518  simp-10l  519  simp-10r  520  simp-11l  521  simp-11r  522  im2anan9  562  bi2bian9  572  jaao  671  ordi  762  con1bidc  801  con1bdc  805  pm5.18dc  810  dfandc  811  pm4.54dc  838  stabtestimpdc  857  orandc  880  ccase2  907  simpl1  941  simpl2  942  simpl3  943  3ad2ant1  959  3ad2ant2  960  simpll1  977  simpll2  978  simpll3  979  simplr1  980  simplr2  981  simplr3  982  simpl1l  989  simpl1r  990  simpl2l  991  simpl2r  992  simpl3l  993  simpl3r  994  simpl11  1013  simpl12  1014  simpl13  1015  simpl21  1016  simpl22  1017  simpl23  1018  simpl31  1019  simpl32  1020  simpl33  1021  xorbin  1315  biassdc  1326  bilukdc  1327  sbequi  1760  nfsbxyt  1860  euan  1997  datisi  2051  fresison  2059  ralbid  2366  rexbid  2367  ralimdv  2430  reubidv  2537  rmobidv  2542  rabbidv  2593  elex22  2614  gencbvex  2645  rspct  2694  ceqsrexbv  2726  elrabf  2747  eueq3dc  2766  reu6  2781  reuind  2795  csbcomg  2929  csbiebt  2942  eldif  2982  sseq1  3020  undif3ss  3225  difrab  3238  ifcldcd  3381  disjpr2  3456  diftpsn3  3527  preqr1g  3558  nfopd  3587  eluni  3604  dfnfc2  3619  iuneq12d  3702  iuneq2d  3703  disjeq12d  3775  disjxsn  3783  mpteq12dv  3860  mpteq2dv  3869  trel  3882  csbexga  3906  opexg  3983  opm  3989  copsexg  3999  euotd  4009  elopab  4013  epelg  4045  sotritrieq  4080  frirrg  4105  wepo  4114  alxfr  4211  rexxfrd  4213  op1stbg  4228  ordelsuc  4249  onsucelsucr  4252  onintonm  4261  onsucelsucexmidlem  4272  reg2exmidlema  4277  en2lp  4297  preleq  4298  opthreg  4299  ordsuc  4306  onsucuni2  4307  onintexmid  4315  wetriext  4319  reg3exmidlemwe  4321  peano5  4339  poinxp  4427  sosng  4431  eqrelrdv2  4457  xpsspw  4468  relopabi  4481  opeliunxp2  4494  relop  4504  opeldmg  4558  xpid11m  4575  riinint  4611  asymref  4730  xpidtr  4735  ssxpbm  4776  ssxp1  4777  ssxp2  4778  xpexr2m  4782  rnpropg  4820  elxp4  4828  elxp5  4829  funeu  4946  funun  4964  fununi  4987  funimaexglem  5002  funfni  5019  fneu  5023  fco  5076  funssxp  5080  feu  5092  fimacnvdisj  5094  f1ss  5117  f1ssr  5118  f1ssres  5119  f1imacnv  5163  foimacnv  5164  fun11iun  5167  f1o00  5181  nffvd  5207  fnbrfvb  5235  fvelrnb  5242  fvelimab  5250  ssimaex  5255  fvopab3g  5266  fvmptssdm  5276  fvmpt2d  5278  fvmptdf  5279  eqfnfv  5286  fndmdif  5293  fndmin  5295  fneqeql2  5297  fvimacnv  5303  ffvelrn  5321  dff3im  5333  dffo3  5335  fmptco  5351  fcompt  5354  fsn2  5358  fprg  5367  fvunsng  5378  fsnunres  5385  resfunexg  5403  fnex  5404  f1ocnvfv1  5437  f1ocnvfv2  5438  foeqcnvco  5450  f1eqcocnv  5451  fliftf  5459  fliftval  5460  isocnv  5471  isocnv2  5472  isores3  5475  isoini  5477  isoini2  5478  isoselem  5479  riotaexg  5492  riota2df  5508  acexmid  5531  oprabid  5557  0neqopab  5570  mpt2eq123dv  5587  cbvmpt2x  5602  eloprabga  5611  ovmpt2dxf  5646  ovmpt2df  5652  ov6g  5658  oprssov  5662  caovord3  5694  caovimo  5714  grprinvlem  5715  grprinvd  5716  f1opw2  5726  suppssfv  5728  suppssov1  5729  fnofval  5741  off  5744  offval2  5746  ofrfval2  5747  ofc12  5751  caofref  5752  caofinvl  5753  caofrss  5755  caoftrn  5756  fnexALT  5760  iunexg  5766  offval3  5781  f1stres  5806  elxp6  5816  elxp7  5817  unielxp  5820  xpopth  5822  op1steq  5825  releldm2  5831  dfoprab4  5838  fmpt2x  5846  1stconst  5862  2ndconst  5863  cnvf1o  5866  f1o2ndf1  5869  f1od2  5876  mpt2xopoveq  5878  isprmpt2  5881  brtpos2  5889  smores2  5932  iordsmo  5935  smoiso  5940  tfrlem1  5946  tfrlem3a  5948  tfrlem4  5952  tfrlem8  5957  tfrlemisucaccv  5962  tfrlemiubacc  5967  tfrlemi1  5969  tfri3  5976  rdgivallem  5991  rdgon  5996  frecrdg  6015  freccl  6016  sucinc2  6049  oav2  6066  oaword1  6073  nnmcl  6083  nndi  6088  nntri2or2  6099  nnaordi  6104  nnaword  6107  nnmordi  6112  nnmord  6113  nnaordex  6123  nnawordex  6124  nnm00  6125  ersymb  6143  erref  6149  iserd  6155  erth  6173  erinxp  6203  qliftel  6209  qliftfun  6211  eroveu  6220  eroprf  6222  th3qlem1  6231  ecovass  6238  ecoviass  6239  dom2lem  6275  ssdomg  6281  fundmen  6309  cnven  6311  fndmeng  6312  xpsnen  6318  xpdom2  6328  fopwdom  6333  phplem2  6339  nneneq  6343  nndomo  6350  phpm  6351  fidifsnen  6355  infiexmid  6362  dif1en  6364  php5fin  6366  fin0  6369  fin0or  6370  findcard2  6373  findcard2s  6374  findcard2d  6375  findcard2sd  6376  diffisn  6377  diffifi  6378  en2eqpr  6380  fientri3  6381  onunsnss  6383  unsnfi  6384  unsnfidcex  6385  unsnfidcel  6386  snon0  6387  fnfi  6388  relcnvfi  6391  f1dmvrnfibi  6393  supelti  6415  supsnti  6418  supisolem  6421  infglbti  6438  ordiso2  6446  ordiso  6447  carden2bex  6458  pr2ne  6461  elni2  6504  mulclpi  6518  addasspig  6520  mulasspig  6522  mulcanpig  6525  ltexpi  6527  ltapig  6528  ltmpig  6529  indpi  6532  enqeceq  6549  addcmpblnq  6557  dmaddpqlem  6567  distrnqg  6577  mulidnq  6579  ltsonq  6588  ltexnqq  6598  subhalfnqq  6604  ltbtwnnqq  6605  ltbtwnnq  6606  archnqq  6607  ltrnqg  6610  enq0sym  6622  enq0tr  6624  enq0eceq  6627  nqnq0pi  6628  nqnq0  6631  addcmpblnq0  6633  mulnnnq0  6640  nqpnq0nq  6643  nqnq0a  6644  nqnq0m  6645  nq0m0r  6646  distrnq0  6649  addassnq0  6652  nq02m  6655  preqlu  6662  prubl  6676  prloc  6681  prarloclemlt  6683  prarloclemn  6689  prarloc  6693  prarloc2  6694  genpml  6707  genpmu  6708  genpcdl  6709  genpcuu  6710  genprndl  6711  genprndu  6712  genpassl  6714  genpassu  6715  addlocprlemeq  6723  addlocprlemgt  6724  addlocpr  6726  nqprl  6741  nqpru  6742  addnqprlemrl  6747  addnqprlemru  6748  addnqprlemfl  6749  addnqprlemfu  6750  appdivnq  6753  appdiv0nq  6754  mulnqprl  6758  mulnqpru  6759  mullocprlem  6760  mullocpr  6761  mulnqprlemrl  6763  mulnqprlemru  6764  mulnqprlemfl  6765  mulnqprlemfu  6766  distrlem1prl  6772  distrlem1pru  6773  distrlem4prl  6774  distrlem4pru  6775  ltprordil  6779  1idprl  6780  1idpru  6781  ltpopr  6785  ltsopr  6786  ltaddpr  6787  ltexprlemm  6790  ltexprlemopl  6791  ltexprlemopu  6793  ltexprlemloc  6797  ltexprlemrl  6800  ltexprlemru  6802  addcanprleml  6804  addcanprlemu  6805  addcanprg  6806  ltaprlem  6808  prplnqu  6810  addextpr  6811  recexprlemell  6812  recexprlemelu  6813  recexprlemm  6814  recexprlemdisj  6820  recexprlempr  6822  recexprlem1ssl  6823  recexprlem1ssu  6824  recexprlemss1l  6825  recexprlemss1u  6826  aptiprleml  6829  aptiprlemu  6830  ltmprr  6832  cauappcvgprlemopu  6838  cauappcvgprlemdisj  6841  cauappcvgprlemloc  6842  cauappcvgprlemladdfu  6844  cauappcvgprlemladdfl  6845  cauappcvgprlemladdru  6846  cauappcvgprlemladdrl  6847  cauappcvgprlem1  6849  cauappcvgprlem2  6850  cauappcvgprlemlim  6851  archrecnq  6853  caucvgprlemnkj  6856  caucvgprlemnbj  6857  caucvgprlemopu  6861  caucvgprlemdisj  6864  caucvgprlemloc  6865  caucvgprlemladdfu  6867  caucvgprlem2  6870  caucvgprprlemval  6878  caucvgprprlemnkltj  6879  caucvgprprlemnkeqj  6880  caucvgprprlemnjltk  6881  caucvgprprlemnbj  6883  caucvgprprlemmu  6885  caucvgprprlemopl  6887  caucvgprprlemopu  6889  caucvgprprlemdisj  6892  caucvgprprlemloc  6893  caucvgprprlemexbt  6896  caucvgprprlemexb  6897  caucvgprprlemaddq  6898  caucvgprprlem2  6900  enreceq  6913  mulcmpblnrlemg  6917  ltsrprg  6924  recexgt0sr  6950  addgt0sr  6952  mulgt0sr  6954  archsr  6958  prsrriota  6964  caucvgsrlemcau  6969  caucvgsrlemgt1  6971  caucvgsrlemoffval  6972  caucvgsrlemofff  6973  caucvgsrlemoffcau  6974  caucvgsrlemoffgt1  6975  caucvgsrlemoffres  6976  caucvgsr  6978  pitonn  7016  ltrennb  7022  ax0id  7044  rereceu  7055  recriota  7056  axcaucvglemval  7063  axcaucvglemcau  7064  axcaucvglemres  7065  ltxrlt  7178  lttri3  7191  ltnsym  7197  ltletr  7200  muladd11  7241  readdcan  7248  cnegexlem1  7283  cnegexlem2  7284  cnegexlem3  7285  cnegex  7286  negeu  7299  npncan2  7335  subneg  7357  negcon1  7360  addid0  7477  lelttrdi  7530  ltleadd  7550  lt2sub  7564  le2sub  7565  lenegcon1  7570  addge01  7576  leaddle0  7581  mullt0  7584  recexre  7678  reapti  7679  rimul  7685  apreap  7687  ltmul1  7692  apreim  7703  apcotr  7707  mulext1  7712  mulge0  7719  apti  7722  ltleap  7730  recextlem1  7741  recexaplem2  7742  recexap  7743  mulcanapd  7751  divmulassap  7783  divmulasscomap  7784  divmul13ap  7803  conjmulap  7817  p1le  7927  recgt0  7928  prodgt0gt0  7929  prodgt0  7930  lemul2a  7937  ltmul12a  7938  mulgt1  7941  lemulge12  7945  ltdivmul  7954  ltrec1  7966  ledivdiv  7968  lediv2a  7973  lbinf  8026  suprleubex  8032  cju  8038  nn1suc  8058  nnmulcl  8060  nn2ge  8071  nnsub  8077  halfaddsub  8265  div4p1lem1div2  8284  nnrecl  8286  nn0ge2m1nn  8348  nn0nndivcl  8350  elnn0z  8364  peano2z  8387  zaddcllempos  8388  zaddcllemneg  8390  zaddcl  8391  ztri3or  8394  zletric  8395  zlelttric  8396  zleloe  8398  zrevaddcl  8401  zltp1le  8405  zlem1lt  8407  elz2  8419  zdceq  8423  zdcle  8424  zdclt  8425  nn0n0n1ge2b  8427  nn0lt2  8429  nn0ge0div  8434  zdiv  8435  zdivadd  8436  zdivmul  8437  zextle  8438  suprzclex  8445  msqznn  8447  zneo  8448  zeo  8452  peano5uzti  8455  nn0ind-raph  8464  uztrn  8635  uzss  8639  eluzadd  8647  uzaddcl  8674  indstr  8681  supinfneg  8683  infsupneg  8684  indstr2  8696  nn0ge2m1nnALT  8703  qmulz  8708  qaddcl  8720  qnegcl  8721  qmulcl  8722  qreccl  8727  qrevaddcl  8729  ge0p1rp  8765  rpnegap  8766  divlt1lt  8801  divle1le  8802  ledivge1le  8803  nnledivrp  8837  nn0ledivnn  8838  ltxr  8849  xrltnsym  8868  xrlttr  8870  xrltso  8871  xrlttri3  8872  xrltletr  8877  xrre2  8888  ge0nemnf  8891  xltnegi  8902  lbioog  8936  iccss2  8967  iccssioo2  8969  iccssico2  8970  iooshf  8975  elioopnf  8990  elioomnf  8991  elicopnf  8992  elxrge0  9001  icoshftf1o  9013  iccshftr  9016  iccshftl  9018  iccdil  9020  icccntr  9022  lincmb01cmp  9025  iccf1o  9026  zltaddlt1le  9028  elfz5  9037  fztri3or  9058  fznlem  9060  fzn  9061  uzsubsubfz  9066  fzdisj  9071  fzmmmeqm  9076  fzaddel  9077  fzopth  9079  fznatpl1  9093  fzdifsuc  9098  elfz1b  9107  fseq1p1m1  9111  elfzp1b  9114  fzm1  9117  fzneuz  9118  ige2m1fz  9127  elfz0ubfz0  9136  elfz0fzfz0  9137  fz0fzelfz0  9138  fz0fzdiffz0  9141  elfzmlbp  9143  difelfzle  9145  difelfznle  9146  nn0disj  9148  1fv  9149  4fvwrd4  9150  fzoss1  9180  fzospliti  9185  fzosplit  9186  fzouzdisj  9189  fzo1fzo0n0  9192  elfzo0z  9193  fzonmapblen  9196  fzofzim  9197  fzoaddel  9201  fzosubel  9203  fzosubel3  9205  eluzgtdifelfzo  9206  elfzodifsumelfzo  9210  elfzom1elp1fzo  9211  zpnn0elfzo1  9217  elfzom1p1elfzo  9223  ssfzo12  9233  ssfzo12bi  9234  ubmelm1fzo  9235  elfzonelfzo  9239  elfzomelpfzo  9240  fzoshftral  9247  exfzdc  9249  fvinim0ffz  9250  subfzo0  9251  qletric  9253  qlelttric  9254  qdceq  9256  qbtwnre  9265  qbtwnxr  9266  qavgle  9267  ico0  9270  ioc0  9271  flqge  9284  flqltnz  9289  flqbi  9292  flqge0nn0  9295  flqge1nn  9296  flqaddz  9299  btwnzge0  9302  flltdivnn0lt  9306  fldiv4p1lem1div2  9307  flqeqceilz  9320  intfracq  9322  flqdiv  9323  zmod1congr  9343  zmodcl  9346  zmodfz  9348  modqid0  9352  zmodid2  9354  modqmuladdnn0  9370  modqm1p1mod0  9377  q2txmodxeq0  9386  q2submod  9387  modifeq2int  9388  modaddmodup  9389  modaddmodlo  9390  modqaddmulmod  9393  modqsubdir  9395  modfzo0difsn  9397  modsumfzodifsn  9398  addmodlteq  9400  frec2uzltd  9405  frec2uzlt2d  9406  frec2uzrand  9407  frec2uzf1od  9408  frec2uzisod  9409  frecuzrdgrrn  9410  frec2uzrdg  9411  frecuzrdgfn  9414  frecuzrdgcl  9415  frecuzrdgsuc  9417  frecfzennn  9419  uzsinds  9428  iseqovex  9439  iseqval  9440  iseqf  9444  iseqss  9446  iseqfveq2  9448  iseqfeq2  9449  iseqfeq  9451  iseqshft2  9452  monoord  9455  monoord2  9456  isermono  9457  iseqsplit  9458  iseqcaopr3  9460  iseqcaopr2  9461  iseqid3  9465  iseqid3s  9466  iseqid  9467  iseqhomo  9468  iseqz  9469  iseqdistr  9470  expivallem  9477  expival  9478  expp1  9483  expn1ap0  9486  expcllem  9487  expcl2lemap  9488  rpexpcl  9495  m1expcl2  9498  expclzaplem  9500  1exp  9505  expap0  9506  expeq0  9507  expnegzap  9510  mulexp  9515  expadd  9518  expaddzaplem  9519  expmul  9521  leexp2r  9530  leexp1a  9531  expubnd  9533  sqgt0ap  9544  subsq  9581  binom2sub  9587  zesq  9591  bernneq  9593  bernneq3  9595  expnbnd  9596  expnlbnd  9597  sqoddm1div8  9625  nn0opthlem2d  9648  nn0opthd  9649  facnn2  9661  facdiv  9665  facwordi  9667  faclbnd  9668  faclbnd3  9670  faclbnd6  9671  facubnd  9672  facavg  9673  bcval4  9679  bccmpl  9681  ibcval5  9690  bcpasc  9693  shftlem  9704  shftuz  9705  shftfvalg  9706  shftfval  9709  shftfn  9712  shftval3  9715  shftcan2  9723  crre  9744  reim0b  9749  rereb  9750  mulreap  9751  readd  9756  remullem  9758  remul2  9760  imadd  9764  immul2  9767  cjadd  9771  cjexp  9780  cjap  9793  caucvgre  9867  cvg1nlemf  9869  cvg1nlemres  9871  cvg1n  9872  rexanuz2  9877  recvguniq  9881  resqrexlem1arp  9891  resqrexlemp1rp  9892  resqrexlemfp1  9895  resqrexlemover  9896  resqrexlemdec  9897  resqrexlemlo  9899  resqrexlemcalc1  9900  resqrexlemcalc2  9901  resqrexlemcalc3  9902  resqrexlemnm  9904  resqrexlemcvg  9905  resqrexlemgt0  9906  resqrexlemoverl  9907  resqrexlemglsq  9908  resqrexlemga  9909  resqrexlemex  9911  rersqrtthlem  9916  sqrtmul  9921  sqrtsq2  9929  absrpclap  9947  absnid  9959  absexp  9965  absexpzap  9966  nn0abscl  9971  ltabs  9973  lenegsq  9981  recvalap  9983  nnabscl  9986  fzomaxdiflem  9998  fzomaxdif  9999  cau3lem  10000  maxabslemlub  10093  maxleast  10099  maxleastlt  10101  maxltsup  10104  fimaxre2  10109  minmax  10112  clim  10120  climconst  10129  climconst2  10130  climuni  10132  climmpt  10139  2clim  10140  climshft2  10145  climcn1  10147  climcn2  10148  mulcn2  10151  climge0  10163  climadd  10164  climmul  10165  climsub  10166  climaddc1  10167  climaddc2  10168  climmulc2  10169  climsubc1  10170  climsubc2  10171  climsqz  10173  climsqz2  10174  clim2iser  10175  clim2iser2  10176  iiserex  10177  iisermulc2  10178  climlec2  10179  iserile  10180  climrecvg1n  10185  dvdsval2  10198  dvdsval3  10199  nndivdvds  10201  moddvds  10204  dvds0lem  10205  absdvdsb  10213  zdvdsdc  10216  dvdscmulr  10224  dvdsmulcr  10225  modmulconst  10227  dvds2ln  10228  dvdstr  10232  dvdssub2  10237  dvdsadd  10238  dvdsadd2b  10242  dvdslelemd  10243  dvdsleabs2  10246  dvdsabseq  10247  dvdseq  10248  divconjdvds  10249  dvdsflip  10251  dvdsssfz1  10252  dvds1  10253  fzm1ndvds  10256  fzo0dvdseq  10257  mulmoddvds  10263  even2n  10273  mod2eq1n2dvds  10279  evennn02n  10282  evennn2n  10283  2tp1odd  10284  2teven  10287  ltoddhalfle  10293  halfleoddlt  10294  nnehalf  10304  nno  10306  nn0o  10307  nn0ob  10308  divalglemnn  10318  divalglemnqt  10320  divalglemeunn  10321  divalglemeuneg  10323  divalgmod  10327  modremain  10329  flodddiv4  10334  fldivndvdslt  10335  flodddiv4t2lthalf  10337  gcdmndc  10340  zsupcllemstep  10341  zsupcllemex  10342  zssinfcl  10344  infssuzex  10345  gcdsupex  10349  gcdsupcl  10350  divgcdnn  10366  gcd0id  10370  gcdneg  10373  gcdaddm  10375  gcdadd  10376  gcdabs1  10380  modgcd  10382  bezoutlemnewy  10385  bezoutlemzz  10391  bezoutlemaz  10392  bezoutlemsup  10398  dfgcd3  10399  bezout  10400  dfgcd2  10403  gcdmultiple  10409  gcdmultiplez  10410  gcdzeq  10411  dvdssqim  10413  dvdsmulgcd  10414  rpmulgcd  10415  rplpwr  10416  sqgcd  10418  dvdssqlem  10419  dvdssq  10420  bezoutr  10421  bezoutr1  10422  nn0seqcvgd  10423  ialgrlem1st  10424  ialgrlemconst  10425  ialgrp1  10428  algcvgblem  10431  ialgcvga  10433  eucalgval2  10435  eucalgf  10437  eucalginv  10438  eucalglt  10439  lcmmndc  10444  lcmval  10445  lcmcllem  10449  lcmledvds  10452  lcmcl  10454  lcmneg  10456  lcmgcdlem  10459  lcmgcd  10460  lcmdvds  10461  lcmid  10462  lcmgcdeq  10465  lcmass  10467  coprmgcdb  10470  ncoprmgcdne1b  10471  coprmdvds  10474  coprmdvds2  10475  mulgcddvds  10476  rpmulgcd2  10477  qredeq  10478  qredeu  10479  divgcdcoprm0  10483  divgcdcoprmex  10484  cncongr1  10485  cncongr2  10486  isprm2  10499  isprm3  10500  prmind2  10502  prmind  10503  dvdsprime  10504  nprm  10505  dvdsnprmd  10507  oddprmge3  10516  sqnprm  10517  dvdsprm  10518  divgcdodd  10522  coprm  10523  isprm6  10526  prmdvdsexpr  10529  prmexpb  10530  prmfac1  10531  rpexp  10532  pw2dvdseulemle  10545  oddpwdclemdc  10551  oddpwdc  10552  sqrt2irrap  10558  sscoll2  10783  qdencn  10785