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 ph is true, and ph implies ps, then ps 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 666.

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	|- ph
maj	|- ( ph -> ps )

Assertion

Ref	Expression
ax-mp	|- ps

Detailed syntax breakdown of Axiom ax-mp

Step	Hyp	Ref	Expression
1		wps	1 wff ps

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  642  notnoti  648  pm2.21i  649  pm2.24ii  650  notbii  672  nbn  704  ori  728  orci  736  olci  737  biorfi  751  imorri  754  dcbii  845  simp1i  1030  simp2i  1031  simp3i  1032  3mix1i  1193  3mix2i  1194  3mix3i  1195  3jaoi  1337  mptru  1404  dfnot  1413  mptnan  1465  mtpor  1467  mtpxor  1468  dcfromnotnotr  1490  dcfromcon  1491  dcfrompeirce  1492  mpg  1497  19.23h  1544  hbequid  1559  axi12  1560  nfri  1565  spi  1582  19.21  1629  eximii  1648  19.35i  1671  nfn  1704  19.37aiv  1721  19.23  1724  exan  1739  equid  1747  hbae  1764  equvini  1804  equveli  1805  sbid  1820  sbieh  1836  exdistrfor  1846  dveeq2or  1862  ax11v  1873  ax11ev  1874  equs5or  1876  sb4or  1879  sb4bor  1881  nfsb2or  1883  sbequilem  1884  sbequi  1885  speiv  1908  nfsbxy  1993  nfsbxyt  1994  sbco  2019  sbcocom  2021  sbcomxyyz  2023  sbal1yz  2052  dvelimALT  2061  dvelimfv  2062  dvelimor  2069  eumoi  2110  moani  2148  elsb1  2207  elsb2  2208  eqeq1i  2237  eqeq2i  2240  eleq1i  2295  eleq2i  2296  nfcrii  2365  neeq1i  2415  neeq2i  2416  necon3i  2448  rspec  2582  rgen2a  2584  mprg  2587  r19.21  2606  r19.23  2639  raleqi  2732  rexeqi  2733  rabeqif  2790  elv  2803  elexi  2812  ceqsal  2829  vtocl3  2857  vtoclef  2876  vtocle  2877  spcv  2897  spcev  2898  clel3  2938  elabf  2946  elab2  2951  elab3  2955  euxfrdc  2989  reueq  3002  rmoimi2  3006  sbsbc  3032  sbc8g  3036  sbc6  3054  sbcie  3063  sbcrex  3108  csbvarg  3152  csbief  3169  csbie2  3174  sbnfc2  3185  sseli  3220  sselii  3221  sseq1i  3250  sseq2i  3251  difeq1i  3318  difeq2i  3319  uneq1i  3354  uneq2i  3355  ineq1i  3401  ineq2i  3402  ssinss1  3433  difdif2ss  3461  n0ii  3500  ne0ii  3501  vn0  3502  vn0m  3503  abf  3535  disj2  3547  difid  3560  0dif  3563  disjdif  3564  difin0  3565  undif1ss  3566  difdifdirss  3576  iftruei  3608  iffalsei  3611  ifbieq2i  3626  ifbieq12i  3628  pweqi  3653  pwid  3664  sneqi  3678  elsn  3682  elpr  3687  elsn2  3700  ralsn  3709  rexsn  3710  eltp  3714  rabrsndc  3734  preq1i  3746  preq2i  3747  prid1  3772  snnz  3786  snm  3787  prnz  3790  prm  3791  tpnz  3793  snss  3803  snsssn  3839  opeq1i  3860  opeq2i  3861  unieqi  3898  unissi  3911  inteqi  3927  intmin2  3949  intab  3952  intsn  3958  iinconstm  3974  iuniin  3975  iinss1  3977  iunxdif2  4014  ssiinf  4015  iinss  4017  iinss2  4018  iinab  4027  iundif2ss  4031  iindif2m  4033  iinin2m  4034  iunxsn  4042  iunxprg  4046  iinpw  4056  invdisjrab  4077  sndisj  4079  disjxsn  4081  breqi  4089  breq1i  4090  breq2i  4091  brab1  4131  opabbii  4151  truni  4196  bm1.3ii  4205  a9evsep  4206  ax9vsep  4207  zfnuleu  4208  axnul  4209  ssexi  4222  rabex  4228  rabex2  4230  elpw2  4241  pwnss  4243  iin0r  4253  intv  4254  pwex  4267  snex  4269  notnotsnex  4271  ord3ex  4274  dtruarb  4275  undifexmid  4277  intid  4310  opnzi  4321  copsexg  4330  opwo0id  4335  opelopabf  4363  epelc  4382  elon  4465  inton  4484  onn0  4491  onm  4492  elsuc  4497  elsuc2  4498  sucid  4508  iunsuc  4511  onordi  4517  ontrci  4518  onelssi  4520  eusvnf  4544  ssonunii  4581  sucex  4591  onssi  4607  onsuci  4608  ordtriexmidlem  4611  ordtriexmidlem2  4612  ordtriexmid  4613  ontriexmidim  4614  ordtri2orexmid  4615  2ordpr  4616  ontr2exmid  4617  onsucsssucexmid  4619  onsucelsucexmid  4622  regexmidlemm  4624  reg2exmid  4628  onirri  4635  ruALT  4643  onprc  4644  sucon  4645  dtru  4652  0elsucexmid  4657  ordpwsucexmid  4662  ordtri2or2exmid  4663  ontri2orexmidim  4664  dcextest  4673  omex  4685  find  4691  omelon  4701  nnoni  4703  limom  4706  nnregexmid  4713  omsinds  4714  xpeq1i  4739  xpeq2i  4740  0nelxp  4747  opthprc  4770  mosubop  4785  releqi  4802  relssi  4810  relin1  4837  relin2  4838  reldif  4839  inopab  4854  difopab  4855  xpiindim  4859  opabbi2dv  4871  ideq  4874  coeq1i  4881  coeq2i  4882  cnveqi  4897  eldm  4920  eldm2  4921  dmeqi  4924  dmv  4939  rneqi  4952  elrnmpti  4977  dmex  4991  rnex  4992  reseq1i  5001  reseq2i  5002  residm  5037  resex  5046  resmpt3  5054  imaeq1i  5065  imaeq2i  5066  elima  5073  imaex  5083  elimasn  5095  args  5097  epini  5099  dfse2  5101  eliniseg2  5108  relbrcnv  5109  cotr  5110  issref  5111  cnvsym  5112  asymref  5114  intirr  5115  codir  5117  qfto  5118  ssrnres  5171  cnveq0  5185  cnvsn0  5197  dmsnop  5202  rnsnop  5209  resdm2  5219  dfco2a  5229  cocnvcnv1  5239  coi2  5245  coires1  5246  cnvssrndm  5250  cossxp  5251  cocnvres  5253  relrelss  5255  relcoi2  5259  unidmrn  5261  dfdm2  5263  unixpm  5264  cnvexg  5266  cnvex  5267  cnviinm  5270  iotaval  5290  funeqi  5339  funi  5350  funres  5359  funcnvsn  5366  funcnvcnv  5380  funin  5392  funcnvres  5394  isarep2  5408  fneq1i  5415  fneq2i  5416  fndmi  5421  fnresdisj  5433  fnresi  5441  mpt0  5451  dmmpti  5453  feq1i  5466  feq2i  5467  fdmi  5481  fun2  5500  fssres  5503  resasplitss  5507  fintm  5513  fconst6  5527  f1ores  5589  foimacnv  5592  resdif  5596  funcocnv2  5599  f10d  5609  f1ovi  5614  fveq1i  5630  fveq2i  5632  0fv  5667  fvun1  5702  fvopab3ig  5710  fvmptss2  5711  mptrcl  5719  elfvmptrab1  5731  fndmdif  5742  fneqeql2  5746  f1oresrab  5802  fmptco  5803  funopsn  5819  fnressn  5829  fressnfv  5830  fmptap  5833  fvsnun1  5840  fvsnun2  5841  fsnunfv  5844  fconst2  5860  mptex  5869  fnfvimad  5879  riotabiia  5979  acexmidlema  5998  acexmidlemb  5999  acexmidlemcase  6002  acexmidlem2  6004  acexmidlemv  6005  oveq1i  6017  oveq2i  6018  oveqi  6020  oprabidlem  6038  0neqopab  6055  oprabbii  6065  oprabss  6096  mpompt  6102  funoprab  6110  fnoprab  6113  ovigg  6131  elmpocl  6206  relmptopab  6213  resfunexgALT  6259  cofunexg  6260  mptexw  6264  opabex3d  6272  opabex3  6273  1st0  6296  2nd0  6297  op1st  6298  op2nd  6299  f1stres  6311  f2ndres  6312  fo1stresm  6313  fo2ndresm  6314  1stcof  6315  2ndcof  6316  1stexg  6319  2ndexg  6320  releldm2  6337  reldm  6338  dfoprab3  6343  mpomptsx  6349  mpompts  6350  fnmpoi  6355  dmmpo  6356  mpoexxg  6362  mpoexw  6365  1stconst  6373  2ndconst  6374  dfmpo  6375  algrflem  6381  algrflemg  6382  cnvoprab  6386  f1od2  6387  mpoxopn0yelv  6391  mpoxopoveq  6392  tposssxp  6401  brtpos2  6403  reldmtpos  6405  dftpos2  6413  dftpos4  6415  tpostpos  6416  tpostpos2  6417  tposfo  6423  tposf  6424  tposeqi  6429  tposex  6430  tposoprab  6432  issmo  6440  smores  6444  smores2  6446  iordsmo  6449  smo0  6450  tfrlem8  6470  tfrexlem  6486  tfr1onlem3  6490  tfr1onlemsucaccv  6493  tfr1onlembxssdm  6495  tfr1onlemres  6501  tfri1dALT  6503  tfri2  6518  rdgisuc1  6536  rdg0  6539  frecfun  6547  frec0g  6549  freccllem  6554  frecfcllem  6556  frecsuclem  6558  frecrdg  6560  2on0  6578  xp01disj  6587  2oconcl  6593  fnoa  6601  oaexg  6602  fnom  6604  omexg  6605  fnoei  6606  oeiexg  6607  oei0  6613  oacl  6614  oasuc  6618  o1p1e2  6622  omsuc  6626  nna0r  6632  nnm0r  6633  1onn  6674  2onn  6675  3onn  6676  4onn  6677  2ssom  6678  eqerlem  6719  eceq2i  6726  elqs  6741  qsex  6747  ecqs  6752  iinerm  6762  th3qlem1  6792  th3q  6795  mapsn  6845  mapsnf1o3  6852  ixpiinm  6879  ixpssmap  6887  brdom  6907  f1dom  6919  enref  6924  dom2  6934  idssen  6936  ssdomg  6938  ensymi  6942  ensn1  6956  fiprc  6976  1domsn  6984  dom1o  6985  xpcomf1o  6992  xpcomco  6993  dom0  7007  0dom  7008  xpmapenlem  7018  phplem2  7022  php5  7027  snnen2og  7028  1nen2  7030  php5dom  7032  ssfilem  7045  ssfiexmid  7046  domfiexmid  7048  0fin  7054  diffitest  7057  findcard  7058  findcard2  7059  findcard2s  7060  isinfinf  7067  ac6sfi  7068  inffiexmid  7076  pw1fin  7080  unfiexmid  7088  xpfi  7102  fisseneq  7104  ssfirab  7106  residfi  7115  en1eqsn  7123  snexxph  7125  sbthlem2  7133  sbthlemi3  7134  sbthlemi6  7137  sbthlem7  7138  fi0  7150  supeq1i  7163  infeq1i  7188  djuexb  7219  djuf1olemr  7229  inresflem  7235  djuinr  7238  updjudhcoinlf  7255  updjudhcoinrg  7256  casefun  7260  caserel  7262  caseinj  7264  caseinl  7266  caseinr  7267  omp1eomlem  7269  endjusym  7271  difinfsn  7275  difinfinf  7276  djuinj  7281  0ct  7282  ctmlemr  7283  ctssdclemn0  7285  ctssdccl  7286  omct  7292  ctfoex  7293  finomni  7315  exmidomni  7317  fodjuomni  7324  ctssexmid  7325  fodjumkv  7335  nninfwlporlem  7348  nninfwlpoimlemg  7350  nninfwlpoim  7354  nninfinfwlpo  7355  card0  7368  ficardon  7369  exmidonfinlem  7379  dju1p1e2  7383  exmidfodomrlemim  7387  exmidfodomrlemr  7388  exmidfodomrlemrALT  7389  iftrueb01  7416  3nelsucpw1  7427  sucpw1nss3  7428  3nsssucpw1  7429  2onetap  7449  exmidmotap  7455  0npi  7508  dmaddpi  7520  dmmulpi  7521  1lt2pi  7535  0nnq  7559  1nq  7561  dmaddpq  7574  dmmulpq  7575  rec1nq  7590  1lt2nq  7601  halfnqq  7605  prarloclemarch2  7614  enq0enq  7626  nqnq0pi  7633  nnnq0lem1  7641  addnnnq0  7644  mulnnnq0  7645  nq0m0r  7651  addpinq1  7659  prarloclem5  7695  prarloclemcalc  7697  1pr  7749  1idprl  7785  1idpru  7786  ltexprlemm  7795  recexprlem1ssl  7828  recexprlem1ssu  7829  suplocexprlemell  7908  suplocexprlem2b  7909  suplocexprlemmu  7913  suplocexprlemdisj  7915  suplocexprlemloc  7916  suplocexprlemub  7918  suplocexprlemlub  7919  prsrlem1  7937  addsrpr  7940  mulsrpr  7941  gt0srpr  7943  0nsr  7944  0r  7945  1sr  7946  m1r  7947  m1m1sr  7956  caucvgsr  7997  suplocsrlempr  8002  addresr  8032  mulresr  8033  pitonnlem1  8040  peano1nnnn  8047  axi2m1  8070  axcnre  8076  peano5nnnn  8087  axcaucvg  8095  mpomulf  8144  mulridi  8156  mullidi  8157  pnfnre  8196  mnfnre  8197  pnfnemnf  8209  mnfxr  8211  rexri  8212  ltnri  8247  ltleii  8257  00id  8295  addridi  8296  addlidi  8297  0cnALT  8344  negeqi  8348  negicn  8355  neg0  8400  renegcli  8416  negcli  8422  negidi  8423  negnegi  8424  subidi  8425  subid1i  8426  negne0bi  8427  negrebi  8428  mul02i  8544  mul01i  8545  mulm1i  8557  leidi  8640  gt0ne0ii  8642  inelr  8739  msqge0i  8772  gt0ap0ii  8783  1div1e1  8859  div1i  8895  eqnegi  8896  recclapi  8897  recidapi  8898  divmulapi  8921  rerecclapi  8932  redivclapi  8934  rerecapb  8998  recgt0  9005  ltp1i  9060  divgt0ii  9074  ltmul1ii  9083  ltdiv1ii  9084  sup3exmid  9112  peano5nni  9121  nnrei  9127  1nn  9129  nngt0i  9148  neg1ap0  9227  2timesi  9248  times2i  9249  2nn  9280  3nn  9281  4nn  9282  5nn  9283  6nn  9284  7nn  9285  8nn  9286  9nn  9287  2muline0  9344  rehalfcli  9368  nn0ssre  9381  nnnn0i  9385  dfn2  9390  0nn0  9392  nn0ge0i  9404  zrei  9460  neg1z  9486  nn0negzi  9489  dfz2  9527  nneoi  9559  peano5uzi  9564  dfuzi  9565  nn0ind-raph  9572  deceq1i  9592  deceq2i  9593  10nn  9601  numltc  9611  eluzel2  9735  eluz1i  9737  nn0uz  9765  nnuz  9766  infrenegsupex  9797  lbzbi  9819  divfnzn  9824  qdivcl  9846  irrmul  9850  irrmulap  9851  cnref1o  9854  0ltpnf  9986  mnflt0  9988  0lepnf  9994  xrltnsym  9997  xrlttri3  10001  nltpnft  10018  ngtmnft  10021  xrrebnd  10023  xnegmnf  10033  xneg0  10035  xltnegi  10039  xaddmnf1  10052  xaddmnf2  10053  mnfaddpnf  10055  xaddid1  10066  xnn0lenn0nn0  10069  xnn0xadd0  10071  xposdif  10086  ixxex  10103  iooval2  10119  unirnioo  10177  ioorebasg  10179  elrege0  10180  fzval2  10215  fzen  10247  fzprval  10286  fztpval  10287  uzdisj  10297  ige2m1fz  10314  fz01or  10315  fz1ssfz0  10321  fz0sn  10325  fz0tp  10326  fz0to3un2pr  10327  fz0to4untppr  10328  nn0disj  10342  1fv  10343  4fvwrd4  10344  fzo0ss1  10380  fzo01  10430  fzo12sn  10431  fzo0to2pr  10432  fzo0to3tp  10433  fzo0to42pr  10434  zsupssdc  10466  qbtwnxr  10485  flval  10500  fldiv4lem1div2  10535  modqfrac  10567  modqmulnn  10572  q2txmodxeq0  10614  frecuzrdgdom  10648  frecuzrdgfun  10650  frecuzrdgsuct  10654  frechashgf1o  10658  nnct  10665  xnn0nnen  10667  fxnn0nninf  10669  0tonninf  10670  1tonninf  10671  iseqvalcbv  10689  ser0f  10764  0exp0e1  10774  qexpcl  10785  qexpclz  10790  m1expcl2  10791  1exp  10798  sqvali  10849  sqcli  10850  sqeq0i  10851  resqcli  10854  sq1  10863  neg1sqe1  10864  iexpcyc  10874  qsqeqor  10880  facnn  10957  fac0  10958  fac1  10959  fac2  10961  fac3  10962  fac4  10963  bcval  10979  bcm1k  10990  bcpasc  10996  bccl  10997  4bc3eq4  11003  4bc2eq6  11004  hashinfom  11008  hashennn  11010  hashfz1  11013  fihasheq0  11023  hash0  11026  hashsng  11028  fihashen1  11029  omgadd  11032  hashp1i  11040  hashxp  11056  fimaxq  11057  zfz1iso  11071  hash2en  11073  wrdexi  11092  wrdv  11095  wrdeqi  11102  wrd0  11104  lsw0  11127  ccatclab  11137  ccatidid  11153  s1prc  11164  ccat1st1st  11180  swrds1  11208  fnpfx  11217  swrdccatin2  11269  pfxccatin12lem2  11271  cats1fvn  11304  shftidt2  11351  cjexp  11412  re0  11414  im0  11415  re1  11416  im1  11417  cj0  11420  cji  11421  recli  11430  imcli  11431  cjcli  11432  replimi  11433  cjcji  11434  reim0bi  11435  rerebi  11436  cjrebi  11437  recji  11438  imcji  11439  cjmulrcli  11440  cjmulvali  11441  cjmulge0i  11442  renegi  11443  imnegi  11444  cjnegi  11445  addcji  11446  uzin2  11506  rexanuz  11507  rexfiuz  11508  sqrtrval  11519  sqrt0  11523  resqrexlemcalc3  11535  resqrexlemcvg  11538  resqrex  11545  abs0  11577  absi  11578  qabsor  11594  absimle  11603  recan  11628  caubnd2  11636  leabsi  11647  absrei  11648  sqrtpclii  11649  sqrtgt0ii  11650  absvalsqi  11659  absvalsq2i  11660  abscli  11661  absge0i  11662  absval2i  11663  abs00i  11664  absgt0api  11665  absnegi  11666  abscji  11667  releabsi  11668  infxrnegsupex  11782  xrbdtri  11795  cbvsum  11879  sumeq1i  11882  sum0  11907  isumz  11908  fisumss  11911  fsumsersdc  11914  fsumadd  11925  isumclim  11940  isumclim3  11942  fsumcnv  11956  modfsummodlem1  11975  fsumrelem  11990  binomlem  12002  binom  12003  arisum2  12018  expcnv  12023  0.999...  12040  prodf1f  12062  cbvprod  12077  prodeq1i  12080  zproddc  12098  zprodap0  12100  prod0  12104  fprodssdc  12109  prodsnf  12111  fprodcnv  12144  fprodge0  12156  fprodge1  12158  ef0lem  12179  esum  12181  ere  12189  ege2le3  12190  ef0  12191  eff2  12199  efsep  12210  reeff1  12219  sin0  12248  cos0  12249  ef01bndlem  12275  cos2bnd  12279  sincos1sgn  12284  sincos2sgn  12285  sin4lt0  12286  eirr  12298  0dvds  12330  dvds1  12372  z0even  12430  n2dvdsm1  12432  z2even  12433  n2dvds3  12434  ndvdssub  12449  ndvdsi  12452  flodddiv4  12455  bits0  12467  bitsfzo  12474  0bits  12478  m1bits  12479  bitsinv1lem  12480  bitsinv1  12481  gcddvds  12492  gcd1  12516  6gcd4e2  12524  bezoutlembi  12534  dfgcd3  12539  dfgcd2  12543  nninfctlemfo  12569  nninfct  12570  3lcm2e6woprm  12616  qredeu  12627  isprm2lem  12646  isprm3  12648  prm2orodd  12656  isprm5lem  12671  sqrt2irr0  12694  pw2dvds  12696  phicl2  12744  phi1  12749  dfphi2  12750  phiprmpw  12752  eulerthlemrprm  12759  eulerthlemh  12761  odzval  12772  oddprm  12790  pczpre  12828  pcdiv  12833  pc0  12835  pcqdiv  12838  pcrec  12839  pcexp  12840  pcxcl  12842  pcxqcl  12843  pcdvdstr  12858  pc2dvds  12861  dvdsprmpweqnn  12867  pcmpt  12874  qexpz  12883  pockthi  12889  1arith2  12899  4sqlemffi  12927  4sqlem11  12932  4sqlem13m  12934  4sqlem19  12940  dec2dvds  12942  dec5nprm  12945  modxai  12947  modxp1i  12949  numexp0  12953  numexp1  12954  ennnfonelemp1  12985  ennnfonelem1  12986  ennnfonelemkh  12991  ennnfonelemex  12993  ennnfonelemnn0  13001  ennnfonelemr  13002  exmidunben  13005  ctinfomlemom  13006  ctinfom  13007  ctinf  13009  qnnen  13010  omctfn  13022  omiunct  13023  ssnnctlemct  13025  nninfdc  13032  structcnvcnv  13056  structfun  13058  structfn  13059  ndxarg  13063  ndxid  13064  setsresg  13078  setsslnid  13092  basmex  13100  basmexd  13101  strleun  13145  strle1g  13147  prdsex  13310  prdsvallem  13313  prdsval  13314  prdsbaslemss  13315  imasaddfnlemg  13355  quslem  13365  xpsfrnel  13385  xpsff1o  13390  ismgmn0  13399  fn0g  13416  0g0  13417  fngsum  13429  idghm  13804  rhmfn  14144  rmodislmodlem  14322  rmodislmod  14323  lidlmex  14447  mopnset  14524  cntopex  14526  cnfldex  14531  cnfldbas  14532  mpocnfldadd  14533  mpocnfldmul  14535  cnfldcj  14537  cnfldtset  14538  cnfldle  14539  cnfldds  14540  cnring  14542  cnfld0  14543  cnfld1  14544  cnfldneg  14545  cnfldplusf  14546  cnfldsub  14547  cnfldmulg  14548  cnfldexp  14549  cnsubglem  14551  cnsubrglem  14552  gzsubrg  14554  gsumfzfsumlem0  14558  cnfldui  14561  zringring  14565  zringabl  14566  zringgrp  14567  zring1  14573  zringsubgval  14577  expghmap  14579  znval  14608  znle  14609  znbaslemnn  14611  znbas  14616  znzrh2  14618  znzrhval  14619  znzrhfo  14620  znleval  14625  znidom  14629  znidomb  14630  fnpsr  14639  psrelbas  14647  psradd  14651  psraddcl  14652  psr1clfi  14660  mplrcl  14666  mplbasss  14668  mpladd  14676  istopon  14695  topontopi  14698  toponunii  14699  toponrestid  14703  istps  14714  topontopn  14719  eltpsi  14723  eltg4i  14737  eltg3  14739  tg1  14741  tg2  14742  tgclb  14747  topnex  14768  sn0topon  14770  distps  14773  cldrcl  14784  sn0cld  14819  restco  14856  lmrcl  14874  ssidcn  14892  cnconst2  14915  cnptopresti  14920  cnptoprest  14921  txuni2  14938  txbas  14940  eltx  14941  txcnp  14953  upxp  14954  txcnmpt  14955  uptx  14956  txcn  14957  txrest  14958  txlm  14961  cnmptid  14963  cnmpt1st  14970  cnmpt2nd  14971  hmeofn  14984  psmetge0  15013  ismeti  15028  xmetunirn  15040  xmetge0  15047  unirnblps  15104  unirnbl  15105  mopnex  15187  qtopbasss  15203  retop  15206  uniretop  15207  iooretopg  15210  cnxmet  15213  cntoptopon  15214  cnbl0  15216  cnfldxms  15219  cnfldtps  15220  rexmet  15231  blssioo  15235  tgioo  15236  tgqioo  15237  cnopnap  15293  hovercncf  15328  limcresi  15348  dvfvalap  15363  dvidlemap  15373  dvidrelem  15374  dvidsslem  15375  dvcnp2cntop  15381  dvcoapbr  15389  dvexp2  15394  dvrecap  15395  dveflem  15408  dvef  15409  plyun0  15418  plyrecj  15445  dvply2  15449  reeff1o  15455  sin0pilem1  15463  sin0pilem2  15464  pilem3  15465  pigt2lt4  15466  pire  15468  sinhalfpilem  15473  pidiv2halves  15477  cosneghalfpi  15480  cospi  15482  efipi  15483  sin2pi  15485  cos2pi  15486  ef2pi  15487  cosq14gt0  15514  coseq00topi  15517  coseq0negpitopi  15518  sincos4thpi  15522  sincos6thpi  15524  sincos3rdpi  15525  pigt3  15526  cos02pilt1  15533  ioocosf1o  15536  dfrelog  15542  relogf1o  15543  relogcl  15544  relogiso  15555  rpcxpsqrt  15604  rpabscxpbnd  15622  2logb9irr  15653  2logb9irrALT  15656  sqrt2cxp2logb9e3  15657  2irrexpq  15658  2logb9irrap  15659  2irrexpqap  15660  mpodvdsmulf1o  15672  fsumdvdsmul  15673  perfectlem2  15682  lgsdir2lem1  15715  lgsdir2lem2  15716  lgsdir2lem4  15718  lgsdir2lem5  15719  lgsdi  15724  gausslemma2dlem0i  15744  gausslemma2dlem4  15751  lgseisenlem4  15760  lgsquadlem1  15764  lgsquad2lem2  15769  lgsquad2  15770  m1lgs  15772  2lgs2  15789  2lgslem4  15790  2lgsoddprmlem2  15793  2lgsoddprmlem3c  15796  2lgsoddprmlem3d  15797  2sqlem9  15811  2sqlem10  15812  1vgrex  15829  vtxval0  15862  iedgval0  15863  uhgr0  15893  upgrfi  15910  umgrislfupgrdom  15937  ausgrusgrben  15974  uspgredgiedg  15984  uspgriedgedg  15985  usgrislfuspgrdom  15996  uspgredg2vlem  16026  uspgredg2v  16027  0wlk0  16092  ex-fl  16113  ex-ceil  16114  ex-exp  16115  ex-fac  16116  ex-gcd  16119  bj-stfal  16130  bj-stst  16133  bj-dcfal  16143  bj-dcdc  16147  bj-stdc  16148  bj-dcst  16149  bj-el2oss1o  16162  elabf2  16170  bd0  16211  bdeli  16233  bdcriota  16270  bdbm1.3ii  16278  bdinex1  16286  bdssexi  16290  bj-inex  16294  bj-snex  16300  bj-sucex  16310  bj-d0clsepcl  16312  bj-omind  16321  bj-om  16324  bj-2inf  16325  bj-peano2  16326  bdpeano5  16330  bj-omssonALT  16350  bj-inf2vnlem1  16357  bj-omex2  16364  bj-nn0sucALT  16365  3dom  16381  012of  16386  2o01f  16387  subctctexmid  16395  pw1dceq  16399  nninfall  16405  nninfsellemqall  16411  nninfsellemeqinf  16412  nninfomnilem  16414  nninfomni  16415  exmidsbthrlem  16420  sbthom  16424  isomninnlem  16428  isomninn  16429  cvgcmp2nlemabs  16430  iooreen  16433  trilpolemisumle  16436  trilpolemeq1  16438  trilpo  16441  trirec0  16442  apdifflemr  16445  iswomninnlem  16447  iswomninn  16448  ismkvnnlem  16450  ismkvnn  16451  redcwlpo  16453  dcapnconst  16459  nconstwlpolem0  16461  nconstwlpo  16464  neapmkv  16466  neap0mkv  16467  taupi  16471