Axiom ax-mp 5

Description: Rule of Modus Ponens. The postulated inference rule of propositional calculus. See e.g. Rule 1 of [Hamilton] p. 73. The rule says, "if 𝜑 is true, and 𝜑 implies 𝜓, then 𝜓 must also be true." This rule is sometimes called "detachment", since it detaches the minor premise from the major premise. "Modus ponens" is short for "modus ponendo ponens", a Latin phrase that means "the mode that by affirming affirms" - remark in [Sanford] p. 39. This rule is similar to the rule of modus tollens mto 652.

Note: In some web page displays such as the Statement List, the symbols "& " and "⇒ " informally indicate the relationship between the hypotheses and the assertion (conclusion), abbreviating the English words "and" and "implies." They are not part of the formal language. (Contributed by NM, 30-Sep-1992.)

Hypotheses

Ref	Expression
min	⊢ 𝜑
maj	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ax-mp	⊢ 𝜓

Detailed syntax breakdown of Axiom ax-mp

Step	Hyp	Ref	Expression
1		wps	1 wff 𝜓

This axiom is referenced by:  mp2b  8  a1i  9  mp1i  10  a2i  11  mpd  13  mp2  16  idALT  20  simpli  110  simpri  112  biimpi  119  bicomi  131  mpbi  144  mpbir  145  imbi1i  237  a1bi  242  tbt  246  biantru  300  biantrur  301  mp2an  423  pm2.65i  629  notnoti  635  pm2.21i  636  pm2.24ii  637  notbii  658  nbn  689  ori  713  orci  721  olci  722  biorfi  736  imorri  739  dcbii  826  simp1i  991  simp2i  992  simp3i  993  3mix1i  1154  3mix2i  1155  3mix3i  1156  3jaoi  1282  mptru  1341  dfnot  1350  mptnan  1402  mtpor  1404  mtpxor  1405  mpg  1428  19.23h  1475  hbequid  1494  axi12  1495  nfri  1500  spi  1517  19.21  1563  eximii  1582  19.35i  1605  nfn  1637  19.37aiv  1654  19.23  1657  exan  1672  equid  1678  hbae  1697  equvini  1732  equveli  1733  sbid  1748  sbieh  1764  exdistrfor  1773  dveeq2or  1789  ax11v  1800  ax11ev  1801  equs5or  1803  sb4or  1806  sb4bor  1808  nfsb2or  1810  sbequilem  1811  sbequi  1812  speiv  1835  nfsbxy  1916  nfsbxyt  1917  sbco  1942  sbcocom  1944  sbcomxyyz  1946  elsb3  1952  elsb4  1953  sbal1yz  1977  dvelimALT  1986  dvelimfv  1987  dvelimor  1994  eumoi  2033  moani  2070  eqeq1i  2148  eqeq2i  2151  eleq1i  2206  eleq2i  2207  nfcrii  2275  neeq1i  2324  neeq2i  2325  necon3i  2357  rspec  2487  rgen2a  2489  mprg  2492  r19.21  2511  r19.23  2543  raleqi  2633  rexeqi  2634  rabeqif  2680  elv  2693  elexi  2701  ceqsal  2718  vtocl3  2745  vtoclef  2762  vtocle  2763  spcv  2783  spcev  2784  clel3  2824  elabf  2831  elab2  2836  elab3  2840  euxfrdc  2874  reueq  2887  rmoimi2  2891  sbsbc  2917  sbc8g  2920  sbc6  2938  sbcie  2947  sbcrex  2992  csbvarg  3035  csbief  3049  csbie2  3054  sbnfc2  3065  sseli  3098  sselii  3099  sseq1i  3128  sseq2i  3129  difeq1i  3195  difeq2i  3196  uneq1i  3231  uneq2i  3232  ineq1i  3278  ineq2i  3279  ssinss1  3310  difdif2ss  3338  n0ii  3376  ne0ii  3377  vn0  3378  vn0m  3379  abf  3411  disj2  3423  difid  3436  0dif  3439  disjdif  3440  difin0  3441  undif1ss  3442  difdifdirss  3452  rgenm  3470  iftruei  3485  iffalsei  3488  ifbieq2i  3500  ifbieq12i  3502  pweqi  3519  pwid  3530  sneqi  3544  elsn  3548  elpr  3553  elsn2  3566  ralsn  3574  rexsn  3575  eltp  3579  rabrsndc  3599  preq1i  3611  preq2i  3612  prid1  3637  snnz  3650  snm  3651  prnz  3653  prm  3654  tpnz  3656  snsssn  3696  opeq1i  3716  opeq2i  3717  unieqi  3754  unissi  3767  inteqi  3783  intmin2  3805  intab  3808  intsn  3814  iinconstm  3830  iuniin  3831  iinss1  3833  iunxdif2  3869  ssiinf  3870  iinss  3872  iinss2  3873  iinab  3882  iundif2ss  3886  iindif2m  3888  iinin2m  3889  iunxsn  3897  iunxprg  3901  iinpw  3911  sndisj  3933  disjxsn  3935  breqi  3943  breq1i  3944  breq2i  3945  brab1  3983  opabbii  4003  truni  4048  bm1.3ii  4057  a9evsep  4058  ax9vsep  4059  zfnuleu  4060  axnul  4061  ssexi  4074  rabex  4080  elpw2  4090  pwnss  4091  iin0r  4101  intv  4102  pwex  4115  snex  4117  notnotsnex  4119  ord3ex  4122  dtruarb  4123  undifexmid  4125  intid  4154  opnzi  4165  copsexg  4174  opelopabf  4204  epelc  4221  elon  4304  inton  4323  onn0  4330  onm  4331  elsuc  4336  elsuc2  4337  sucid  4347  iunsuc  4350  onordi  4356  ontrci  4357  onelssi  4359  eusvnf  4382  ssonunii  4413  sucex  4423  onssi  4439  onsuci  4440  ordtriexmidlem  4443  ordtriexmidlem2  4444  ordtriexmid  4445  ordtri2orexmid  4446  2ordpr  4447  ontr2exmid  4448  onsucsssucexmid  4450  onsucelsucexmid  4453  regexmidlemm  4455  reg2exmid  4459  onirri  4466  ruALT  4474  onprc  4475  sucon  4476  dtru  4483  0elsucexmid  4488  ordpwsucexmid  4493  ordtri2or2exmid  4494  dcextest  4503  omex  4515  find  4521  omelon  4530  nnoni  4532  limom  4535  nnregexmid  4542  omsinds  4543  xpeq1i  4567  xpeq2i  4568  0nelxp  4575  opthprc  4598  mosubop  4613  releqi  4630  relssi  4638  relin1  4665  relin2  4666  reldif  4667  inopab  4679  difopab  4680  xpiindim  4684  opabbi2dv  4696  ideq  4699  coeq1i  4706  coeq2i  4707  cnveqi  4722  eldm  4744  eldm2  4745  dmeqi  4748  dmv  4763  rneqi  4775  elrnmpti  4800  dmex  4813  rnex  4814  reseq1i  4823  reseq2i  4824  residm  4859  resex  4868  resmpt3  4876  imaeq1i  4886  imaeq2i  4887  elima  4894  imaex  4902  elimasn  4914  args  4916  epini  4918  dfse2  4920  relbrcnv  4927  cotr  4928  issref  4929  cnvsym  4930  asymref  4932  intirr  4933  codir  4935  qfto  4936  ssrnres  4989  cnveq0  5003  cnvsn0  5015  dmsnop  5020  rnsnop  5027  resdm2  5037  dfco2a  5047  cocnvcnv1  5057  coi2  5063  coires1  5064  cnvssrndm  5068  cossxp  5069  cocnvres  5071  relrelss  5073  relcoi2  5077  unidmrn  5079  dfdm2  5081  unixpm  5082  cnvexg  5084  cnvex  5085  cnviinm  5088  iotaval  5107  funeqi  5152  funi  5163  funres  5172  funcnvsn  5176  funcnvcnv  5190  funin  5202  funcnvres  5204  isarep2  5218  fneq1i  5225  fneq2i  5226  fnresdisj  5241  fnresi  5248  mpt0  5258  dmmpti  5260  feq1i  5273  feq2i  5274  fdmi  5288  fun2  5304  fssres  5306  resasplitss  5310  fintm  5316  fconst6  5330  f1ores  5390  foimacnv  5393  resdif  5397  funcocnv2  5400  f1ovi  5414  fveq1i  5430  fveq2i  5432  0fv  5464  fvun1  5495  fvopab3ig  5503  fvmptss2  5504  mptrcl  5511  elfvmptrab1  5523  fndmdif  5533  fneqeql2  5537  f1oresrab  5593  fmptco  5594  fnressn  5614  fressnfv  5615  fmptap  5618  fvsnun1  5625  fvsnun2  5626  fsnunfv  5629  fconst2  5645  mptex  5654  riotabiia  5755  acexmidlema  5773  acexmidlemb  5774  acexmidlemcase  5777  acexmidlem2  5779  acexmidlemv  5780  oveq1i  5792  oveq2i  5793  oveqi  5795  oprabidlem  5810  0neqopab  5824  oprabbii  5834  oprabss  5865  mpompt  5871  funoprab  5879  fnoprab  5882  fovcl  5884  ovigg  5899  elmpocl  5976  resfunexgALT  6016  cofunexg  6017  opabex3d  6027  opabex3  6028  1st0  6050  2nd0  6051  op1st  6052  op2nd  6053  f1stres  6065  f2ndres  6066  fo1stresm  6067  fo2ndresm  6068  1stcof  6069  2ndcof  6070  1stexg  6073  2ndexg  6074  releldm2  6091  reldm  6092  dfoprab3  6097  mpomptsx  6103  mpompts  6104  fnmpoi  6110  dmmpo  6111  mpoexxg  6116  1stconst  6126  2ndconst  6127  dfmpo  6128  algrflem  6134  algrflemg  6135  cnvoprab  6139  f1od2  6140  mpoxopn0yelv  6144  mpoxopoveq  6145  tposssxp  6154  brtpos2  6156  reldmtpos  6158  dftpos2  6166  dftpos4  6168  tpostpos  6169  tpostpos2  6170  tposfo  6176  tposf  6177  tposeqi  6182  tposex  6183  tposoprab  6185  issmo  6193  smores  6197  smores2  6199  iordsmo  6202  smo0  6203  tfrlem8  6223  tfrexlem  6239  tfr1onlem3  6243  tfr1onlemsucaccv  6246  tfr1onlembxssdm  6248  tfr1onlemres  6254  tfri1dALT  6256  tfri2  6271  rdgisuc1  6289  rdg0  6292  frecfun  6300  frec0g  6302  freccllem  6307  frecfcllem  6309  frecsuclem  6311  frecrdg  6313  2on0  6331  xp01disj  6338  2oconcl  6344  fnoa  6351  oaexg  6352  fnom  6354  omexg  6355  fnoei  6356  oeiexg  6357  oei0  6363  oacl  6364  oasuc  6368  o1p1e2  6372  omsuc  6376  nna0r  6382  nnm0r  6383  1onn  6424  2onn  6425  3onn  6426  4onn  6427  eqerlem  6468  elqs  6488  qsex  6494  ecqs  6499  iinerm  6509  th3qlem1  6539  th3q  6542  mapsn  6592  mapsnf1o3  6599  ixpiinm  6626  ixpssmap  6634  brdom  6652  f1dom  6662  enref  6667  dom2  6677  idssen  6679  ssdomg  6680  ensymi  6684  ensn1  6698  fiprc  6717  1domsn  6721  xpcomf1o  6727  xpcomco  6728  dom0  6740  0dom  6741  xpmapenlem  6751  phplem2  6755  php5  6760  snnen2og  6761  1nen2  6763  php5dom  6765  ssfilem  6777  ssfiexmid  6778  domfiexmid  6780  0fin  6786  diffitest  6789  findcard  6790  findcard2  6791  findcard2s  6792  isinfinf  6799  ac6sfi  6800  inffiexmid  6808  unfiexmid  6814  xpfi  6826  fisseneq  6828  ssfirab  6830  en1eqsn  6844  snexxph  6846  sbthlem2  6854  sbthlemi3  6855  sbthlemi6  6858  sbthlem7  6859  fi0  6871  supeq1i  6883  infeq1i  6908  djuexb  6937  djuf1olemr  6947  inresflem  6953  djuinr  6956  updjudhcoinlf  6973  updjudhcoinrg  6974  casefun  6978  caserel  6980  caseinj  6982  caseinl  6984  caseinr  6985  omp1eomlem  6987  endjusym  6989  difinfsn  6993  difinfinf  6994  djuinj  6999  0ct  7000  ctmlemr  7001  ctssdclemn0  7003  ctssdccl  7004  omct  7010  ctfoex  7011  finomni  7020  exmidomni  7022  fodjuomni  7029  nnnninf  7031  ctssexmid  7032  fodjumkv  7042  card0  7061  exmidonfinlem  7066  dju1p1e2  7070  exmidfodomrlemim  7074  exmidfodomrlemr  7075  exmidfodomrlemrALT  7076  0npi  7145  dmaddpi  7157  dmmulpi  7158  1lt2pi  7172  0nnq  7196  1nq  7198  dmaddpq  7211  dmmulpq  7212  rec1nq  7227  1lt2nq  7238  halfnqq  7242  prarloclemarch2  7251  enq0enq  7263  nqnq0pi  7270  nnnq0lem1  7278  addnnnq0  7281  mulnnnq0  7282  nq0m0r  7288  addpinq1  7296  prarloclem5  7332  prarloclemcalc  7334  1pr  7386  1idprl  7422  1idpru  7423  ltexprlemm  7432  recexprlem1ssl  7465  recexprlem1ssu  7466  suplocexprlemell  7545  suplocexprlem2b  7546  suplocexprlemmu  7550  suplocexprlemdisj  7552  suplocexprlemloc  7553  suplocexprlemub  7555  suplocexprlemlub  7556  prsrlem1  7574  addsrpr  7577  mulsrpr  7578  gt0srpr  7580  0nsr  7581  0r  7582  1sr  7583  m1r  7584  m1m1sr  7593  caucvgsr  7634  suplocsrlempr  7639  addresr  7669  mulresr  7670  pitonnlem1  7677  peano1nnnn  7684  axi2m1  7707  axcnre  7713  peano5nnnn  7724  axcaucvg  7732  mulid1i  7792  mulid2i  7793  pnfnre  7831  mnfnre  7832  pnfnemnf  7844  mnfxr  7846  rexri  7847  ltnri  7880  ltleii  7890  00id  7927  addid1i  7928  addid2i  7929  0cnALT  7976  negeqi  7980  negicn  7987  neg0  8032  renegcli  8048  negcli  8054  negidi  8055  negnegi  8056  subidi  8057  subid1i  8058  negne0bi  8059  negrebi  8060  mul02i  8176  mul01i  8177  mulm1i  8189  leidi  8271  gt0ne0ii  8273  inelr  8370  msqge0i  8403  gt0ap0ii  8414  1div1e1  8488  div1i  8524  eqnegi  8525  recclapi  8526  recidapi  8527  divmulapi  8550  rerecclapi  8561  redivclapi  8563  recgt0  8632  ltp1i  8687  divgt0ii  8701  ltmul1ii  8710  ltdiv1ii  8711  sup3exmid  8739  peano5nni  8747  nnrei  8753  1nn  8755  nngt0i  8774  neg1ap0  8853  2timesi  8874  times2i  8875  2nn  8905  3nn  8906  4nn  8907  5nn  8908  6nn  8909  7nn  8910  8nn  8911  9nn  8912  2muline0  8969  rehalfcli  8992  nn0ssre  9005  nnnn0i  9009  dfn2  9014  0nn0  9016  nn0ge0i  9028  zrei  9084  neg1z  9110  nn0negzi  9113  dfz2  9147  nneoi  9179  peano5uzi  9184  dfuzi  9185  nn0ind-raph  9192  deceq1i  9212  deceq2i  9213  10nn  9221  numltc  9231  eluzel2  9355  eluz1i  9357  nn0uz  9384  nnuz  9385  infrenegsupex  9416  lbzbi  9435  divfnzn  9440  qdivcl  9462  irrmul  9466  cnref1o  9469  0ltpnf  9598  mnflt0  9600  0lepnf  9606  xrltnsym  9609  xrlttri3  9613  nltpnft  9627  ngtmnft  9630  xrrebnd  9632  xnegmnf  9642  xneg0  9644  xltnegi  9648  xaddmnf1  9661  xaddmnf2  9662  mnfaddpnf  9664  xaddid1  9675  xnn0lenn0nn0  9678  xnn0xadd0  9680  xposdif  9695  ixxex  9712  iooval2  9728  unirnioo  9786  ioorebasg  9788  elrege0  9789  fzval2  9824  fzen  9854  fzprval  9893  fztpval  9894  uzdisj  9904  ige2m1fz  9921  fz01or  9922  fz1ssfz0  9928  fz0tp  9932  nn0disj  9946  1fv  9947  4fvwrd4  9948  fzo0ss1  9982  fzo01  10024  fzo12sn  10025  fzo0to2pr  10026  fzo0to3tp  10027  fzo0to42pr  10028  qbtwnxr  10066  flval  10076  modqfrac  10141  modqmulnn  10146  q2txmodxeq0  10188  frecuzrdgdom  10222  frecuzrdgfun  10224  frecuzrdgsuct  10228  frechashgf1o  10232  nnct  10239  fxnn0nninf  10242  0tonninf  10243  1tonninf  10244  iseqvalcbv  10261  ser0f  10319  0exp0e1  10329  qexpcl  10340  qexpclz  10345  m1expcl2  10346  1exp  10353  sqvali  10403  sqcli  10404  sqeq0i  10405  resqcli  10408  sq1  10417  neg1sqe1  10418  iexpcyc  10428  facnn  10505  fac0  10506  fac1  10507  fac2  10509  fac3  10510  fac4  10511  bcval  10527  bcm1k  10538  bcpasc  10544  bccl  10545  4bc3eq4  10551  4bc2eq6  10552  hashinfom  10556  hashennn  10558  hashfz1  10561  fihasheq0  10572  hash0  10575  hashsng  10576  fihashen1  10577  omgadd  10580  hashp1i  10588  hashxp  10604  fimaxq  10605  zfz1iso  10616  shftidt2  10636  cjexp  10697  re0  10699  im0  10700  re1  10701  im1  10702  cj0  10705  cji  10706  recli  10715  imcli  10716  cjcli  10717  replimi  10718  cjcji  10719  reim0bi  10720  rerebi  10721  cjrebi  10722  recji  10723  imcji  10724  cjmulrcli  10725  cjmulvali  10726  cjmulge0i  10727  renegi  10728  imnegi  10729  cjnegi  10730  addcji  10731  uzin2  10791  rexanuz  10792  rexfiuz  10793  sqrtrval  10804  sqrt0  10808  resqrexlemcalc3  10820  resqrexlemcvg  10823  resqrex  10830  abs0  10862  absi  10863  qabsor  10879  absimle  10888  recan  10913  caubnd2  10921  leabsi  10932  absrei  10933  sqrtpclii  10934  sqrtgt0ii  10935  absvalsqi  10944  absvalsq2i  10945  abscli  10946  absge0i  10947  absval2i  10948  abs00i  10949  absgt0api  10950  absnegi  10951  abscji  10952  releabsi  10953  infxrnegsupex  11064  xrbdtri  11077  cbvsum  11161  sumeq1i  11164  sum0  11189  isumz  11190  fisumss  11193  fsumsersdc  11196  fsumadd  11207  isumclim  11222  isumclim3  11224  fsumcnv  11238  modfsummodlem1  11257  fsumrelem  11272  binomlem  11284  binom  11285  arisum2  11300  expcnv  11305  0.999...  11322  prodf1f  11344  cbvprod  11359  prodeq1i  11362  zproddc  11380  zprodap0  11382  ef0lem  11403  esum  11405  ere  11413  ege2le3  11414  ef0  11415  eff2  11423  efsep  11434  reeff1  11443  sin0  11472  cos0  11473  ef01bndlem  11499  cos2bnd  11503  sincos1sgn  11507  sincos2sgn  11508  sin4lt0  11509  eirr  11521  0dvds  11549  dvds1  11587  z0even  11644  n2dvdsm1  11646  z2even  11647  n2dvds3  11648  ndvdssub  11663  ndvdsi  11666  flodddiv4  11667  gcddvds  11688  gcd1  11711  6gcd4e2  11719  bezoutlembi  11729  dfgcd3  11734  dfgcd2  11738  lcmval  11780  lcmcllem  11784  lcmledvds  11787  3lcm2e6woprm  11803  qredeu  11814  isprm2lem  11833  isprm3  11835  prm2orodd  11843  sqrt2irr0  11878  pw2dvds  11880  phicl2  11926  phi1  11931  dfphi2  11932  phiprmpw  11934  ennnfonelemp1  11955  ennnfonelem1  11956  ennnfonelemkh  11961  ennnfonelemex  11963  ennnfonelemnn0  11971  ennnfonelemr  11972  exmidunben  11975  ctinfomlemom  11976  ctinfom  11977  ctinf  11979  qnnen  11980  omctfn  11992  omiunct  11993  structcnvcnv  12014  structfun  12016  structfn  12017  ndxarg  12021  ndxid  12022  setsresg  12036  setsslnid  12049  strleun  12087  strle1g  12088  istopon  12219  topontopi  12222  toponunii  12223  toponrestid  12227  istps  12238  topontopn  12243  eltpsi  12247  eltg4i  12263  eltg3  12265  tg1  12267  tg2  12268  tgclb  12273  topnex  12294  sn0topon  12296  distps  12299  cldrcl  12310  sn0cld  12345  restco  12382  lmrcl  12399  ssidcn  12418  cnconst2  12441  cnptopresti  12446  cnptoprest  12447  txuni2  12464  txbas  12466  eltx  12467  txcnp  12479  upxp  12480  txcnmpt  12481  uptx  12482  txcn  12483  txrest  12484  txlm  12487  cnmptid  12489  cnmpt1st  12496  cnmpt2nd  12497  hmeofn  12510  psmetge0  12539  ismeti  12554  xmetunirn  12566  xmetge0  12573  unirnblps  12630  unirnbl  12631  mopnex  12713  qtopbasss  12729  retop  12732  uniretop  12733  iooretopg  12736  cnxmet  12739  cntoptopon  12740  cnbl0  12742  rexmet  12749  blssioo  12753  tgioo  12754  tgqioo  12755  cnopnap  12802  limcresi  12843  dvfvalap  12858  dvidlemap  12868  dvcnp2cntop  12871  dvcoapbr  12879  dvexp2  12884  dvrecap  12885  dveflem  12895  dvef  12896  reeff1o  12902  sin0pilem1  12910  sin0pilem2  12911  pilem3  12912  pigt2lt4  12913  pire  12915  sinhalfpilem  12920  pidiv2halves  12924  cosneghalfpi  12927  cospi  12929  efipi  12930  sin2pi  12932  cos2pi  12933  ef2pi  12934  cosq14gt0  12961  coseq00topi  12964  coseq0negpitopi  12965  sincos4thpi  12969  sincos6thpi  12971  sincos3rdpi  12972  pigt3  12973  cos02pilt1  12980  ioocosf1o  12983  dfrelog  12989  relogf1o  12990  relogcl  12991  relogiso  13002  rpcxpsqrt  13050  rpabscxpbnd  13067  2logb9irr  13096  2logb9irrALT  13099  sqrt2cxp2logb9e3  13100  2irrexpq  13101  2logb9irrap  13102  2irrexpqap  13103  ex-fl  13108  ex-ceil  13109  ex-exp  13110  ex-fac  13111  ex-gcd  13114  bj-dcdc  13136  bj-stdc  13137  bj-dcst  13138  bj-stst  13139  bj-el2oss1o  13152  elabf2  13160  bd0  13193  bdeli  13215  bdcriota  13252  bdbm1.3ii  13260  bdinex1  13268  bdssexi  13272  bj-inex  13276  bj-snex  13282  bj-sucex  13292  bj-d0clsepcl  13294  bj-omind  13303  bj-om  13306  bj-2inf  13307  bj-peano2  13308  bdpeano5  13312  bj-omssonALT  13332  bj-inf2vnlem1  13339  bj-omex2  13346  bj-nn0sucALT  13347  012of  13363  2o01f  13364  subctctexmid  13369  nninfall  13379  nninfsellemqall  13386  nninfsellemeqinf  13387  nninfomnilem  13389  nninfomni  13390  exmidsbthrlem  13392  sbthom  13396  isomninnlem  13400  isomninn  13401  cvgcmp2nlemabs  13402  trilpolemisumle  13406  trilpolemeq1  13408  trilpo  13411  trirec0  13412  apdifflemr  13415  iswomninnlem  13417  iswomninn  13418  ismkvnnlem  13419  ismkvnn  13420  redcwlpo  13422  neapmkv  13425  iooreen  13427  taupi  13430