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 663.

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  111  simpri  113  biimpi  120  bicomi  132  mpbi  145  mpbir  146  imbi1i  238  a1bi  243  tbt  247  biantru  302  biantrur  303  mp2an  426  pm2.65i  640  notnoti  646  pm2.21i  647  pm2.24ii  648  notbii  669  nbn  700  ori  724  orci  732  olci  733  biorfi  747  imorri  750  dcbii  841  simp1i  1008  simp2i  1009  simp3i  1010  3mix1i  1171  3mix2i  1172  3mix3i  1173  3jaoi  1314  mptru  1373  dfnot  1382  mptnan  1434  mtpor  1436  mtpxor  1437  mpg  1462  19.23h  1509  hbequid  1524  axi12  1525  nfri  1530  spi  1547  19.21  1594  eximii  1613  19.35i  1636  nfn  1669  19.37aiv  1686  19.23  1689  exan  1704  equid  1712  hbae  1729  equvini  1769  equveli  1770  sbid  1785  sbieh  1801  exdistrfor  1811  dveeq2or  1827  ax11v  1838  ax11ev  1839  equs5or  1841  sb4or  1844  sb4bor  1846  nfsb2or  1848  sbequilem  1849  sbequi  1850  speiv  1873  nfsbxy  1958  nfsbxyt  1959  sbco  1984  sbcocom  1986  sbcomxyyz  1988  sbal1yz  2017  dvelimALT  2026  dvelimfv  2027  dvelimor  2034  eumoi  2075  moani  2112  elsb1  2171  elsb2  2172  eqeq1i  2201  eqeq2i  2204  eleq1i  2259  eleq2i  2260  nfcrii  2329  neeq1i  2379  neeq2i  2380  necon3i  2412  rspec  2546  rgen2a  2548  mprg  2551  r19.21  2570  r19.23  2602  raleqi  2694  rexeqi  2695  rabeqif  2751  elv  2764  elexi  2772  ceqsal  2789  vtocl3  2817  vtoclef  2834  vtocle  2835  spcv  2855  spcev  2856  clel3  2896  elabf  2904  elab2  2909  elab3  2913  euxfrdc  2947  reueq  2960  rmoimi2  2964  sbsbc  2990  sbc8g  2994  sbc6  3012  sbcie  3021  sbcrex  3066  csbvarg  3109  csbief  3126  csbie2  3131  sbnfc2  3142  sseli  3176  sselii  3177  sseq1i  3206  sseq2i  3207  difeq1i  3274  difeq2i  3275  uneq1i  3310  uneq2i  3311  ineq1i  3357  ineq2i  3358  ssinss1  3389  difdif2ss  3417  n0ii  3456  ne0ii  3457  vn0  3458  vn0m  3459  abf  3491  disj2  3503  difid  3516  0dif  3519  disjdif  3520  difin0  3521  undif1ss  3522  difdifdirss  3532  iftruei  3564  iffalsei  3567  ifbieq2i  3581  ifbieq12i  3583  pweqi  3606  pwid  3617  sneqi  3631  elsn  3635  elpr  3640  elsn2  3653  ralsn  3662  rexsn  3663  eltp  3667  rabrsndc  3687  preq1i  3699  preq2i  3700  prid1  3725  snnz  3738  snm  3739  prnz  3741  prm  3742  tpnz  3744  snss  3754  snsssn  3788  opeq1i  3808  opeq2i  3809  unieqi  3846  unissi  3859  inteqi  3875  intmin2  3897  intab  3900  intsn  3906  iinconstm  3922  iuniin  3923  iinss1  3925  iunxdif2  3962  ssiinf  3963  iinss  3965  iinss2  3966  iinab  3975  iundif2ss  3979  iindif2m  3981  iinin2m  3982  iunxsn  3990  iunxprg  3994  iinpw  4004  sndisj  4026  disjxsn  4028  breqi  4036  breq1i  4037  breq2i  4038  brab1  4077  opabbii  4097  truni  4142  bm1.3ii  4151  a9evsep  4152  ax9vsep  4153  zfnuleu  4154  axnul  4155  ssexi  4168  rabex  4174  rabex2  4176  elpw2  4187  pwnss  4189  iin0r  4199  intv  4200  pwex  4213  snex  4215  notnotsnex  4217  ord3ex  4220  dtruarb  4221  undifexmid  4223  intid  4254  opnzi  4265  copsexg  4274  opelopabf  4306  epelc  4323  elon  4406  inton  4425  onn0  4432  onm  4433  elsuc  4438  elsuc2  4439  sucid  4449  iunsuc  4452  onordi  4458  ontrci  4459  onelssi  4461  eusvnf  4485  ssonunii  4522  sucex  4532  onssi  4548  onsuci  4549  ordtriexmidlem  4552  ordtriexmidlem2  4553  ordtriexmid  4554  ontriexmidim  4555  ordtri2orexmid  4556  2ordpr  4557  ontr2exmid  4558  onsucsssucexmid  4560  onsucelsucexmid  4563  regexmidlemm  4565  reg2exmid  4569  onirri  4576  ruALT  4584  onprc  4585  sucon  4586  dtru  4593  0elsucexmid  4598  ordpwsucexmid  4603  ordtri2or2exmid  4604  ontri2orexmidim  4605  dcextest  4614  omex  4626  find  4632  omelon  4642  nnoni  4644  limom  4647  nnregexmid  4654  omsinds  4655  xpeq1i  4680  xpeq2i  4681  0nelxp  4688  opthprc  4711  mosubop  4726  releqi  4743  relssi  4751  relin1  4778  relin2  4779  reldif  4780  inopab  4795  difopab  4796  xpiindim  4800  opabbi2dv  4812  ideq  4815  coeq1i  4822  coeq2i  4823  cnveqi  4838  eldm  4860  eldm2  4861  dmeqi  4864  dmv  4879  rneqi  4891  elrnmpti  4916  dmex  4929  rnex  4930  reseq1i  4939  reseq2i  4940  residm  4975  resex  4984  resmpt3  4992  imaeq1i  5003  imaeq2i  5004  elima  5011  imaex  5021  elimasn  5033  args  5035  epini  5037  dfse2  5039  eliniseg2  5046  relbrcnv  5047  cotr  5048  issref  5049  cnvsym  5050  asymref  5052  intirr  5053  codir  5055  qfto  5056  ssrnres  5109  cnveq0  5123  cnvsn0  5135  dmsnop  5140  rnsnop  5147  resdm2  5157  dfco2a  5167  cocnvcnv1  5177  coi2  5183  coires1  5184  cnvssrndm  5188  cossxp  5189  cocnvres  5191  relrelss  5193  relcoi2  5197  unidmrn  5199  dfdm2  5201  unixpm  5202  cnvexg  5204  cnvex  5205  cnviinm  5208  iotaval  5227  funeqi  5276  funi  5287  funres  5296  funcnvsn  5300  funcnvcnv  5314  funin  5326  funcnvres  5328  isarep2  5342  fneq1i  5349  fneq2i  5350  fnresdisj  5365  fnresi  5372  mpt0  5382  dmmpti  5384  feq1i  5397  feq2i  5398  fdmi  5412  fun2  5428  fssres  5430  resasplitss  5434  fintm  5440  fconst6  5454  f1ores  5516  foimacnv  5519  resdif  5523  funcocnv2  5526  f1ovi  5540  fveq1i  5556  fveq2i  5558  0fv  5591  fvun1  5624  fvopab3ig  5632  fvmptss2  5633  mptrcl  5641  elfvmptrab1  5653  fndmdif  5664  fneqeql2  5668  f1oresrab  5724  fmptco  5725  fnressn  5745  fressnfv  5746  fmptap  5749  fvsnun1  5756  fvsnun2  5757  fsnunfv  5760  fconst2  5776  mptex  5785  riotabiia  5892  acexmidlema  5910  acexmidlemb  5911  acexmidlemcase  5914  acexmidlem2  5916  acexmidlemv  5917  oveq1i  5929  oveq2i  5930  oveqi  5932  oprabidlem  5950  0neqopab  5964  oprabbii  5974  oprabss  6005  mpompt  6011  funoprab  6019  fnoprab  6022  ovigg  6040  elmpocl  6115  resfunexgALT  6162  cofunexg  6163  mptexw  6167  opabex3d  6175  opabex3  6176  1st0  6199  2nd0  6200  op1st  6201  op2nd  6202  f1stres  6214  f2ndres  6215  fo1stresm  6216  fo2ndresm  6217  1stcof  6218  2ndcof  6219  1stexg  6222  2ndexg  6223  releldm2  6240  reldm  6241  dfoprab3  6246  mpomptsx  6252  mpompts  6253  fnmpoi  6258  dmmpo  6259  mpoexxg  6265  mpoexw  6268  1stconst  6276  2ndconst  6277  dfmpo  6278  algrflem  6284  algrflemg  6285  cnvoprab  6289  f1od2  6290  mpoxopn0yelv  6294  mpoxopoveq  6295  tposssxp  6304  brtpos2  6306  reldmtpos  6308  dftpos2  6316  dftpos4  6318  tpostpos  6319  tpostpos2  6320  tposfo  6326  tposf  6327  tposeqi  6332  tposex  6333  tposoprab  6335  issmo  6343  smores  6347  smores2  6349  iordsmo  6352  smo0  6353  tfrlem8  6373  tfrexlem  6389  tfr1onlem3  6393  tfr1onlemsucaccv  6396  tfr1onlembxssdm  6398  tfr1onlemres  6404  tfri1dALT  6406  tfri2  6421  rdgisuc1  6439  rdg0  6442  frecfun  6450  frec0g  6452  freccllem  6457  frecfcllem  6459  frecsuclem  6461  frecrdg  6463  2on0  6481  xp01disj  6488  2oconcl  6494  fnoa  6502  oaexg  6503  fnom  6505  omexg  6506  fnoei  6507  oeiexg  6508  oei0  6514  oacl  6515  oasuc  6519  o1p1e2  6523  omsuc  6527  nna0r  6533  nnm0r  6534  1onn  6575  2onn  6576  3onn  6577  4onn  6578  2ssom  6579  eqerlem  6620  eceq2i  6627  elqs  6642  qsex  6648  ecqs  6653  iinerm  6663  th3qlem1  6693  th3q  6696  mapsn  6746  mapsnf1o3  6753  ixpiinm  6780  ixpssmap  6788  brdom  6806  f1dom  6816  enref  6821  dom2  6831  idssen  6833  ssdomg  6834  ensymi  6838  ensn1  6852  fiprc  6871  1domsn  6875  xpcomf1o  6881  xpcomco  6882  dom0  6896  0dom  6897  xpmapenlem  6907  phplem2  6911  php5  6916  snnen2og  6917  1nen2  6919  php5dom  6921  ssfilem  6933  ssfiexmid  6934  domfiexmid  6936  0fin  6942  diffitest  6945  findcard  6946  findcard2  6947  findcard2s  6948  isinfinf  6955  ac6sfi  6956  inffiexmid  6964  pw1fin  6968  unfiexmid  6976  xpfi  6988  fisseneq  6990  ssfirab  6992  residfi  7001  en1eqsn  7009  snexxph  7011  sbthlem2  7019  sbthlemi3  7020  sbthlemi6  7023  sbthlem7  7024  fi0  7036  supeq1i  7049  infeq1i  7074  djuexb  7105  djuf1olemr  7115  inresflem  7121  djuinr  7124  updjudhcoinlf  7141  updjudhcoinrg  7142  casefun  7146  caserel  7148  caseinj  7150  caseinl  7152  caseinr  7153  omp1eomlem  7155  endjusym  7157  difinfsn  7161  difinfinf  7162  djuinj  7167  0ct  7168  ctmlemr  7169  ctssdclemn0  7171  ctssdccl  7172  omct  7178  ctfoex  7179  finomni  7201  exmidomni  7203  fodjuomni  7210  ctssexmid  7211  fodjumkv  7221  nninfwlporlem  7234  nninfwlpoimlemg  7236  nninfwlpoim  7239  card0  7250  exmidonfinlem  7255  dju1p1e2  7259  exmidfodomrlemim  7263  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  3nelsucpw1  7296  sucpw1nss3  7297  3nsssucpw1  7298  2onetap  7317  exmidmotap  7323  0npi  7375  dmaddpi  7387  dmmulpi  7388  1lt2pi  7402  0nnq  7426  1nq  7428  dmaddpq  7441  dmmulpq  7442  rec1nq  7457  1lt2nq  7468  halfnqq  7472  prarloclemarch2  7481  enq0enq  7493  nqnq0pi  7500  nnnq0lem1  7508  addnnnq0  7511  mulnnnq0  7512  nq0m0r  7518  addpinq1  7526  prarloclem5  7562  prarloclemcalc  7564  1pr  7616  1idprl  7652  1idpru  7653  ltexprlemm  7662  recexprlem1ssl  7695  recexprlem1ssu  7696  suplocexprlemell  7775  suplocexprlem2b  7776  suplocexprlemmu  7780  suplocexprlemdisj  7782  suplocexprlemloc  7783  suplocexprlemub  7785  suplocexprlemlub  7786  prsrlem1  7804  addsrpr  7807  mulsrpr  7808  gt0srpr  7810  0nsr  7811  0r  7812  1sr  7813  m1r  7814  m1m1sr  7823  caucvgsr  7864  suplocsrlempr  7869  addresr  7899  mulresr  7900  pitonnlem1  7907  peano1nnnn  7914  axi2m1  7937  axcnre  7943  peano5nnnn  7954  axcaucvg  7962  mpomulf  8011  mulid1i  8023  mullidi  8024  pnfnre  8063  mnfnre  8064  pnfnemnf  8076  mnfxr  8078  rexri  8079  ltnri  8114  ltleii  8124  00id  8162  addid1i  8163  addid2i  8164  0cnALT  8211  negeqi  8215  negicn  8222  neg0  8267  renegcli  8283  negcli  8289  negidi  8290  negnegi  8291  subidi  8292  subid1i  8293  negne0bi  8294  negrebi  8295  mul02i  8411  mul01i  8412  mulm1i  8424  leidi  8506  gt0ne0ii  8508  inelr  8605  msqge0i  8638  gt0ap0ii  8649  1div1e1  8725  div1i  8761  eqnegi  8762  recclapi  8763  recidapi  8764  divmulapi  8787  rerecclapi  8798  redivclapi  8800  rerecapb  8864  recgt0  8871  ltp1i  8926  divgt0ii  8940  ltmul1ii  8949  ltdiv1ii  8950  sup3exmid  8978  peano5nni  8987  nnrei  8993  1nn  8995  nngt0i  9014  neg1ap0  9093  2timesi  9114  times2i  9115  2nn  9146  3nn  9147  4nn  9148  5nn  9149  6nn  9150  7nn  9151  8nn  9152  9nn  9153  2muline0  9210  rehalfcli  9234  nn0ssre  9247  nnnn0i  9251  dfn2  9256  0nn0  9258  nn0ge0i  9270  zrei  9326  neg1z  9352  nn0negzi  9355  dfz2  9392  nneoi  9424  peano5uzi  9429  dfuzi  9430  nn0ind-raph  9437  deceq1i  9457  deceq2i  9458  10nn  9466  numltc  9476  eluzel2  9600  eluz1i  9602  nn0uz  9630  nnuz  9631  infrenegsupex  9662  lbzbi  9684  divfnzn  9689  qdivcl  9711  irrmul  9715  irrmulap  9716  cnref1o  9719  0ltpnf  9851  mnflt0  9853  0lepnf  9859  xrltnsym  9862  xrlttri3  9866  nltpnft  9883  ngtmnft  9886  xrrebnd  9888  xnegmnf  9898  xneg0  9900  xltnegi  9904  xaddmnf1  9917  xaddmnf2  9918  mnfaddpnf  9920  xaddid1  9931  xnn0lenn0nn0  9934  xnn0xadd0  9936  xposdif  9951  ixxex  9968  iooval2  9984  unirnioo  10042  ioorebasg  10044  elrege0  10045  fzval2  10080  fzen  10112  fzprval  10151  fztpval  10152  uzdisj  10162  ige2m1fz  10179  fz01or  10180  fz1ssfz0  10186  fz0sn  10190  fz0tp  10191  fz0to3un2pr  10192  fz0to4untppr  10193  nn0disj  10207  1fv  10208  4fvwrd4  10209  fzo0ss1  10244  fzo01  10286  fzo12sn  10287  fzo0to2pr  10288  fzo0to3tp  10289  fzo0to42pr  10290  qbtwnxr  10329  flval  10344  fldiv4lem1div2  10379  modqfrac  10411  modqmulnn  10416  q2txmodxeq0  10458  frecuzrdgdom  10492  frecuzrdgfun  10494  frecuzrdgsuct  10498  frechashgf1o  10502  nnct  10509  xnn0nnen  10511  fxnn0nninf  10513  0tonninf  10514  1tonninf  10515  iseqvalcbv  10533  ser0f  10608  0exp0e1  10618  qexpcl  10629  qexpclz  10634  m1expcl2  10635  1exp  10642  sqvali  10693  sqcli  10694  sqeq0i  10695  resqcli  10698  sq1  10707  neg1sqe1  10708  iexpcyc  10718  qsqeqor  10724  facnn  10801  fac0  10802  fac1  10803  fac2  10805  fac3  10806  fac4  10807  bcval  10823  bcm1k  10834  bcpasc  10840  bccl  10841  4bc3eq4  10847  4bc2eq6  10848  hashinfom  10852  hashennn  10854  hashfz1  10857  fihasheq0  10867  hash0  10870  hashsng  10872  fihashen1  10873  omgadd  10876  hashp1i  10884  hashxp  10900  fimaxq  10901  zfz1iso  10915  wrdexi  10930  wrdv  10933  wrdeqi  10940  wrd0  10942  shftidt2  10979  cjexp  11040  re0  11042  im0  11043  re1  11044  im1  11045  cj0  11048  cji  11049  recli  11058  imcli  11059  cjcli  11060  replimi  11061  cjcji  11062  reim0bi  11063  rerebi  11064  cjrebi  11065  recji  11066  imcji  11067  cjmulrcli  11068  cjmulvali  11069  cjmulge0i  11070  renegi  11071  imnegi  11072  cjnegi  11073  addcji  11074  uzin2  11134  rexanuz  11135  rexfiuz  11136  sqrtrval  11147  sqrt0  11151  resqrexlemcalc3  11163  resqrexlemcvg  11166  resqrex  11173  abs0  11205  absi  11206  qabsor  11222  absimle  11231  recan  11256  caubnd2  11264  leabsi  11275  absrei  11276  sqrtpclii  11277  sqrtgt0ii  11278  absvalsqi  11287  absvalsq2i  11288  abscli  11289  absge0i  11290  absval2i  11291  abs00i  11292  absgt0api  11293  absnegi  11294  abscji  11295  releabsi  11296  infxrnegsupex  11409  xrbdtri  11422  cbvsum  11506  sumeq1i  11509  sum0  11534  isumz  11535  fisumss  11538  fsumsersdc  11541  fsumadd  11552  isumclim  11567  isumclim3  11569  fsumcnv  11583  modfsummodlem1  11602  fsumrelem  11617  binomlem  11629  binom  11630  arisum2  11645  expcnv  11650  0.999...  11667  prodf1f  11689  cbvprod  11704  prodeq1i  11707  zproddc  11725  zprodap0  11727  prod0  11731  fprodssdc  11736  prodsnf  11738  fprodcnv  11771  fprodge0  11783  fprodge1  11785  ef0lem  11806  esum  11808  ere  11816  ege2le3  11817  ef0  11818  eff2  11826  efsep  11837  reeff1  11846  sin0  11875  cos0  11876  ef01bndlem  11902  cos2bnd  11906  sincos1sgn  11911  sincos2sgn  11912  sin4lt0  11913  eirr  11925  0dvds  11957  dvds1  11998  z0even  12055  n2dvdsm1  12057  z2even  12058  n2dvds3  12059  ndvdssub  12074  ndvdsi  12077  flodddiv4  12078  zsupssdc  12094  gcddvds  12103  gcd1  12127  6gcd4e2  12135  bezoutlembi  12145  dfgcd3  12150  dfgcd2  12154  nninfctlemfo  12180  nninfct  12181  3lcm2e6woprm  12227  qredeu  12238  isprm2lem  12257  isprm3  12259  prm2orodd  12267  isprm5lem  12282  sqrt2irr0  12305  pw2dvds  12307  phicl2  12355  phi1  12360  dfphi2  12361  phiprmpw  12363  eulerthlemrprm  12370  eulerthlemh  12372  odzval  12382  oddprm  12400  pczpre  12438  pcdiv  12443  pc0  12445  pcqdiv  12448  pcrec  12449  pcexp  12450  pcxcl  12452  pcxqcl  12453  pcdvdstr  12468  pc2dvds  12471  dvdsprmpweqnn  12477  pcmpt  12484  qexpz  12493  pockthi  12499  1arith2  12509  4sqlemffi  12537  4sqlem11  12542  4sqlem13m  12544  4sqlem19  12550  ennnfonelemp1  12566  ennnfonelem1  12567  ennnfonelemkh  12572  ennnfonelemex  12574  ennnfonelemnn0  12582  ennnfonelemr  12583  exmidunben  12586  ctinfomlemom  12587  ctinfom  12588  ctinf  12590  qnnen  12591  omctfn  12603  omiunct  12604  ssnnctlemct  12606  nninfdc  12613  structcnvcnv  12637  structfun  12639  structfn  12640  ndxarg  12644  ndxid  12645  setsresg  12659  setsslnid  12673  basmex  12680  basmexd  12681  strleun  12725  strle1g  12727  prdsex  12883  imasaddfnlemg  12900  quslem  12910  xpsfrnel  12930  xpsff1o  12935  ismgmn0  12944  fn0g  12961  0g0  12962  fngsum  12974  idghm  13332  rhmfn  13671  rmodislmodlem  13849  rmodislmod  13850  lidlmex  13974  mopnset  14051  cntopex  14053  cnfldex  14058  cnfldbas  14059  mpocnfldadd  14060  mpocnfldmul  14062  cnfldcj  14064  cnfldtset  14065  cnfldle  14066  cnfldds  14067  cnring  14069  cnfld0  14070  cnfld1  14071  cnfldneg  14072  cnfldplusf  14073  cnfldsub  14074  cnfldmulg  14075  cnfldexp  14076  cnsubglem  14078  cnsubrglem  14079  gzsubrg  14081  gsumfzfsumlem0  14085  cnfldui  14088  zringring  14092  zringabl  14093  zringgrp  14094  zring1  14100  zringsubgval  14104  expghmap  14106  znval  14135  znle  14136  znbaslemnn  14138  znbas  14143  znzrh2  14145  znzrhval  14146  znzrhfo  14147  znleval  14152  znidom  14156  znidomb  14157  fnpsr  14164  psrelbas  14171  psradd  14174  psraddcl  14175  istopon  14192  topontopi  14195  toponunii  14196  toponrestid  14200  istps  14211  topontopn  14216  eltpsi  14220  eltg4i  14234  eltg3  14236  tg1  14238  tg2  14239  tgclb  14244  topnex  14265  sn0topon  14267  distps  14270  cldrcl  14281  sn0cld  14316  restco  14353  lmrcl  14370  ssidcn  14389  cnconst2  14412  cnptopresti  14417  cnptoprest  14418  txuni2  14435  txbas  14437  eltx  14438  txcnp  14450  upxp  14451  txcnmpt  14452  uptx  14453  txcn  14454  txrest  14455  txlm  14458  cnmptid  14460  cnmpt1st  14467  cnmpt2nd  14468  hmeofn  14481  psmetge0  14510  ismeti  14525  xmetunirn  14537  xmetge0  14544  unirnblps  14601  unirnbl  14602  mopnex  14684  qtopbasss  14700  retop  14703  uniretop  14704  iooretopg  14707  cnxmet  14710  cntoptopon  14711  cnbl0  14713  cnfldxms  14716  cnfldtps  14717  rexmet  14728  blssioo  14732  tgioo  14733  tgqioo  14734  cnopnap  14790  hovercncf  14825  limcresi  14845  dvfvalap  14860  dvidlemap  14870  dvidrelem  14871  dvidsslem  14872  dvcnp2cntop  14878  dvcoapbr  14886  dvexp2  14891  dvrecap  14892  dveflem  14905  dvef  14906  plyun0  14915  plyrecj  14941  reeff1o  14949  sin0pilem1  14957  sin0pilem2  14958  pilem3  14959  pigt2lt4  14960  pire  14962  sinhalfpilem  14967  pidiv2halves  14971  cosneghalfpi  14974  cospi  14976  efipi  14977  sin2pi  14979  cos2pi  14980  ef2pi  14981  cosq14gt0  15008  coseq00topi  15011  coseq0negpitopi  15012  sincos4thpi  15016  sincos6thpi  15018  sincos3rdpi  15019  pigt3  15020  cos02pilt1  15027  ioocosf1o  15030  dfrelog  15036  relogf1o  15037  relogcl  15038  relogiso  15049  rpcxpsqrt  15097  rpabscxpbnd  15114  2logb9irr  15144  2logb9irrALT  15147  sqrt2cxp2logb9e3  15148  2irrexpq  15149  2logb9irrap  15150  2irrexpqap  15151  lgsdir2lem1  15185  lgsdir2lem2  15186  lgsdir2lem4  15188  lgsdir2lem5  15189  lgsdi  15194  gausslemma2dlem0i  15214  gausslemma2dlem4  15221  lgseisenlem4  15230  lgsquadlem1  15234  lgsquad2lem2  15239  lgsquad2  15240  m1lgs  15242  2lgs2  15259  2lgslem4  15260  2lgsoddprmlem2  15263  2lgsoddprmlem3c  15266  2lgsoddprmlem3d  15267  2sqlem9  15281  2sqlem10  15282  ex-fl  15287  ex-ceil  15288  ex-exp  15289  ex-fac  15290  ex-gcd  15293  bj-stfal  15304  bj-stst  15307  bj-dcfal  15317  bj-dcdc  15321  bj-stdc  15322  bj-dcst  15323  bj-el2oss1o  15336  elabf2  15344  bd0  15386  bdeli  15408  bdcriota  15445  bdbm1.3ii  15453  bdinex1  15461  bdssexi  15465  bj-inex  15469  bj-snex  15475  bj-sucex  15485  bj-d0clsepcl  15487  bj-omind  15496  bj-om  15499  bj-2inf  15500  bj-peano2  15501  bdpeano5  15505  bj-omssonALT  15525  bj-inf2vnlem1  15532  bj-omex2  15539  bj-nn0sucALT  15540  012of  15556  2o01f  15557  subctctexmid  15561  nninfall  15569  nninfsellemqall  15575  nninfsellemeqinf  15576  nninfomnilem  15578  nninfomni  15579  exmidsbthrlem  15582  sbthom  15586  isomninnlem  15590  isomninn  15591  cvgcmp2nlemabs  15592  iooreen  15595  trilpolemisumle  15598  trilpolemeq1  15600  trilpo  15603  trirec0  15604  apdifflemr  15607  iswomninnlem  15609  iswomninn  15610  ismkvnnlem  15612  ismkvnn  15613  redcwlpo  15615  dcapnconst  15621  nconstwlpolem0  15623  nconstwlpo  15626  neapmkv  15628  neap0mkv  15629  taupi  15633