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

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 used 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  430  pm2.65i  648  notnoti  654  pm2.21i  655  pm2.24ii  656  notbii  678  nbn  711  ori  735  orci  743  olci  744  biorfi  758  imorri  761  dcbii  852  simp1i  1037  simp2i  1038  simp3i  1039  3mix1i  1200  3mix2i  1201  3mix3i  1202  3jaoi  1344  mptru  1411  dfnot  1420  mptnan  1472  mtpor  1474  mtpxor  1475  dcfromnotnotr  1497  dcfromcon  1498  dcfrompeirce  1499  mpg  1504  19.23h  1551  hbequid  1566  axi12  1567  nfri  1572  spi  1589  19.21  1636  eximii  1655  19.35i  1678  nfn  1710  19.37aiv  1727  19.23  1730  exan  1745  equid  1753  hbae  1770  equvini  1811  equveli  1812  sbid  1827  sbieh  1843  exdistrfor  1853  dveeq2or  1869  ax11v  1880  ax11ev  1881  equs5or  1883  sb4or  1886  sb4bor  1888  nfsb2or  1890  sbequilem  1891  sbequi  1892  speiv  1915  nfsbxy  2002  nfsbxyt  2003  sbco  2028  sbcocom  2030  sbcomxyyz  2032  sbal1yz  2061  dvelimALT  2070  dvelimfv  2071  dvelimor  2078  eumoi  2119  moani  2157  elsb1  2216  elsb2  2217  eqeq1i  2246  eqeq2i  2249  eleq1i  2304  eleq2i  2305  nfcrii  2385  neeq1i  2435  neeq2i  2436  necon3i  2468  rspec  2602  rgen2a  2604  mprg  2607  r19.21  2626  r19.23  2659  raleqi  2753  rexeqi  2754  rabeqif  2812  elv  2825  elexi  2834  ceqsal  2851  vtocl3  2879  vtoclef  2898  vtocle  2899  spcv  2919  spcev  2920  clel3  2961  elabf  2969  elab2  2974  elab3  2978  euxfrdc  3012  reueq  3025  rmoimi2  3029  sbsbc  3055  sbc8g  3059  sbc6  3077  sbcie  3086  sbcrex  3131  csbvarg  3175  csbief  3192  csbie2  3197  sbnfc2  3208  sseli  3244  sselii  3245  sseq1i  3274  sseq2i  3275  difeq1i  3343  difeq2i  3344  uneq1i  3379  uneq2i  3380  ineq1i  3428  ineq2i  3429  ssinss1  3460  difdif2ss  3488  n0ii  3530  ne0ii  3531  vn0  3532  vn0m  3533  abf  3570  disj2  3580  difid  3594  0dif  3597  disjdif  3599  difin0  3601  undif1ss  3602  difdifdirss  3612  iftruei  3646  iffalsei  3649  ifbieq2i  3664  ifbieq12i  3666  pweqi  3692  sspwi  3703  pwid  3707  sneqi  3721  elsn  3725  elpr  3730  elsn2  3743  ralsn  3752  rexsn  3753  eltp  3757  rabrsndc  3779  preq1i  3791  preq2i  3792  prid1  3817  snnz  3832  snm  3833  prnz  3836  prm  3837  tpnz  3839  snss  3850  snsssn  3886  opeq1i  3907  opeq2i  3908  unieqi  3945  unissi  3958  inteqi  3974  intmin2  3996  intab  3999  intsn  4005  iinconstm  4021  iuniin  4022  iinss1  4024  iunxdif2  4061  ssiinf  4062  iinss  4064  iinss2  4065  iinab  4074  iundif2ss  4078  iindif2m  4080  iinin2m  4081  iunxsn  4089  iunxprg  4093  iinpw  4103  invdisjrab  4124  sndisj  4126  disjxsn  4128  breqi  4136  breq1i  4137  breq2i  4138  brab1  4178  opabbii  4198  truni  4243  sepgi  4252  bm1.3ii  4254  a9evsep  4255  ax9vsep  4256  zfnuleu  4257  axnul  4258  ssexi  4271  difexi  4276  rabex  4280  rabex2  4282  elpw2  4293  pwnss  4296  iin0r  4306  intv  4307  pwex  4320  snex  4322  notnotsnex  4324  ord3ex  4327  dtruarb  4328  undifexmid  4330  intid  4364  opnzi  4375  copsexg  4384  opwo0id  4389  opelopabf  4417  epelc  4436  elon  4519  inton  4538  onn0  4545  onm  4546  elsuc  4551  elsuc2  4552  sucid  4562  iunsuc  4565  onordi  4571  ontrci  4572  onelssi  4574  eusvnf  4599  ssonunii  4636  sucex  4646  onssi  4662  onsuci  4663  ordtriexmidlem  4666  ordtriexmidlem2  4667  ordtriexmid  4668  ontriexmidim  4669  ordtri2orexmid  4670  2ordpr  4671  ontr2exmid  4672  onsucsssucexmid  4674  onsucelsucexmid  4677  regexmidlemm  4679  reg2exmid  4683  onirri  4690  ruALT  4698  onprc  4699  sucon  4700  dtru  4707  0elsucexmid  4712  ordpwsucexmid  4717  ordtri2or2exmid  4718  ontri2orexmidim  4719  dcextest  4728  omex  4740  find  4746  omelon  4756  nnoni  4758  limom  4761  nnregexmid  4768  omsinds  4769  xpeq1i  4794  xpeq2i  4795  0nelxp  4802  opthprc  4826  mosubop  4841  releqi  4858  relssi  4866  relin1  4895  relin2  4896  reldif  4897  inopab  4912  difopab  4913  xpiindim  4917  opabbi2dv  4929  ideq  4932  coeq1i  4939  coeq2i  4940  cnveqi  4955  eldm  4978  eldm2  4979  dmeqi  4982  dmv  4997  rneqi  5010  elrnmpti  5035  dmex  5049  rnex  5050  reseq1i  5059  reseq2i  5060  residm  5095  resex  5104  resmpt3  5112  imaeq1i  5123  imaeq2i  5124  elima  5131  imaex  5141  elimasn  5154  args  5156  epini  5158  dfse2  5160  eliniseg2  5167  relbrcnv  5168  cotr  5169  issref  5170  cnvsym  5171  asymref  5173  intirr  5174  codir  5176  qfto  5177  ssrnres  5230  cnveq0  5244  cnvsn0  5256  dmsnop  5261  rnsnop  5268  resdm2  5278  dfco2a  5288  cocnvcnv1  5298  coi2  5304  coires1  5305  cnvssrndm  5309  cossxp  5310  cocnvres  5312  relrelss  5314  relcoi2  5318  unidmrn  5320  dfdm2  5322  unixpm  5323  cnvexg  5325  cnvex  5326  cnviinm  5329  iotaval  5349  funeqi  5398  funi  5409  funres  5418  funcnvsn  5426  funcnvcnv  5440  funin  5452  funcnvres  5454  isarep2  5468  fneq1i  5475  fneq2i  5476  fndmi  5481  fnresdisj  5493  fnresi  5501  mpt0  5511  dmmpti  5513  feq1i  5526  feq2i  5527  fdmi  5541  fun2  5562  fssres  5565  resasplitss  5569  fintm  5577  fconst6  5592  f1ores  5654  foimacnv  5657  resdif  5661  funcocnv2  5664  f10d  5675  f1ovi  5680  fveq1i  5696  fveq2i  5698  0fv  5734  fvun1  5769  fvopab3ig  5779  fvmptss2  5780  mptrcl  5788  elfvmptrab1  5801  fndmdif  5814  fneqeql2  5818  f1oresrab  5873  fmptco  5874  funopsn  5891  fnressn  5901  fressnfv  5902  fmptap  5905  fvsnun1  5912  fvsnun2  5913  fsnunfv  5916  fconst2  5932  mptex  5943  fnfvimad  5954  rinvf1o  6035  riotabiia  6057  acexmidlema  6076  acexmidlemb  6077  acexmidlemcase  6080  acexmidlem2  6082  acexmidlemv  6083  oveq1i  6095  oveq2i  6096  oveqi  6098  oprabidlem  6116  0neqopab  6133  oprabbii  6143  oprabss  6174  mpompt  6180  funoprab  6188  fnoprab  6191  ovigg  6209  elmpocl  6284  relmptopab  6291  resfunexgALT  6337  cofunexg  6338  mptexw  6342  opabex3d  6350  opabex3  6351  1st0  6378  2nd0  6379  op1st  6380  op2nd  6381  f1stres  6393  f2ndres  6394  fo1stresm  6395  fo2ndresm  6396  1stcof  6397  2ndcof  6398  1stexg  6401  2ndexg  6402  releldm2  6419  reldm  6420  dfoprab3  6425  mpomptsx  6433  mpompts  6434  fnmpoi  6439  dmmpo  6440  mpoexxg  6446  mpoexw  6449  1stconst  6457  2ndconst  6458  dfmpo  6459  algrflem  6465  algrflemg  6466  cnvoprab  6470  f1od2  6471  elmpom  6474  mpoxopn0yelv  6510  mpoxopoveq  6511  tposssxp  6520  brtpos2  6522  reldmtpos  6524  dftpos2  6532  dftpos4  6534  tpostpos  6535  tpostpos2  6536  tposfo  6542  tposf  6543  tposeqi  6548  tposex  6549  tposoprab  6551  issmo  6559  smores  6563  smores2  6565  iordsmo  6568  smo0  6569  tfrlem8  6589  tfrexlem  6605  tfr1onlem3  6609  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlemres  6620  tfri1dALT  6622  tfri2  6637  rdgisuc1  6655  rdg0  6658  frecfun  6666  frec0g  6668  freccllem  6673  frecfcllem  6675  frecsuclem  6677  frecrdg  6679  2on0  6697  xp01disj  6706  2oconcl  6712  fnoa  6720  oaexg  6721  fnom  6723  omexg  6724  fnoei  6725  oeiexg  6726  oei0  6732  oacl  6733  oasuc  6737  o1p1e2  6741  omsuc  6745  nna0r  6751  nnm0r  6752  1onn  6793  2onn  6794  3onn  6795  4onn  6796  2ssom  6797  eqerlem  6838  eceq2i  6845  elqs  6860  qsex  6866  ecqs  6871  iinerm  6881  th3qlem1  6911  th3q  6914  mapsn  6972  mapsnf1o3  6979  ixpiinm  7006  ixpssmap  7014  brdom  7034  f1dom  7046  enref  7051  dom2  7061  idssen  7063  ssdomg  7065  ensymi  7069  ensn1  7083  fiprc  7104  1domsn  7115  dom1o  7116  xpcomf1o  7123  xpcomco  7124  dom0  7138  0dom  7139  xpmapenlem  7149  phplem2  7154  php5  7159  snnen2og  7160  1nen2  7162  php5dom  7164  ssfilem  7177  ssfiexmid  7178  ssfilemd  7179  ssfiexmidt  7180  domfiexmid  7182  0fi  7188  diffitest  7191  findcard  7192  findcard2  7193  findcard2s  7194  isinfinf  7201  ac6sfi  7202  inffiexmid  7213  pw1fin  7217  unfiexmid  7225  xpfi  7239  fisseneq  7242  ssfirab  7244  residfi  7254  mapfi  7261  en1eqsn  7265  snexxph  7267  sbthlem2  7275  sbthlemi3  7276  sbthlemi6  7279  sbthlem7  7280  fi0  7309  fipwfi  7321  supeq1i  7328  infeq1i  7353  djuexb  7384  djuf1olemr  7394  inresflem  7400  djuinr  7403  updjudhcoinlf  7420  updjudhcoinrg  7421  casefun  7425  caserel  7427  caseinj  7429  caseinl  7431  caseinr  7432  omp1eomlem  7434  endjusym  7436  difinfsn  7440  difinfinf  7441  djuinj  7446  0ct  7447  ctmlemr  7448  ctssdclemn0  7450  ctssdccl  7451  omct  7457  ctfoex  7458  finomni  7480  exmidomni  7482  fodjuomni  7489  ctssexmid  7490  fodjumkv  7500  nninfwlporlem  7513  nninfwlpoimlemg  7515  nninfwlpoim  7519  nninfinfwlpo  7520  card0  7533  ficardon  7534  exmidonfinlem  7545  dju1p1e2  7549  exmidfodomrlemim  7553  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  iftrueb01  7582  3nelsucpw1  7593  sucpw1nss3  7594  3nsssucpw1  7595  fmelpw1o  7606  2onetap  7621  exmidmotap  7627  0npi  7680  dmaddpi  7692  dmmulpi  7693  1lt2pi  7707  0nnq  7731  1nq  7733  dmaddpq  7746  dmmulpq  7747  rec1nq  7762  1lt2nq  7773  halfnqq  7777  prarloclemarch2  7786  enq0enq  7798  nqnq0pi  7805  nnnq0lem1  7813  addnnnq0  7816  mulnnnq0  7817  nq0m0r  7823  addpinq1  7831  prarloclem5  7867  prarloclemcalc  7869  1pr  7921  1idprl  7957  1idpru  7958  ltexprlemm  7967  recexprlem1ssl  8000  recexprlem1ssu  8001  suplocexprlemell  8080  suplocexprlem2b  8081  suplocexprlemmu  8085  suplocexprlemdisj  8087  suplocexprlemloc  8088  suplocexprlemub  8090  suplocexprlemlub  8091  prsrlem1  8109  addsrpr  8112  mulsrpr  8113  gt0srpr  8115  0nsr  8116  0r  8117  1sr  8118  m1r  8119  m1m1sr  8128  caucvgsr  8169  suplocsrlempr  8174  addresr  8204  mulresr  8205  pitonnlem1  8212  peano1nnnn  8219  axi2m1  8242  axcnre  8248  peano5nnnn  8259  axcaucvg  8267  mpomulf  8316  mulridi  8328  mullidi  8329  pnfnre  8367  mnfnre  8368  pnfnemnf  8380  mnfxr  8382  rexri  8383  ltnri  8418  ltleii  8428  00id  8467  addridi  8468  addlidi  8469  0cnALT  8516  negeqi  8520  negicn  8527  neg0  8572  renegcli  8588  negcli  8594  negidi  8595  negnegi  8596  subidi  8597  subid1i  8598  negne0bi  8599  negrebi  8600  mul02i  8717  mul01i  8718  mulm1i  8730  leidi  8813  gt0ne0ii  8815  inelr  8912  msqge0i  8945  gt0ap0ii  8956  1div1e1  9034  div1i  9070  eqnegi  9071  recclapi  9072  recidapi  9073  divmulapi  9096  rerecclapi  9107  redivclapi  9109  rerecapb  9173  recgt0  9180  ltp1i  9235  divgt0ii  9249  ltmul1ii  9258  ltdiv1ii  9259  sup3exmid  9287  indconst0  9302  indconst1  9303  peano5nni  9307  nnrei  9313  1nn  9315  nngt0i  9334  neg1ap0  9413  2timesi  9434  times2i  9435  2nn  9466  3nn  9467  4nn  9468  5nn  9469  6nn  9470  7nn  9471  8nn  9472  9nn  9473  2muline0  9530  rehalfcli  9554  nn0ssre  9567  nnnn0i  9571  dfn2  9576  0nn0  9578  nn0ge0i  9590  zrei  9650  neg1z  9676  nn0negzi  9679  dfz2  9717  nneoi  9750  peano5uzi  9755  dfuzi  9756  nn0ind-raph  9763  deceq1i  9783  deceq2i  9784  10nn  9792  numltc  9802  eluzel2  9926  eluz1i  9929  nn0uz  9957  nnuz  9958  uzuzle35  9965  infrenegsupex  9994  lbzbi  10016  divfnzn  10021  qdivcl  10043  irrmul  10047  irrmulap  10048  cnref1o  10051  0ltpnf  10184  mnflt0  10186  0lepnf  10192  xrltnsym  10195  xrlttri3  10199  nltpnft  10216  ngtmnft  10219  xrrebnd  10221  xnegmnf  10231  xneg0  10233  xltnegi  10237  xaddmnf1  10250  xaddmnf2  10251  mnfaddpnf  10253  xaddid1  10264  xnn0lenn0nn0  10267  xnn0xadd0  10269  xposdif  10284  ixxex  10301  iooval2  10317  unirnioo  10375  ioorebasg  10377  elrege0  10378  fzval2  10414  fzen  10447  fzprval  10489  fztpval  10490  uzdisj  10500  ige2m1fz  10517  fz01or  10518  fz1ssfz0  10524  fz0sn  10528  fz0tp  10529  fz0to3un2pr  10530  fz0to4untppr  10531  nn0disj  10545  1fv  10546  4fvwrd4  10547  fzo0ss1  10583  fzo01  10634  fzo12sn  10635  fzo0to2pr  10636  fzo0to3tp  10637  fzo0to42pr  10638  zsupssdc  10673  qbtwnxr  10692  flval  10707  fldiv4lem1div2  10742  modqfrac  10774  modqmulnn  10779  q2txmodxeq0  10821  frecuzrdgdom  10855  frecuzrdgfun  10857  frecuzrdgsuct  10861  frechashgf1o  10865  nnct  10872  xnn0nnen  10874  fxnn0nninf  10876  0tonninf  10877  1tonninf  10878  iseqvalcbv  10896  ser0f  10971  0exp0e1  10981  qexpcl  10992  qexpclz  10997  m1expcl2  10998  1exp  11005  sqvali  11056  sqcli  11057  sqeq0i  11058  resqcli  11061  sq1  11070  neg1sqe1  11071  iexpcyc  11081  qsqeqor  11087  facnn  11165  fac0  11166  fac1  11167  fac2  11169  fac3  11170  fac4  11171  bcval  11187  bcm1k  11198  bcpasc  11204  bccl  11205  4bc3eq4  11212  4bc2eq6  11213  hashinfom  11217  hashennn  11219  hashfz1  11222  fihasheq0  11232  hash0  11235  hashsng  11237  fihashen1  11238  en1hash  11239  omgadd  11242  hashp1i  11251  hashxp  11267  hashpwfi  11269  fimaxq  11270  ssenneg  11280  hashfibc  11283  hashf1lem1  11285  hashf1  11287  zfz1iso  11293  hash2en  11295  wrdexi  11317  wrdv  11320  wrdeqi  11327  wrd0  11329  lsw0  11352  ccatclab  11362  ccatidid  11378  s1prc  11391  ccat1st1st  11409  swrds1  11440  fnpfx  11449  swrdccatin2  11501  pfxccatin12lem2  11503  cats1fvn  11536  shftidt2  11597  cjexp  11658  re0  11661  im0  11662  re1  11663  im1  11664  cj0  11667  cji  11668  recli  11677  imcli  11678  cjcli  11679  replimi  11680  cjcji  11681  reim0bi  11682  rerebi  11683  cjrebi  11684  recji  11685  imcji  11686  cjmulrcli  11687  cjmulvali  11688  cjmulge0i  11689  renegi  11690  imnegi  11691  cjnegi  11692  addcji  11693  uzin2  11753  rexanuz  11754  rexfiuz  11755  sqrtrval  11766  sqrt0  11770  resqrexlemcalc3  11782  resqrexlemcvg  11785  resqrex  11792  abs0  11824  absi  11825  qabsor  11841  absimle  11850  recan  11875  caubnd2  11883  leabsi  11894  absrei  11895  sqrtpclii  11896  sqrtgt0ii  11897  absvalsqi  11906  absvalsq2i  11907  abscli  11908  absge0i  11909  absval2i  11910  abs00i  11911  absgt0api  11912  absnegi  11913  abscji  11914  releabsi  11915  infxrnegsupex  12029  xrbdtri  12042  cbvsum  12126  sumeq1i  12129  sum0  12155  isumz  12156  fisumss  12159  fsumsersdc  12162  fsumadd  12173  isumclim  12188  isumclim3  12190  fsumcnv  12204  modfsummodlem1  12223  fsumrelem  12238  binomlem  12250  binom  12251  arisum2  12266  expcnv  12271  0.999...  12288  prodf1f  12310  cbvprod  12325  prodeq1i  12328  zproddc  12346  zprodap0  12348  prod0  12352  fprodssdc  12357  prodsnf  12359  fprodcnv  12392  fprodge0  12404  fprodge1  12406  ef0lem  12427  esum  12429  ere  12437  ege2le3  12438  ef0  12439  eff2  12447  efsep  12458  reeff1  12467  sin0  12496  cos0  12497  ef01bndlem  12523  cos2bnd  12527  sincos1sgn  12532  sincos2sgn  12533  sin4lt0  12534  eirr  12546  0dvds  12578  dvds1  12620  z0even  12678  n2dvdsm1  12680  z2even  12681  n2dvds3  12682  ndvdssub  12697  ndvdsi  12700  flodddiv4  12703  bits0  12715  bitsfzo  12722  0bits  12726  m1bits  12727  bitsinv1lem  12728  bitsinv1  12729  gcddvds  12740  gcd1  12764  6gcd4e2  12772  bezoutlembi  12782  dfgcd3  12787  dfgcd2  12791  nninfctlemfo  12817  nninfct  12818  3lcm2e6woprm  12864  qredeu  12875  isprm2lem  12894  isprm3  12896  prm2orodd  12904  isprm5lem  12919  sqrt2irr0  12942  pw2dvds  12944  phicl2  12992  phi1  12997  dfphi2  12998  phiprmpw  13000  eulerthlemrprm  13007  eulerthlemh  13009  odzval  13020  oddprm  13038  pczpre  13076  pcdiv  13081  pc0  13083  pcqdiv  13086  pcrec  13087  pcexp  13088  pcxcl  13090  pcxqcl  13091  pcdvdstr  13106  pc2dvds  13109  dvdsprmpweqnn  13115  pcmpt  13122  qexpz  13131  pockthi  13137  1arith2  13147  4sqlemffi  13175  4sqlem11  13180  4sqlem13m  13182  4sqlem19  13188  dec2dvds  13190  dec5nprm  13193  modxai  13195  modxp1i  13197  numexp0  13201  numexp1  13202  ballotfilem1  13220  ballotfilemonn  13221  ballotfilem2  13228  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilem4  13241  ballotfilemi  13243  ballotfilem7  13279  ballotfilem8  13280  ballotfilemth  13281  ennnfonelemp1  13297  ennnfonelem1  13298  ennnfonelemkh  13303  ennnfonelemex  13305  ennnfonelemnn0  13313  ennnfonelemr  13314  exmidunben  13317  ctinfomlemom  13318  ctinfom  13319  ctinf  13321  qnnen  13322  omctfn  13334  omiunct  13335  ssnnctlemct  13337  nninfdc  13344  structcnvcnv  13368  structfun  13370  structfn  13371  ndxarg  13375  ndxid  13376  setsresg  13390  setsslnid  13404  basmex  13412  basmexd  13413  slotm  13415  strleun  13458  strle1g  13460  prdsvallem  13621  imasaddfnlemg  13635  quslem  13645  xpsfrnel  13665  xpsff1o  13670  ismgmn0  13678  fn0g  13695  0g0  13696  fngzsum  13708  idghm  14062  gsumsncmn  14156  gsumclfi  14159  gsummptfidmadd  14161  gsumsubmclfi  14163  gsumconstcmn  14166  prdsex  14172  prdsval  14173  prdsbaslemss  14174  mgpplusg  14222  mgpbas  14225  ringidval  14265  rhmfn  14479  rmodislmodlem  14687  rmodislmod  14688  lidlmex  14812  mopnset  14889  cntopex  14891  cnfldex  14896  cnfldbas  14897  mpocnfldadd  14898  mpocnfldmul  14900  cnfldcj  14902  cnfldtset  14903  cnfldle  14904  cnfldds  14905  cnring  14907  cnfld0  14908  cnfld1  14909  cnfldneg  14910  cnfldplusf  14911  cnfldsub  14912  cnfldmulg  14913  cnfldexp  14914  cnsubglem  14916  cnsubrglem  14917  gzsubrg  14919  gsumfsum  14923  cnfldui  14924  zringring  14928  zringabl  14929  zringgrp  14930  zring1  14936  zringsubgval  14940  expghmap  14942  znval  14971  znle  14972  znbaslemnn  14974  znbas  14979  znzrh2  14981  znzrhval  14982  znzrhfo  14983  znleval  14988  znidom  14992  znidomb  14993  fnpsr  15051  psrelbas  15066  psradd  15070  psraddcl  15071  psr1clfi  15079  mplrcl  15085  mplbasss  15087  mpladd  15095  istopon  15114  topontopi  15117  toponunii  15118  toponrestid  15122  istps  15133  topontopn  15138  eltpsi  15142  eltg4i  15156  eltg3  15158  tg1  15160  tg2  15161  tgclb  15166  topnex  15187  sn0topon  15189  distps  15192  cldrcl  15203  sn0cld  15238  restco  15275  lmrcl  15293  ssidcn  15311  cnconst2  15334  cnptopresti  15339  cnptoprest  15340  txuni2  15357  txbas  15359  eltx  15360  txcnp  15372  upxp  15373  txcnmpt  15374  uptx  15375  txcn  15376  txrest  15377  txlm  15380  cnmptid  15382  cnmpt1st  15389  cnmpt2nd  15390  hmeofn  15403  psmetge0  15432  ismeti  15447  xmetunirn  15459  xmetge0  15466  unirnblps  15523  unirnbl  15524  mopnex  15606  qtopbasss  15622  retop  15625  uniretop  15626  iooretopg  15629  cnxmet  15632  cntoptopon  15633  cnbl0  15635  cnfldxms  15638  cnfldtps  15639  rexmet  15650  blssioo  15654  tgioo  15655  tgqioo  15656  cnopnap  15712  hovercncf  15747  limcresi  15767  dvfvalap  15782  dvidlemap  15792  dvidrelem  15793  dvidsslem  15794  dvcnp2cntop  15800  dvcoapbr  15808  dvexp2  15813  dvrecap  15814  dveflem  15827  dvef  15828  plyun0  15837  plyrecj  15864  dvply2  15868  reeff1o  15874  sin0pilem1  15882  sin0pilem2  15883  pilem3  15884  pigt2lt4  15885  pire  15887  sinhalfpilem  15892  pidiv2halves  15896  cosneghalfpi  15899  cospi  15901  efipi  15902  sin2pi  15904  cos2pi  15905  ef2pi  15906  cosq14gt0  15933  coseq00topi  15936  coseq0negpitopi  15937  sincos4thpi  15941  sincos6thpi  15943  sincos3rdpi  15944  pigt3  15945  cos02pilt1  15952  ioocosf1o  15955  dfrelog  15961  relogf1o  15962  relogcl  15963  relogiso  15974  logfac  15995  rpcxpsqrt  16024  rpabscxpbnd  16042  2logb9irr  16073  2logb9irrALT  16076  sqrt2cxp2logb9e3  16077  2irrexpq  16078  2logb9irrap  16079  2irrexpqap  16080  log2tlbndlog2  16082  log2ublem2  16084  log2ublem3  16085  log2ublog2  16086  birthdaylog2  16090  mpodvdsmulf1o  16104  fsumdvdsmul  16105  perfectlem2  16114  lgsdir2lem1  16147  lgsdir2lem2  16148  lgsdir2lem4  16150  lgsdir2lem5  16151  lgsdi  16156  gausslemma2dlem0i  16176  gausslemma2dlem4  16183  lgseisenlem4  16192  lgsquadlem1  16196  lgsquad2lem2  16201  lgsquad2  16202  m1lgs  16204  2lgs2  16221  2lgslem4  16222  2lgsoddprmlem2  16225  2lgsoddprmlem3c  16228  2lgsoddprmlem3d  16229  2sqlem9  16243  2sqlem10  16244  1vgrex  16261  vtxval0  16294  iedgval0  16295  uhgr0  16326  upgrfi  16343  umgrislfupgrdom  16372  ausgrusgrben  16409  uspgredgiedg  16419  uspgriedgedg  16420  usgrislfuspgrdom  16431  uspgredg2vlem  16461  uspgredg2v  16462  usgr0  16480  griedg0prc  16491  subupgr  16514  vdegp1cid  16557  0wlk0  16612  clwwlkn1  16659  clwwlkn2  16662  eupth2lem1  16699  eulerpathum  16722  konigsbergiedgwen  16725  konigsberglem1  16729  konigsberglem3  16731  konigsberglem4  16732  konigsberglem5  16733  konigsberg  16734  ex-fl  16739  ex-ceil  16740  ex-exp  16741  ex-fac  16742  ex-gcd  16745  bj-stfal  16770  bj-stst  16773  bj-dcfal  16783  bj-dcdc  16787  bj-stdc  16788  bj-dcst  16789  bj-el2oss1o  16802  elabf2  16810  bd0  16850  bdeli  16872  bdcriota  16909  bdbm1.3ii  16917  bdinex1  16925  bdssexi  16929  bj-inex  16933  bj-snex  16939  bj-sucex  16949  bj-d0clsepcl  16951  bj-omind  16960  bj-om  16963  bj-2inf  16964  bj-peano2  16965  bdpeano5  16969  bj-omssonALT  16989  bj-inf2vnlem1  16996  bj-omex2  17003  bj-nn0sucALT  17004  3dom  17018  012of  17023  2o01f  17024  subctctexmid  17030  pw1dceq  17035  exmidpeirce  17038  wexmiddc  17042  wexmiddiffilem  17043  wexmiddifxylem  17045  wexmiddifxy  17046  nninfall  17052  nninfsellemqall  17058  nninfsellemeqinf  17059  nninfomnilem  17061  nninfomni  17062  exmidsbthrlem  17067  sbthom  17071  isomninnlem  17079  isomninn  17080  cvgcmp2nlemabs  17081  iooreen  17084  trilpolemisumle  17087  trilpolemeq1  17089  trilpo  17092  trirec0  17093  apdifflemr  17096  qdiff  17098  iswomninnlem  17099  iswomninn  17100  ismkvnnlem  17102  ismkvnn  17103  redcwlpo  17105  dcapnconst  17111  nconstwlpolem0  17113  nconstwlpo  17116  neapmkv  17118  neap0mkv  17119  taupi  17123