Theorem mpbi 229

Description: An inference from a biconditional, related to modus ponens. (Contributed by NM, 11-May-1993.)

Hypotheses

Ref	Expression
mpbi.min	⊢ 𝜑
mpbi.maj	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
mpbi	⊢ 𝜓

Proof of Theorem mpbi

Step	Hyp	Ref	Expression
1		mpbi.min	. 2 ⊢ 𝜑
2		mpbi.maj	. . 3 ⊢ (𝜑 ↔ 𝜓)
3	2	biimpi 215	. 2 ⊢ (𝜑 → 𝜓)
4	1, 3	ax-mp 5	1 ⊢ 𝜓

Syntax hints:   ↔ wb 205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  pm5.74i  270  notbii  319  biluk  386  pm5.19  387  pm3.24  403  dfbi  476  pm4.71i  560  pm5.32i  575  biadani  818  biadanii  820  imori  852  ori  859  pm5.16  1012  dn1  1056  3ori  1424  cadan  1610  nic-dfim  1671  nic-dfneg  1672  nic-mp  1673  nic-mpALT  1674  tbw-negdf  1701  rb-imdf  1752  nfri  1791  mpgbi  1800  19.35i  1881  nfim1  2192  19.36i  2224  ax6  2383  sbie  2501  datisi  2675  disamis  2676  dimatis  2683  fresison  2684  bamalip  2687  axi12  2701  eqcomi  2741  eqtri  2760  eleqtri  2831  nfnfc  2915  neii  2942  necomi  2995  neeqtri  3013  neli  3048  nrex  3074  rexlimivOLD  3184  rexlimi  3256  nfra2wOLD  3297  eueqi  3705  euxfr2w  3716  euxfr2  3718  reuxfrd  3744  cdeqri  3762  sseqtri  4018  3sstr3i  4024  pssn2lp  4101  equncomi  4155  unssi  4185  ssini  4231  unabs  4254  inabs  4255  dfin4  4267  vn0  4338  difidALT  4371  ab0orv  4378  ab0orvALT  4379  disjdif  4471  difin0  4473  pwundif  4626  snid  4664  rabrsn  4728  iinrab2  5073  symdifv  5089  rintn0  5112  breqtri  5173  axsepgfromrep  5297  bm1.3ii  5302  ax6vsep  5303  notzfaus  5361  zfpow  5364  dtruALT2  5368  dtruALT  5386  reusv2lem4  5399  dtru  5436  el  5437  dtruOLD  5441  op1stb  5471  copsexgw  5490  copsexg  5491  uniop  5515  rn0  5925  dmresi  6051  somincom  6135  cnvimassrndm  6151  cnvcnv  6191  elid  6198  rescnvcnv  6203  cnvcnvres  6204  cocnvcnv2  6257  cores2  6258  co01  6260  cnviin  6285  predres  6340  iota4an  6525  fnopab  6688  mpt0  6692  fnmpti  6693  f1cnvcnv  6797  f1ovi  6872  eliman0  6931  fvco4i  6992  cnvimainrn  7068  fmpti  7113  funiunfv  7249  oprabss  7517  relmptopab  7658  zfun  7728  tfinds2  7855  omon  7869  2nd0  7984  f1stres  8001  f2ndres  8002  cnvoprab  8048  relmpoopab  8082  df1st2  8086  df2nd2  8087  fsplit  8105  frpoins3xpg  8128  frpoins3xp3g  8129  poxp2  8131  poseq  8146  reldmtpos  8221  dftpos4  8232  tpostpos  8233  tpos0  8243  frrlem4  8276  wfrlem4OLD  8314  smo0  8360  tfrlem14  8393  tfrlem16  8395  rdgsucg  8425  rdglimg  8427  frfnom  8437  oawordeulem  8556  uniixp  8917  dfdom2  8976  ssdomg  8998  xpcomf1o  9063  sbthlem5  9089  sdom0  9110  limensuci  9155  1sdom2  9242  fiint  9326  fidomdm  9331  residfi  9335  pwfilemOLD  9348  mptfi  9353  fisn  9424  dffi3  9428  ordtypelem6  9520  ordtypelem7  9521  wemaplem2  9544  harwdom  9588  suc11reg  9616  zfinf  9636  axinf2  9637  noinfep  9657  cantnfvalf  9662  cantnflt  9669  cantnf0  9672  cantnf  9690  ttrclco  9715  tz9.1c  9727  tc2  9739  r111  9772  r1tr2  9774  r1ordg  9775  r1sssuc  9780  r1val1  9783  tz9.13  9788  r1elssi  9802  pwwf  9804  rankopb  9849  rankeq0b  9857  ranksuc  9862  rankmapu  9875  rankxplim3  9878  rankxpsuc  9879  cp  9888  karden  9892  card0  9955  cardlim  9969  cardom  9983  infxpenlem  10010  alephsuc2  10077  alephgeom  10079  unialeph  10098  dfac4  10119  dfacacn  10138  dju1dif  10169  dju1p1e2  10170  infdju1  10186  ackbij1lem13  10229  ackbij2  10240  cf0  10248  cfsuc  10254  cfom  10261  cfslb2n  10265  ominf4  10309  fin23lem17  10335  fin23lem28  10337  fin23lem30  10339  fin23lem31  10340  fin23lem40  10348  isfin1-3  10383  dfacfin7  10396  fin1a2lem6  10402  itunitc1  10417  axcc3  10435  dcomex  10444  axdc2lem  10445  axcclem  10454  zfac  10457  ac3  10459  ackm  10462  axac2  10463  axac  10464  axaci  10465  cardeqv  10466  numth2  10468  numth  10469  dmct  10521  brdom3  10525  fin71ac  10530  cardf  10547  aleph1  10568  cfpwsdom  10581  smobeth  10583  zfcndrep  10611  zfcndpow  10613  zfcndac  10616  gch2  10672  wunex3  10738  tskpr  10767  inar1  10772  rankcf  10774  tskcard  10778  tskuni  10780  grothpw  10823  axgroth4  10829  grothprim  10831  inaprc  10833  dmaddpi  10887  dmmulpi  10888  1lt2pi  10902  addpqf  10941  mulpqf  10943  1lt2nq  10970  supsrlem  11108  ssxr  11285  gtso  11297  subf  11464  negne0i  11537  mulnzcnopr  11862  infrenegsup  12199  nnne0  12248  halflt1  12432  nn0ssz  12583  3halfnz  12643  zeo  12650  numlt  12704  numltc  12705  le9lt10  12706  decle  12713  uzf  12827  xaddf  13205  xsubge0  13242  xmulf  13253  ixxf  13336  ixxssxr  13338  iooval2  13359  ioof  13426  unirnioo  13428  dfioo2  13429  fzval2  13489  fzf  13490  0nelfz1  13522  fz10  13524  fzpreddisj  13552  4fvwrd4  13623  fzof  13631  fzo0  13658  fldiv4p1lem1div2  13802  fldiv4lem1div2  13804  om2uzoi  13922  faclbnd4lem1  14255  hashkf  14294  hashgval  14295  hashinf  14297  hashresfn  14302  hashnn0n0nn  14353  hashge3el3dif  14449  rev0  14716  s2dm  14843  f1oun2prg  14870  trclublem  14944  sqrt2gt1lt2  15223  limsupgord  15418  fclim  15499  fsumrelem  15755  ackbijnn  15776  incexclem  15784  incexc  15785  arisum2  15809  georeclim  15820  geoisumr  15826  0.999...  15829  risefall0lem  15972  ege2le3  16035  sin0  16094  ef01bndlem  16129  cos2bnd  16133  cos01gt0  16136  sincos2sgn  16139  sin4lt0  16140  rpnnen2lem3  16161  rpnnen2lem9  16167  rexpen  16173  cnso  16192  dvdslelem  16254  divalglem1  16339  divalglem5  16342  divalglem6  16343  divalglem10  16347  flodddiv4  16358  0bits  16382  sadcf  16396  sadcadd  16401  bitsshft  16418  smupf  16421  gcdf  16455  eucalgf  16522  2prm  16631  dfphi2  16709  pockthi  16842  prmrec  16857  vdwapf  16907  vdwlem6  16921  karatsuba  17019  1259lem5  17070  2503lem3  17074  4001lem4  17079  structcnvcnv  17088  structfn  17091  strleun  17092  imasvscafn  17485  xpsff1o  17515  wunnat  17909  wunnatOLD  17910  dfinito3  17957  dftermo3  17958  eldmcoa  18017  coapm  18023  catcfuccl  18071  catcfucclOLD  18072  catcxpccl  18161  catcxpcclOLD  18162  yonedainv  18236  smndex1bas  18789  smndex1n0mnd  18795  grpinvfvi  18869  mulgfvi  18958  symgsssg  19337  symgfisg  19338  psgnunilem5  19364  sylow3lem2  19498  oppglsm  19512  efgmf  19583  efgval  19587  efgsf  19599  0frgp  19649  dmdprd  19870  dprdval  19875  invrfval  20207  drngui  20367  rmodislmod  20545  rmodislmodOLD  20546  lssintcl  20580  cnfldfunALT  20963  cnfldfunALTOLD  20964  cnfld0  20975  cnfld1  20976  cnfldsub  20979  xrsds  20994  psgnghm  21139  zrhpsgnmhm  21143  ocv1  21238  dsmmbas2  21298  mplsubrglem  21569  opsrtoslem2  21623  mdetralt  22117  maducoeval2  22149  eltpsi  22454  unitg  22477  fctop  22514  cctop  22516  ppttop  22517  epttop  22519  leordtvallem1  22721  leordtvallem2  22722  iccordt  22725  iscnp2  22750  discmp  22909  conncompcld  22945  1stcrestlem  22963  2ndcdisj  22967  topnlly  23002  disllycmp  23009  dis1stc  23010  txuni2  23076  xkotf  23096  dfac14lem  23128  prdstps  23140  txindis  23145  tx1stc  23161  xkohaus  23164  xkoptsub  23165  cnmpt1st  23179  cnmpt2nd  23180  ptcmpfi  23324  trfil1  23397  fin1aufil  23443  tgpconncompeqg  23623  tgpconncomp  23624  trust  23741  met1stc  24037  dscmet  24088  retopon  24287  cnfldtopon  24306  xrsxmet  24332  xrsmopn  24335  iimulcn  24461  icopnfhmeo  24466  iccpnfhmeo  24468  xrhmeo  24469  cnheiborlem  24477  lebnumii  24489  ishtpy  24495  htpycc  24503  pco1  24538  pcohtpylem  24542  pcopt  24545  pcopt2  24546  pcoass  24547  pcorevlem  24549  rrxcph  24916  rrx0el  24922  ovoliunlem3  25028  ovolicc1  25040  ovolicc2  25046  volf  25053  ioorf  25097  dyadf  25115  dyadmbl  25124  vitalilem5  25136  vitali  25137  mbfimaopnlem  25179  mbflimsup  25190  0plef  25196  i1fima  25202  i1fima2  25203  i1fd  25205  itg1ge0  25210  itg10  25212  i1f1lem  25213  i1fadd  25219  i1fmul  25220  i1fmulc  25228  mbfi1fseqlem5  25244  itg2addlem  25283  reldv  25394  dvbsss  25426  dvef  25504  lhop1lem  25537  deg1fvi  25610  plypf1  25733  coeeulem  25745  coeeu  25746  vieta1lem2  25831  aannenlem3  25850  aalioulem3  25854  dvradcnv  25940  pserulm  25941  pserdvlem2  25947  sinhalfpilem  25980  sincos4thpi  26030  tan4thpi  26031  sincos6thpi  26032  pige3ALT  26036  resinf1o  26052  tanord1  26053  tanregt0  26055  efabl  26066  relogrn  26077  dfrelog  26081  logneg  26103  logltb  26115  logcn  26162  logf1o2  26165  dvlog  26166  efopnlem2  26172  efopn  26173  logccv  26178  dvsqrt  26257  dvcnsqrt  26259  cxpcn3  26263  logblog  26304  angpined  26342  1cubr  26354  asinsin  26404  asin1  26406  reasinsin  26408  atan0  26420  atanbnd  26438  atan1  26440  log2cnv  26456  log2ub  26461  log2le1  26462  birthday  26466  amgmlem  26501  emcllem5  26511  emgt0  26518  harmonicbnd3  26519  ftalem3  26586  basellem4  26595  sgmf  26656  ppi1  26675  cht1  26676  vma1  26677  ppiltx  26688  sqff1o  26693  ppiublem1  26712  ppiublem2  26713  ppiub  26714  chtub  26722  dchreq  26768  bposlem7  26800  bposlem8  26801  bposlem9  26802  lgsdir2lem2  26836  lgsdir2lem3  26837  chebbnd1  26982  chto1ub  26986  chpo1ubb  26991  pntibndlem1  27099  nosgnn0  27168  sltsolem1  27185  bdayfo  27187  nolt02o  27205  nogt01o  27206  noetasuplem4  27246  noetainflem4  27250  scutbdaybnd2lim  27326  madeun  27386  scutfo  27406  addsproplem2  27463  addsproplem7  27468  addsprop  27469  negsprop  27519  mulsproplem13  27594  mulsproplem14  27595  mulsprop  27596  n0scut  27714  tgldimor  27791  tglnfn  27836  axlowdimlem4  28241  axlowdimlem16  28253  axlowdim  28257  upgrfi  28389  lfgrnloop  28423  lfuhgr1v0e  28549  usgrexmplef  28554  usgrres  28603  vdegp1bi  28832  vtxdginducedm1lem2  28835  pthdlem2  29063  wpthswwlks2on  29253  0ewlk  29405  0pth  29416  konigsbergiedgw  29539  konigsberglem1  29543  konigsberglem2  29544  konigsberglem3  29545  konigsberglem4  29546  konigsberglem5  29547  ex-dif  29714  ex-un  29715  ex-in  29716  ex-fl  29738  avril1  29754  9p10ne21fool  29762  n0lplig  29774  cnidOLD  29873  cnnvm  29973  ipasslem8  30128  ipasslem10  30130  hvsubf  30306  normlem1  30401  normlem6  30406  normlem7  30407  norm-ii-i  30428  norm3adifii  30439  hilid  30452  hlimf  30528  hhssabloi  30553  hhssnv  30555  hhshsslem1  30558  shincli  30653  shsval2i  30678  shs0i  30740  chj0i  30746  chm1i  30747  chincli  30751  chdmm1i  30768  shjshsi  30783  chsup0  30839  h1de2bi  30845  spansnpji  30869  cmcmlem  30882  cmcmii  30888  cmcm2ii  30889  cmcm3ii  30890  pjidmi  30964  pjssmii  30972  pj0i  30984  pjocini  30989  mayetes3i  31020  df0op2  31043  hoaddcomi  31063  hoaddassi  31067  hocadddiri  31070  hocsubdiri  31071  hoaddridi  31077  ho0coi  31079  hoid1i  31080  hoid1ri  31081  hodseqi  31085  honegsubi  31087  adj1o  31185  hoddii  31280  lnopunilem1  31301  lnopunilem2  31302  nmcopexi  31318  nmcopex  31320  nmcoplb  31321  nmcfnexi  31342  nmcfnex  31344  nmcfnlb  31345  adjbd1o  31376  adjcoi  31391  nmopcoadji  31392  opsqrlem6  31436  pjsdii  31446  pjddii  31447  pjidmcoi  31468  pjtoi  31470  pjin1i  31483  pjclem1  31486  stji1i  31533  reuxfrdf  31769  inindif  31792  iuninc  31830  fnresin  31888  rinvf1o  31892  suppss2f  31901  xppreima  31909  ofoprabco  31927  fressupp  31948  supppreima  31951  fsupprnfi  31952  gtiso  31960  df1stres  31963  df2ndres  31964  snct  31976  padct  31982  fsuppcurry1  31988  fsuppcurry2  31989  ffsrn  31992  fpwrelmapffs  31997  fzodif1  32042  nnindf  32063  nn0min  32064  dp2lt  32089  dp2ltsuc  32090  dp2ltc  32091  dplti  32109  dpmul  32117  dpmul4  32118  ressplusf  32165  xrsclat  32219  xrge0base  32224  xrge00  32225  xrnarchi  32371  1fldgenq  32453  xrge0slmod  32504  ply1degltdimlem  32766  ccfldsrarelvec  32805  ccfldextdgrr  32806  locfinreflem  32889  locfinref  32890  unicls  32952  sqsscirc1  32957  mhmhmeotmd  32976  rmulccn  32977  raddcn  32978  xrge0iifiso  32984  xrge0iifhmeo  32985  lmxrge0  33001  cnzh  33019  rezh  33020  qqh0  33033  qqh1  33034  qqhre  33069  rrhre  33070  esumnul  33115  esum0  33116  esumsnf  33131  esumpfinvallem  33141  esumpfinvalf  33143  esumpcvgval  33145  esumcvgsum  33155  esumsup  33156  esumcvgre  33158  sigaclfu2  33188  dmsigagen  33211  ddemeas  33303  mbfmvolf  33334  br2base  33337  omssubadd  33368  sibfof  33408  sitg0  33414  eulerpartlemt  33439  eulerpartgbij  33440  0rrv  33519  coinfliplem  33546  coinflipprob  33547  coinfliprv  33550  ballotlem2  33556  ballotlem4  33566  ballotlem5  33567  ballotlemi1  33570  ballotlem7  33603  ballotth  33605  signsplypnf  33630  signsply0  33631  signsw0g  33636  signswch  33641  signsvf0  33660  hashreprin  33701  reprfz1  33705  chtvalz  33710  hgt750lemd  33729  hgt750lem  33732  hgt750lem2  33733  bnj1098  33863  bnj1109  33866  bnj1131  33867  bnj1533  33932  bnj151  33957  bnj580  33993  bnj852  34001  bnj864  34002  bnj865  34003  bnj978  34029  bnj1021  34046  bnj907  34047  bnj1093  34060  bnj1145  34073  bnj1172  34081  bnj1174  34083  bnj1176  34085  bnj1186  34087  fineqvac  34166  subfacf  34235  subfacp1lem1  34239  subfacp1lem5  34244  subfacp1lem6  34245  subfacval3  34249  erdszelem2  34252  kur14lem4  34269  ioosconn  34307  iccllysconn  34310  satfn  34415  fmlaomn0  34450  gonan0  34452  goaln0  34453  elnanelprv  34489  msrfo  34606  mthmpps  34642  problem5  34723  quad3  34724  circum  34728  axextprim  34745  axrepprim  34746  axunprim  34747  axinfprim  34750  axacprim  34751  logi  34779  bcneg1  34781  setinds  34825  dfon2lem2  34831  dfon2lem4  34833  axextdfeq  34844  fobigcup  34947  snelsingles  34969  fullfunfnv  34993  fullfunfv  34994  rankaltopb  35026  rank0  35217  rankeq1o  35218  hfuni  35231  gg-iimulcn  35244  gg-dfcnfld  35262  gg-cnfldfunALT  35273  gg-cnfld1  35276  fneer  35330  neibastop1  35336  nabi1i  35371  nabi2i  35372  limsucncmpi  35422  knoppcnlem8  35468  knoppcnlem11  35471  cnndvlem1  35505  bj-consensusALT  35548  bj-sbidmOLD  35821  bj-n0i  35924  bj-snsetex  35936  bj-tagss  35953  bj-2upln0  35996  bj-2upln1upl  35997  bj-nuliota  36030  bj-0int  36074  bj-elid5  36142  bj-inftyexpitaufo  36175  bj-pinftyccb  36194  bj-minftyccb  36198  bj-pinftynminfty  36200  bj-isrvec  36267  iccioo01  36300  f1omptsnlem  36309  mptsnunlem  36311  topdifinffinlem  36320  relowlpssretop  36337  1oequni2o  36341  pibt2  36390  imadifss  36555  tan2h  36572  poimirlem3  36583  poimirlem9  36589  poimirlem16  36596  poimirlem17  36597  poimirlem18  36598  poimirlem19  36599  poimirlem20  36600  poimirlem22  36602  poimirlem30  36610  mblfinlem1  36617  mblfinlem2  36618  ovoliunnfl  36622  voliunnfl  36624  itg2addnclem  36631  itg2addnclem2  36632  asindmre  36663  areacirclem1  36668  fdc  36705  cntotbnd  36756  heiborlem6  36776  rrnval  36787  reheibor  36799  rngosn3  36884  brcnvrabga  37303  cnvresrn  37309  moantr  37325  inxp2  37328  dfxrn2  37338  cnvcosseq  37399  refrelcosslem  37424  1cosscnvxrn  37437  redundss3  37590  refrelsredund3  37596  refrelredund3  37599  eqvrel0  37748  eqvrelid  37751  prter2  37843  renegclALT  37925  mapdunirnN  40613  lcmeprodgcdi  40964  3factsumint2  40979  3factsumint3  40980  3factsumint4  40981  3factsumint  40982  lcmineqlem4  40989  3lexlogpow5ineq1  41011  3lexlogpow2ineq1  41015  dvrelogpow2b  41025  aks4d1p1p4  41028  aks4d1p8  41044  aks6d1c2p2  41049  2ap1caineq  41053  sticksstones1  41054  sticksstones2  41055  metakunt6  41082  metakunt24  41100  sqdeccom12  41289  resubf  41342  sn-0ne2  41367  sn-subf  41389  sn-nnne0  41409  sn-0lt1  41423  reneg1lt0  41425  rntrclfvOAI  41517  diophrw  41585  rabren3dioph  41641  pellexlem6  41660  pellex  41661  frmx  41740  frmy  41741  jm2.23  41823  jm2.27dlem3  41838  axac10  41860  pw2f1ocnv  41864  kelac2lem  41894  lmhmlnmsplit  41917  pwfi2f1o  41926  frlmpwfi  41928  insucid  42242  nla0003  42264  ifpbiidcor  42313  sucomisnotcard  42383  alephiso2  42397  alephiso3  42398  cnvnonrel  42427  rnnonrel  42430  resnonrel  42431  cononrel1  42433  cononrel2  42434  fvnonrel  42436  cnvcnvintabd  42439  cnvintabd  42442  rclexi  42454  rtrclex  42456  clcnvlem  42462  cnvrcl0  42464  dmtrcl  42466  rntrcl  42467  dfrtrcl5  42468  iunrelexp0  42541  dmtrclfvRP  42569  rntrclfv  42571  corcltrcl  42578  cotrclrcl  42581  0heALT  42622  frege54cor1a  42703  uneqsn  42864  clsk3nimkb  42879  int-sqdefd  43021  int-sqgeq0d  43026  rr-groth  43146  rr-grothprim  43147  rr-grothshort  43151  seff  43156  expgrowthi  43180  expgrowth  43182  binomcxplemnotnn0  43203  ee233  43368  ax6e2nd  43407  in1  43420  dfvd2ani  43432  dfvd2i  43434  dfvd3i  43441  dfvd3ani  43444  e0bi  43625  uun2221  43662  uun2221p1  43663  uun2221p2  43664  en3lpVD  43694  relopabVD  43750  ax6e2ndVD  43757  ax6e2ndALT  43779  pssnssi  43878  nnf1oxpnn  43979  icof  44003  fnmptif  44055  rn1st  44063  negpilt0  44075  xrgtso  44140  supxrleubrnmptf  44246  xrpnf  44281  rexanuz2nf  44288  ioontr  44309  iccdifioo  44313  iccdifprioo  44314  uzinico2  44360  fsummulc1f  44372  fsumiunss  44376  fnlimfvre2  44478  limsupreuz  44538  limsupvaluz2  44539  limsup10ex  44574  icccncfext  44688  dvcosre  44713  dvsinax  44714  ioodvbdlimc1lem2  44733  ioodvbdlimc2lem  44735  dvmptmulf  44738  dvnmul  44744  dvmptfprodlem  44745  dvnprodlem2  44748  stoweidlem1  44802  stoweidlem26  44827  stoweidlem34  44835  stoweidlem44  44845  stoweid  44864  stirlinglem5  44879  dirkercncflem1  44904  fourierdlem44  44952  fourierdlem56  44963  fourierdlem62  44969  fourierdlem89  44996  fourierdlem91  44998  fourierdlem100  45007  fourierdlem102  45009  fourierdlem103  45010  fourierdlem104  45011  fourierdlem108  45015  fourierdlem112  45019  fourierdlem114  45021  fouriersw  45032  rrndistlt  45091  gsumge0cl  45172  sge0tsms  45181  sge0ltfirpmpt2  45227  ovn0  45367  hoidmv1le  45395  hoidmvle  45401  ovnsubadd2lem  45446  ovolval4lem1  45450  vonioolem2  45482  smflimlem3  45574  nsssmfmbf  45580  axorbtnotaiffb  45698  axorbciffatcxorb  45700  abnotbtaxb  45710  euabsneu  45823  sprval  46232  fmtnoinf  46289  1nevenALTV  46444  nfermltl8rev  46495  nfermltl2rev  46496  nnsum3primes4  46541  tgblthelfgott  46568  tgoldbachlt  46569  pzriprnglem4  46893  pzriprnglem9  46898  pzriprnglem14  46903  ldepslinc  47274  ackval42  47466  rrx2plordso  47494  vsn  47580  sepfsepc  47644  alimp-no-surprise  47912  aacllem  47932  amgmwlem  47933  amgmlemALT  47934