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

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  639  notnoti  645  pm2.21i  646  pm2.24ii  647  notbii  668  nbn  699  ori  723  orci  731  olci  732  biorfi  746  imorri  749  dcbii  840  simp1i  1006  simp2i  1007  simp3i  1008  3mix1i  1169  3mix2i  1170  3mix3i  1171  3jaoi  1303  mptru  1362  dfnot  1371  mptnan  1423  mtpor  1425  mtpxor  1426  mpg  1451  19.23h  1498  hbequid  1513  axi12  1514  nfri  1519  spi  1536  19.21  1583  eximii  1602  19.35i  1625  nfn  1658  19.37aiv  1675  19.23  1678  exan  1693  equid  1701  hbae  1718  equvini  1758  equveli  1759  sbid  1774  sbieh  1790  exdistrfor  1800  dveeq2or  1816  ax11v  1827  ax11ev  1828  equs5or  1830  sb4or  1833  sb4bor  1835  nfsb2or  1837  sbequilem  1838  sbequi  1839  speiv  1862  nfsbxy  1942  nfsbxyt  1943  sbco  1968  sbcocom  1970  sbcomxyyz  1972  sbal1yz  2001  dvelimALT  2010  dvelimfv  2011  dvelimor  2018  eumoi  2059  moani  2096  elsb1  2155  elsb2  2156  eqeq1i  2185  eqeq2i  2188  eleq1i  2243  eleq2i  2244  nfcrii  2312  neeq1i  2362  neeq2i  2363  necon3i  2395  rspec  2529  rgen2a  2531  mprg  2534  r19.21  2553  r19.23  2585  raleqi  2677  rexeqi  2678  rabeqif  2730  elv  2743  elexi  2751  ceqsal  2768  vtocl3  2795  vtoclef  2812  vtocle  2813  spcv  2833  spcev  2834  clel3  2874  elabf  2882  elab2  2887  elab3  2891  euxfrdc  2925  reueq  2938  rmoimi2  2942  sbsbc  2968  sbc8g  2972  sbc6  2990  sbcie  2999  sbcrex  3044  csbvarg  3087  csbief  3103  csbie2  3108  sbnfc2  3119  sseli  3153  sselii  3154  sseq1i  3183  sseq2i  3184  difeq1i  3251  difeq2i  3252  uneq1i  3287  uneq2i  3288  ineq1i  3334  ineq2i  3335  ssinss1  3366  difdif2ss  3394  n0ii  3433  ne0ii  3434  vn0  3435  vn0m  3436  abf  3468  disj2  3480  difid  3493  0dif  3496  disjdif  3497  difin0  3498  undif1ss  3499  difdifdirss  3509  rgenm  3527  iftruei  3542  iffalsei  3545  ifbieq2i  3559  ifbieq12i  3561  pweqi  3581  pwid  3592  sneqi  3606  elsn  3610  elpr  3615  elsn2  3628  ralsn  3637  rexsn  3638  eltp  3642  rabrsndc  3662  preq1i  3674  preq2i  3675  prid1  3700  snnz  3713  snm  3714  prnz  3716  prm  3717  tpnz  3719  snss  3729  snsssn  3763  opeq1i  3783  opeq2i  3784  unieqi  3821  unissi  3834  inteqi  3850  intmin2  3872  intab  3875  intsn  3881  iinconstm  3897  iuniin  3898  iinss1  3900  iunxdif2  3937  ssiinf  3938  iinss  3940  iinss2  3941  iinab  3950  iundif2ss  3954  iindif2m  3956  iinin2m  3957  iunxsn  3965  iunxprg  3969  iinpw  3979  sndisj  4001  disjxsn  4003  breqi  4011  breq1i  4012  breq2i  4013  brab1  4052  opabbii  4072  truni  4117  bm1.3ii  4126  a9evsep  4127  ax9vsep  4128  zfnuleu  4129  axnul  4130  ssexi  4143  rabex  4149  elpw2  4159  pwnss  4161  iin0r  4171  intv  4172  pwex  4185  snex  4187  notnotsnex  4189  ord3ex  4192  dtruarb  4193  undifexmid  4195  intid  4226  opnzi  4237  copsexg  4246  opelopabf  4276  epelc  4293  elon  4376  inton  4395  onn0  4402  onm  4403  elsuc  4408  elsuc2  4409  sucid  4419  iunsuc  4422  onordi  4428  ontrci  4429  onelssi  4431  eusvnf  4455  ssonunii  4490  sucex  4500  onssi  4516  onsuci  4517  ordtriexmidlem  4520  ordtriexmidlem2  4521  ordtriexmid  4522  ontriexmidim  4523  ordtri2orexmid  4524  2ordpr  4525  ontr2exmid  4526  onsucsssucexmid  4528  onsucelsucexmid  4531  regexmidlemm  4533  reg2exmid  4537  onirri  4544  ruALT  4552  onprc  4553  sucon  4554  dtru  4561  0elsucexmid  4566  ordpwsucexmid  4571  ordtri2or2exmid  4572  ontri2orexmidim  4573  dcextest  4582  omex  4594  find  4600  omelon  4610  nnoni  4612  limom  4615  nnregexmid  4622  omsinds  4623  xpeq1i  4648  xpeq2i  4649  0nelxp  4656  opthprc  4679  mosubop  4694  releqi  4711  relssi  4719  relin1  4746  relin2  4747  reldif  4748  inopab  4761  difopab  4762  xpiindim  4766  opabbi2dv  4778  ideq  4781  coeq1i  4788  coeq2i  4789  cnveqi  4804  eldm  4826  eldm2  4827  dmeqi  4830  dmv  4845  rneqi  4857  elrnmpti  4882  dmex  4895  rnex  4896  reseq1i  4905  reseq2i  4906  residm  4941  resex  4950  resmpt3  4958  imaeq1i  4969  imaeq2i  4970  elima  4977  imaex  4985  elimasn  4997  args  4999  epini  5001  dfse2  5003  eliniseg2  5010  relbrcnv  5011  cotr  5012  issref  5013  cnvsym  5014  asymref  5016  intirr  5017  codir  5019  qfto  5020  ssrnres  5073  cnveq0  5087  cnvsn0  5099  dmsnop  5104  rnsnop  5111  resdm2  5121  dfco2a  5131  cocnvcnv1  5141  coi2  5147  coires1  5148  cnvssrndm  5152  cossxp  5153  cocnvres  5155  relrelss  5157  relcoi2  5161  unidmrn  5163  dfdm2  5165  unixpm  5166  cnvexg  5168  cnvex  5169  cnviinm  5172  iotaval  5191  funeqi  5239  funi  5250  funres  5259  funcnvsn  5263  funcnvcnv  5277  funin  5289  funcnvres  5291  isarep2  5305  fneq1i  5312  fneq2i  5313  fnresdisj  5328  fnresi  5335  mpt0  5345  dmmpti  5347  feq1i  5360  feq2i  5361  fdmi  5375  fun2  5391  fssres  5393  resasplitss  5397  fintm  5403  fconst6  5417  f1ores  5478  foimacnv  5481  resdif  5485  funcocnv2  5488  f1ovi  5502  fveq1i  5518  fveq2i  5520  0fv  5552  fvun1  5584  fvopab3ig  5592  fvmptss2  5593  mptrcl  5600  elfvmptrab1  5612  fndmdif  5623  fneqeql2  5627  f1oresrab  5683  fmptco  5684  fnressn  5704  fressnfv  5705  fmptap  5708  fvsnun1  5715  fvsnun2  5716  fsnunfv  5719  fconst2  5735  mptex  5744  riotabiia  5850  acexmidlema  5868  acexmidlemb  5869  acexmidlemcase  5872  acexmidlem2  5874  acexmidlemv  5875  oveq1i  5887  oveq2i  5888  oveqi  5890  oprabidlem  5908  0neqopab  5922  oprabbii  5932  oprabss  5963  mpompt  5969  funoprab  5977  fnoprab  5980  fovcl  5982  ovigg  5997  elmpocl  6071  resfunexgALT  6111  cofunexg  6112  mptexw  6116  opabex3d  6124  opabex3  6125  1st0  6147  2nd0  6148  op1st  6149  op2nd  6150  f1stres  6162  f2ndres  6163  fo1stresm  6164  fo2ndresm  6165  1stcof  6166  2ndcof  6167  1stexg  6170  2ndexg  6171  releldm2  6188  reldm  6189  dfoprab3  6194  mpomptsx  6200  mpompts  6201  fnmpoi  6207  dmmpo  6208  mpoexxg  6213  mpoexw  6216  1stconst  6224  2ndconst  6225  dfmpo  6226  algrflem  6232  algrflemg  6233  cnvoprab  6237  f1od2  6238  mpoxopn0yelv  6242  mpoxopoveq  6243  tposssxp  6252  brtpos2  6254  reldmtpos  6256  dftpos2  6264  dftpos4  6266  tpostpos  6267  tpostpos2  6268  tposfo  6274  tposf  6275  tposeqi  6280  tposex  6281  tposoprab  6283  issmo  6291  smores  6295  smores2  6297  iordsmo  6300  smo0  6301  tfrlem8  6321  tfrexlem  6337  tfr1onlem3  6341  tfr1onlemsucaccv  6344  tfr1onlembxssdm  6346  tfr1onlemres  6352  tfri1dALT  6354  tfri2  6369  rdgisuc1  6387  rdg0  6390  frecfun  6398  frec0g  6400  freccllem  6405  frecfcllem  6407  frecsuclem  6409  frecrdg  6411  2on0  6429  xp01disj  6436  2oconcl  6442  fnoa  6450  oaexg  6451  fnom  6453  omexg  6454  fnoei  6455  oeiexg  6456  oei0  6462  oacl  6463  oasuc  6467  o1p1e2  6471  omsuc  6475  nna0r  6481  nnm0r  6482  1onn  6523  2onn  6524  3onn  6525  4onn  6526  2ssom  6527  eqerlem  6568  elqs  6588  qsex  6594  ecqs  6599  iinerm  6609  th3qlem1  6639  th3q  6642  mapsn  6692  mapsnf1o3  6699  ixpiinm  6726  ixpssmap  6734  brdom  6752  f1dom  6762  enref  6767  dom2  6777  idssen  6779  ssdomg  6780  ensymi  6784  ensn1  6798  fiprc  6817  1domsn  6821  xpcomf1o  6827  xpcomco  6828  dom0  6840  0dom  6841  xpmapenlem  6851  phplem2  6855  php5  6860  snnen2og  6861  1nen2  6863  php5dom  6865  ssfilem  6877  ssfiexmid  6878  domfiexmid  6880  0fin  6886  diffitest  6889  findcard  6890  findcard2  6891  findcard2s  6892  isinfinf  6899  ac6sfi  6900  inffiexmid  6908  pw1fin  6912  unfiexmid  6919  xpfi  6931  fisseneq  6933  ssfirab  6935  en1eqsn  6949  snexxph  6951  sbthlem2  6959  sbthlemi3  6960  sbthlemi6  6963  sbthlem7  6964  fi0  6976  supeq1i  6989  infeq1i  7014  djuexb  7045  djuf1olemr  7055  inresflem  7061  djuinr  7064  updjudhcoinlf  7081  updjudhcoinrg  7082  casefun  7086  caserel  7088  caseinj  7090  caseinl  7092  caseinr  7093  omp1eomlem  7095  endjusym  7097  difinfsn  7101  difinfinf  7102  djuinj  7107  0ct  7108  ctmlemr  7109  ctssdclemn0  7111  ctssdccl  7112  omct  7118  ctfoex  7119  finomni  7140  exmidomni  7142  fodjuomni  7149  ctssexmid  7150  fodjumkv  7160  nninfwlporlem  7173  nninfwlpoimlemg  7175  nninfwlpoim  7178  card0  7189  exmidonfinlem  7194  dju1p1e2  7198  exmidfodomrlemim  7202  exmidfodomrlemr  7203  exmidfodomrlemrALT  7204  3nelsucpw1  7235  sucpw1nss3  7236  3nsssucpw1  7237  2onetap  7256  exmidmotap  7262  0npi  7314  dmaddpi  7326  dmmulpi  7327  1lt2pi  7341  0nnq  7365  1nq  7367  dmaddpq  7380  dmmulpq  7381  rec1nq  7396  1lt2nq  7407  halfnqq  7411  prarloclemarch2  7420  enq0enq  7432  nqnq0pi  7439  nnnq0lem1  7447  addnnnq0  7450  mulnnnq0  7451  nq0m0r  7457  addpinq1  7465  prarloclem5  7501  prarloclemcalc  7503  1pr  7555  1idprl  7591  1idpru  7592  ltexprlemm  7601  recexprlem1ssl  7634  recexprlem1ssu  7635  suplocexprlemell  7714  suplocexprlem2b  7715  suplocexprlemmu  7719  suplocexprlemdisj  7721  suplocexprlemloc  7722  suplocexprlemub  7724  suplocexprlemlub  7725  prsrlem1  7743  addsrpr  7746  mulsrpr  7747  gt0srpr  7749  0nsr  7750  0r  7751  1sr  7752  m1r  7753  m1m1sr  7762  caucvgsr  7803  suplocsrlempr  7808  addresr  7838  mulresr  7839  pitonnlem1  7846  peano1nnnn  7853  axi2m1  7876  axcnre  7882  peano5nnnn  7893  axcaucvg  7901  mulid1i  7961  mullidi  7962  pnfnre  8001  mnfnre  8002  pnfnemnf  8014  mnfxr  8016  rexri  8017  ltnri  8052  ltleii  8062  00id  8100  addid1i  8101  addid2i  8102  0cnALT  8149  negeqi  8153  negicn  8160  neg0  8205  renegcli  8221  negcli  8227  negidi  8228  negnegi  8229  subidi  8230  subid1i  8231  negne0bi  8232  negrebi  8233  mul02i  8349  mul01i  8350  mulm1i  8362  leidi  8444  gt0ne0ii  8446  inelr  8543  msqge0i  8576  gt0ap0ii  8587  1div1e1  8663  div1i  8699  eqnegi  8700  recclapi  8701  recidapi  8702  divmulapi  8725  rerecclapi  8736  redivclapi  8738  rerecapb  8802  recgt0  8809  ltp1i  8864  divgt0ii  8878  ltmul1ii  8887  ltdiv1ii  8888  sup3exmid  8916  peano5nni  8924  nnrei  8930  1nn  8932  nngt0i  8951  neg1ap0  9030  2timesi  9051  times2i  9052  2nn  9082  3nn  9083  4nn  9084  5nn  9085  6nn  9086  7nn  9087  8nn  9088  9nn  9089  2muline0  9146  rehalfcli  9169  nn0ssre  9182  nnnn0i  9186  dfn2  9191  0nn0  9193  nn0ge0i  9205  zrei  9261  neg1z  9287  nn0negzi  9290  dfz2  9327  nneoi  9359  peano5uzi  9364  dfuzi  9365  nn0ind-raph  9372  deceq1i  9392  deceq2i  9393  10nn  9401  numltc  9411  eluzel2  9535  eluz1i  9537  nn0uz  9564  nnuz  9565  infrenegsupex  9596  lbzbi  9618  divfnzn  9623  qdivcl  9645  irrmul  9649  cnref1o  9652  0ltpnf  9784  mnflt0  9786  0lepnf  9792  xrltnsym  9795  xrlttri3  9799  nltpnft  9816  ngtmnft  9819  xrrebnd  9821  xnegmnf  9831  xneg0  9833  xltnegi  9837  xaddmnf1  9850  xaddmnf2  9851  mnfaddpnf  9853  xaddid1  9864  xnn0lenn0nn0  9867  xnn0xadd0  9869  xposdif  9884  ixxex  9901  iooval2  9917  unirnioo  9975  ioorebasg  9977  elrege0  9978  fzval2  10013  fzen  10045  fzprval  10084  fztpval  10085  uzdisj  10095  ige2m1fz  10112  fz01or  10113  fz1ssfz0  10119  fz0sn  10123  fz0tp  10124  fz0to3un2pr  10125  fz0to4untppr  10126  nn0disj  10140  1fv  10141  4fvwrd4  10142  fzo0ss1  10176  fzo01  10218  fzo12sn  10219  fzo0to2pr  10220  fzo0to3tp  10221  fzo0to42pr  10222  qbtwnxr  10260  flval  10274  modqfrac  10339  modqmulnn  10344  q2txmodxeq0  10386  frecuzrdgdom  10420  frecuzrdgfun  10422  frecuzrdgsuct  10426  frechashgf1o  10430  nnct  10437  fxnn0nninf  10440  0tonninf  10441  1tonninf  10442  iseqvalcbv  10459  ser0f  10517  0exp0e1  10527  qexpcl  10538  qexpclz  10543  m1expcl2  10544  1exp  10551  sqvali  10602  sqcli  10603  sqeq0i  10604  resqcli  10607  sq1  10616  neg1sqe1  10617  iexpcyc  10627  qsqeqor  10633  facnn  10709  fac0  10710  fac1  10711  fac2  10713  fac3  10714  fac4  10715  bcval  10731  bcm1k  10742  bcpasc  10748  bccl  10749  4bc3eq4  10755  4bc2eq6  10756  hashinfom  10760  hashennn  10762  hashfz1  10765  fihasheq0  10775  hash0  10778  hashsng  10780  fihashen1  10781  omgadd  10784  hashp1i  10792  hashxp  10808  fimaxq  10809  zfz1iso  10823  shftidt2  10843  cjexp  10904  re0  10906  im0  10907  re1  10908  im1  10909  cj0  10912  cji  10913  recli  10922  imcli  10923  cjcli  10924  replimi  10925  cjcji  10926  reim0bi  10927  rerebi  10928  cjrebi  10929  recji  10930  imcji  10931  cjmulrcli  10932  cjmulvali  10933  cjmulge0i  10934  renegi  10935  imnegi  10936  cjnegi  10937  addcji  10938  uzin2  10998  rexanuz  10999  rexfiuz  11000  sqrtrval  11011  sqrt0  11015  resqrexlemcalc3  11027  resqrexlemcvg  11030  resqrex  11037  abs0  11069  absi  11070  qabsor  11086  absimle  11095  recan  11120  caubnd2  11128  leabsi  11139  absrei  11140  sqrtpclii  11141  sqrtgt0ii  11142  absvalsqi  11151  absvalsq2i  11152  abscli  11153  absge0i  11154  absval2i  11155  abs00i  11156  absgt0api  11157  absnegi  11158  abscji  11159  releabsi  11160  infxrnegsupex  11273  xrbdtri  11286  cbvsum  11370  sumeq1i  11373  sum0  11398  isumz  11399  fisumss  11402  fsumsersdc  11405  fsumadd  11416  isumclim  11431  isumclim3  11433  fsumcnv  11447  modfsummodlem1  11466  fsumrelem  11481  binomlem  11493  binom  11494  arisum2  11509  expcnv  11514  0.999...  11531  prodf1f  11553  cbvprod  11568  prodeq1i  11571  zproddc  11589  zprodap0  11591  prod0  11595  fprodssdc  11600  prodsnf  11602  fprodcnv  11635  fprodge0  11647  fprodge1  11649  ef0lem  11670  esum  11672  ere  11680  ege2le3  11681  ef0  11682  eff2  11690  efsep  11701  reeff1  11710  sin0  11739  cos0  11740  ef01bndlem  11766  cos2bnd  11770  sincos1sgn  11774  sincos2sgn  11775  sin4lt0  11776  eirr  11788  0dvds  11820  dvds1  11861  z0even  11918  n2dvdsm1  11920  z2even  11921  n2dvds3  11922  ndvdssub  11937  ndvdsi  11940  flodddiv4  11941  zsupssdc  11957  gcddvds  11966  gcd1  11990  6gcd4e2  11998  bezoutlembi  12008  dfgcd3  12013  dfgcd2  12017  lcmval  12065  lcmcllem  12069  lcmledvds  12072  3lcm2e6woprm  12088  qredeu  12099  isprm2lem  12118  isprm3  12120  prm2orodd  12128  isprm5lem  12143  sqrt2irr0  12166  pw2dvds  12168  phicl2  12216  phi1  12221  dfphi2  12222  phiprmpw  12224  eulerthlemrprm  12231  eulerthlemh  12233  odzval  12243  oddprm  12261  pczpre  12299  pcdiv  12304  pc0  12306  pcqdiv  12309  pcrec  12310  pcexp  12311  pcxcl  12313  pcdvdstr  12328  pc2dvds  12331  dvdsprmpweqnn  12337  pcmpt  12343  qexpz  12352  pockthi  12358  1arith2  12368  ennnfonelemp1  12409  ennnfonelem1  12410  ennnfonelemkh  12415  ennnfonelemex  12417  ennnfonelemnn0  12425  ennnfonelemr  12426  exmidunben  12429  ctinfomlemom  12430  ctinfom  12431  ctinf  12433  qnnen  12434  omctfn  12446  omiunct  12447  ssnnctlemct  12449  nninfdc  12456  structcnvcnv  12480  structfun  12482  structfn  12483  ndxarg  12487  ndxid  12488  setsresg  12502  setsslnid  12516  basmex  12523  basmexd  12524  strleun  12565  strle1g  12567  prdsex  12723  imasaddfnlemg  12740  quslem  12750  xpsfrnel  12768  xpsff1o  12773  ismgmn0  12782  fn0g  12799  0g0  12800  rmodislmodlem  13445  rmodislmod  13446  cnfldex  13543  cnfldbas  13544  cnfldadd  13545  cnfldmul  13546  cnfldcj  13547  cnring  13549  cnfld0  13550  cnfld1  13551  cnfldneg  13552  cnfldplusf  13553  cnfldsub  13554  cnfldmulg  13555  cnfldexp  13556  cnsubglem  13558  cnsubrglem  13559  gzsubrg  13561  zringring  13568  zringabl  13569  zringgrp  13570  zring1  13576  zringsubgval  13580  istopon  13598  topontopi  13601  toponunii  13602  toponrestid  13606  istps  13617  topontopn  13622  eltpsi  13626  eltg4i  13640  eltg3  13642  tg1  13644  tg2  13645  tgclb  13650  topnex  13671  sn0topon  13673  distps  13676  cldrcl  13687  sn0cld  13722  restco  13759  lmrcl  13776  ssidcn  13795  cnconst2  13818  cnptopresti  13823  cnptoprest  13824  txuni2  13841  txbas  13843  eltx  13844  txcnp  13856  upxp  13857  txcnmpt  13858  uptx  13859  txcn  13860  txrest  13861  txlm  13864  cnmptid  13866  cnmpt1st  13873  cnmpt2nd  13874  hmeofn  13887  psmetge0  13916  ismeti  13931  xmetunirn  13943  xmetge0  13950  unirnblps  14007  unirnbl  14008  mopnex  14090  qtopbasss  14106  retop  14109  uniretop  14110  iooretopg  14113  cnxmet  14116  cntoptopon  14117  cnbl0  14119  rexmet  14126  blssioo  14130  tgioo  14131  tgqioo  14132  cnopnap  14179  limcresi  14220  dvfvalap  14235  dvidlemap  14245  dvcnp2cntop  14248  dvcoapbr  14256  dvexp2  14261  dvrecap  14262  dveflem  14272  dvef  14273  reeff1o  14279  sin0pilem1  14287  sin0pilem2  14288  pilem3  14289  pigt2lt4  14290  pire  14292  sinhalfpilem  14297  pidiv2halves  14301  cosneghalfpi  14304  cospi  14306  efipi  14307  sin2pi  14309  cos2pi  14310  ef2pi  14311  cosq14gt0  14338  coseq00topi  14341  coseq0negpitopi  14342  sincos4thpi  14346  sincos6thpi  14348  sincos3rdpi  14349  pigt3  14350  cos02pilt1  14357  ioocosf1o  14360  dfrelog  14366  relogf1o  14367  relogcl  14368  relogiso  14379  rpcxpsqrt  14427  rpabscxpbnd  14444  2logb9irr  14474  2logb9irrALT  14477  sqrt2cxp2logb9e3  14478  2irrexpq  14479  2logb9irrap  14480  2irrexpqap  14481  lgsdir2lem1  14514  lgsdir2lem2  14515  lgsdir2lem4  14517  lgsdir2lem5  14518  lgsdi  14523  m1lgs  14537  2lgsoddprmlem2  14539  2lgsoddprmlem3c  14542  2lgsoddprmlem3d  14543  2sqlem9  14556  2sqlem10  14557  ex-fl  14562  ex-ceil  14563  ex-exp  14564  ex-fac  14565  ex-gcd  14568  bj-stfal  14579  bj-stst  14582  bj-dcfal  14592  bj-dcdc  14596  bj-stdc  14597  bj-dcst  14598  bj-el2oss1o  14611  elabf2  14619  bd0  14661  bdeli  14683  bdcriota  14720  bdbm1.3ii  14728  bdinex1  14736  bdssexi  14740  bj-inex  14744  bj-snex  14750  bj-sucex  14760  bj-d0clsepcl  14762  bj-omind  14771  bj-om  14774  bj-2inf  14775  bj-peano2  14776  bdpeano5  14780  bj-omssonALT  14800  bj-inf2vnlem1  14807  bj-omex2  14814  bj-nn0sucALT  14815  012of  14830  2o01f  14831  subctctexmid  14835  nninfall  14843  nninfsellemqall  14849  nninfsellemeqinf  14850  nninfomnilem  14852  nninfomni  14853  exmidsbthrlem  14855  sbthom  14859  isomninnlem  14863  isomninn  14864  cvgcmp2nlemabs  14865  iooreen  14868  trilpolemisumle  14871  trilpolemeq1  14873  trilpo  14876  trirec0  14877  apdifflemr  14880  iswomninnlem  14882  iswomninn  14883  ismkvnnlem  14885  ismkvnn  14886  redcwlpo  14888  dcapnconst  14894  nconstwlpolem0  14896  nconstwlpo  14899  neapmkv  14901  neap0mkv  14902  taupi  14906