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  271  notbii  320  biluk  387  pm5.19  388  pm3.24  404  dfbi  477  pm4.71i  561  pm5.32i  576  biadani  819  biadanii  821  imori  853  ori  860  pm5.16  1013  dn1  1057  3ori  1425  cadan  1611  nic-dfim  1672  nic-dfneg  1673  nic-mp  1674  nic-mpALT  1675  tbw-negdf  1702  rb-imdf  1753  nfri  1792  mpgbi  1801  19.35i  1882  nfim1  2193  19.36i  2225  ax6  2384  sbie  2502  datisi  2676  disamis  2677  dimatis  2684  fresison  2685  bamalip  2688  axi12  2702  eqcomi  2742  eqtri  2761  eleqtri  2832  nfnfc  2916  neii  2943  necomi  2996  neeqtri  3014  neli  3049  nrex  3075  rexlimivOLD  3185  rexlimi  3257  nfra2wOLD  3298  eueqi  3704  euxfr2w  3715  euxfr2  3717  reuxfrd  3743  cdeqri  3761  sseqtri  4017  3sstr3i  4023  pssn2lp  4100  equncomi  4154  unssi  4184  ssini  4230  unabs  4253  inabs  4254  dfin4  4266  vn0  4337  difidALT  4370  ab0orv  4377  ab0orvALT  4378  disjdif  4470  difin0  4472  pwundif  4625  snid  4663  rabrsn  4727  iinrab2  5072  symdifv  5088  rintn0  5111  breqtri  5172  axsepgfromrep  5296  bm1.3ii  5301  ax6vsep  5302  notzfaus  5360  zfpow  5363  dtruALT2  5367  dtruALT  5385  reusv2lem4  5398  dtru  5435  el  5436  dtruOLD  5440  op1stb  5470  copsexgw  5489  copsexg  5490  uniop  5514  rn0  5923  dmresi  6049  somincom  6132  cnvimassrndm  6148  cnvcnv  6188  elid  6195  rescnvcnv  6200  cnvcnvres  6201  cocnvcnv2  6254  cores2  6255  co01  6257  cnviin  6282  predres  6337  iota4an  6522  fnopab  6685  mpt0  6689  fnmpti  6690  f1cnvcnv  6794  f1ovi  6869  eliman0  6928  fvco4i  6988  cnvimainrn  7064  fmpti  7107  funiunfv  7242  oprabss  7510  relmptopab  7651  zfun  7721  tfinds2  7848  omon  7862  2nd0  7977  f1stres  7994  f2ndres  7995  cnvoprab  8041  relmpoopab  8075  df1st2  8079  df2nd2  8080  fsplit  8098  frpoins3xpg  8121  frpoins3xp3g  8122  poxp2  8124  poseq  8139  reldmtpos  8214  dftpos4  8225  tpostpos  8226  tpos0  8236  frrlem4  8269  wfrlem4OLD  8307  smo0  8353  tfrlem14  8386  tfrlem16  8388  rdgsucg  8418  rdglimg  8420  frfnom  8430  oawordeulem  8550  uniixp  8911  dfdom2  8970  ssdomg  8992  xpcomf1o  9057  sbthlem5  9083  sdom0  9104  limensuci  9149  1sdom2  9236  fiint  9320  fidomdm  9325  residfi  9329  pwfilemOLD  9342  mptfi  9347  fisn  9418  dffi3  9422  ordtypelem6  9514  ordtypelem7  9515  wemaplem2  9538  harwdom  9582  suc11reg  9610  zfinf  9630  axinf2  9631  noinfep  9651  cantnfvalf  9656  cantnflt  9663  cantnf0  9666  cantnf  9684  ttrclco  9709  tz9.1c  9721  tc2  9733  r111  9766  r1tr2  9768  r1ordg  9769  r1sssuc  9774  r1val1  9777  tz9.13  9782  r1elssi  9796  pwwf  9798  rankopb  9843  rankeq0b  9851  ranksuc  9856  rankmapu  9869  rankxplim3  9872  rankxpsuc  9873  cp  9882  karden  9886  card0  9949  cardlim  9963  cardom  9977  infxpenlem  10004  alephsuc2  10071  alephgeom  10073  unialeph  10092  dfac4  10113  dfacacn  10132  dju1dif  10163  dju1p1e2  10164  infdju1  10180  ackbij1lem13  10223  ackbij2  10234  cf0  10242  cfsuc  10248  cfom  10255  cfslb2n  10259  ominf4  10303  fin23lem17  10329  fin23lem28  10331  fin23lem30  10333  fin23lem31  10334  fin23lem40  10342  isfin1-3  10377  dfacfin7  10390  fin1a2lem6  10396  itunitc1  10411  axcc3  10429  dcomex  10438  axdc2lem  10439  axcclem  10448  zfac  10451  ac3  10453  ackm  10456  axac2  10457  axac  10458  axaci  10459  cardeqv  10460  numth2  10462  numth  10463  dmct  10515  brdom3  10519  fin71ac  10524  cardf  10541  aleph1  10562  cfpwsdom  10575  smobeth  10577  zfcndrep  10605  zfcndpow  10607  zfcndac  10610  gch2  10666  wunex3  10732  tskpr  10761  inar1  10766  rankcf  10768  tskcard  10772  tskuni  10774  grothpw  10817  axgroth4  10823  grothprim  10825  inaprc  10827  dmaddpi  10881  dmmulpi  10882  1lt2pi  10896  addpqf  10935  mulpqf  10937  1lt2nq  10964  supsrlem  11102  ssxr  11279  gtso  11291  subf  11458  negne0i  11531  mulnzcnopr  11856  infrenegsup  12193  nnne0  12242  halflt1  12426  nn0ssz  12577  3halfnz  12637  zeo  12644  numlt  12698  numltc  12699  le9lt10  12700  decle  12707  uzf  12821  xaddf  13199  xsubge0  13236  xmulf  13247  ixxf  13330  ixxssxr  13332  iooval2  13353  ioof  13420  unirnioo  13422  dfioo2  13423  fzval2  13483  fzf  13484  0nelfz1  13516  fz10  13518  fzpreddisj  13546  4fvwrd4  13617  fzof  13625  fzo0  13652  fldiv4p1lem1div2  13796  fldiv4lem1div2  13798  om2uzoi  13916  faclbnd4lem1  14249  hashkf  14288  hashgval  14289  hashinf  14291  hashresfn  14296  hashnn0n0nn  14347  hashge3el3dif  14443  rev0  14710  s2dm  14837  f1oun2prg  14864  trclublem  14938  sqrt2gt1lt2  15217  limsupgord  15412  fclim  15493  fsumrelem  15749  ackbijnn  15770  incexclem  15778  incexc  15779  arisum2  15803  georeclim  15814  geoisumr  15820  0.999...  15823  risefall0lem  15966  ege2le3  16029  sin0  16088  ef01bndlem  16123  cos2bnd  16127  cos01gt0  16130  sincos2sgn  16133  sin4lt0  16134  rpnnen2lem3  16155  rpnnen2lem9  16161  rexpen  16167  cnso  16186  dvdslelem  16248  divalglem1  16333  divalglem5  16336  divalglem6  16337  divalglem10  16341  flodddiv4  16352  0bits  16376  sadcf  16390  sadcadd  16395  bitsshft  16412  smupf  16415  gcdf  16449  eucalgf  16516  2prm  16625  dfphi2  16703  pockthi  16836  prmrec  16851  vdwapf  16901  vdwlem6  16915  karatsuba  17013  1259lem5  17064  2503lem3  17068  4001lem4  17073  structcnvcnv  17082  structfn  17085  strleun  17086  imasvscafn  17479  xpsff1o  17509  wunnat  17903  wunnatOLD  17904  dfinito3  17951  dftermo3  17952  eldmcoa  18011  coapm  18017  catcfuccl  18065  catcfucclOLD  18066  catcxpccl  18155  catcxpcclOLD  18156  yonedainv  18230  smndex1bas  18783  smndex1n0mnd  18789  grpinvfvi  18863  mulgfvi  18950  symgsssg  19328  symgfisg  19329  psgnunilem5  19355  sylow3lem2  19489  oppglsm  19503  efgmf  19574  efgval  19578  efgsf  19590  0frgp  19640  dmdprd  19860  dprdval  19865  invrfval  20192  drngui  20310  rmodislmod  20528  rmodislmodOLD  20529  lssintcl  20563  cnfldfunALT  20942  cnfldfunALTOLD  20943  cnfld0  20954  cnfld1  20955  cnfldsub  20958  xrsds  20973  psgnghm  21117  zrhpsgnmhm  21121  ocv1  21216  dsmmbas2  21276  mplsubrglem  21545  opsrtoslem2  21599  mdetralt  22092  maducoeval2  22124  eltpsi  22429  unitg  22452  fctop  22489  cctop  22491  ppttop  22492  epttop  22494  leordtvallem1  22696  leordtvallem2  22697  iccordt  22700  iscnp2  22725  discmp  22884  conncompcld  22920  1stcrestlem  22938  2ndcdisj  22942  topnlly  22977  disllycmp  22984  dis1stc  22985  txuni2  23051  xkotf  23071  dfac14lem  23103  prdstps  23115  txindis  23120  tx1stc  23136  xkohaus  23139  xkoptsub  23140  cnmpt1st  23154  cnmpt2nd  23155  ptcmpfi  23299  trfil1  23372  fin1aufil  23418  tgpconncompeqg  23598  tgpconncomp  23599  trust  23716  met1stc  24012  dscmet  24063  retopon  24262  cnfldtopon  24281  xrsxmet  24307  xrsmopn  24310  iimulcn  24436  icopnfhmeo  24441  iccpnfhmeo  24443  xrhmeo  24444  cnheiborlem  24452  lebnumii  24464  ishtpy  24470  htpycc  24478  pco1  24513  pcohtpylem  24517  pcopt  24520  pcopt2  24521  pcoass  24522  pcorevlem  24524  rrxcph  24891  rrx0el  24897  ovoliunlem3  25003  ovolicc1  25015  ovolicc2  25021  volf  25028  ioorf  25072  dyadf  25090  dyadmbl  25099  vitalilem5  25111  vitali  25112  mbfimaopnlem  25154  mbflimsup  25165  0plef  25171  i1fima  25177  i1fima2  25178  i1fd  25180  itg1ge0  25185  itg10  25187  i1f1lem  25188  i1fadd  25194  i1fmul  25195  i1fmulc  25203  mbfi1fseqlem5  25219  itg2addlem  25258  reldv  25369  dvbsss  25401  dvef  25479  lhop1lem  25512  deg1fvi  25585  plypf1  25708  coeeulem  25720  coeeu  25721  vieta1lem2  25806  aannenlem3  25825  aalioulem3  25829  dvradcnv  25915  pserulm  25916  pserdvlem2  25922  sinhalfpilem  25955  sincos4thpi  26005  tan4thpi  26006  sincos6thpi  26007  pige3ALT  26011  resinf1o  26027  tanord1  26028  tanregt0  26030  efabl  26041  relogrn  26052  dfrelog  26056  logneg  26078  logltb  26090  logcn  26137  logf1o2  26140  dvlog  26141  efopnlem2  26147  efopn  26148  logccv  26153  dvsqrt  26230  dvcnsqrt  26232  cxpcn3  26236  logblog  26277  angpined  26315  1cubr  26327  asinsin  26377  asin1  26379  reasinsin  26381  atan0  26393  atanbnd  26411  atan1  26413  log2cnv  26429  log2ub  26434  log2le1  26435  birthday  26439  amgmlem  26474  emcllem5  26484  emgt0  26491  harmonicbnd3  26492  ftalem3  26559  basellem4  26568  sgmf  26629  ppi1  26648  cht1  26649  vma1  26650  ppiltx  26661  sqff1o  26666  ppiublem1  26685  ppiublem2  26686  ppiub  26687  chtub  26695  dchreq  26741  bposlem7  26773  bposlem8  26774  bposlem9  26775  lgsdir2lem2  26809  lgsdir2lem3  26810  chebbnd1  26955  chto1ub  26959  chpo1ubb  26964  pntibndlem1  27072  nosgnn0  27141  sltsolem1  27158  bdayfo  27160  nolt02o  27178  nogt01o  27179  noetasuplem4  27219  noetainflem4  27223  scutbdaybnd2lim  27298  madeun  27358  scutfo  27378  addsproplem2  27434  addsproplem7  27439  addsprop  27440  negsprop  27489  mulsproplem13  27564  mulsproplem14  27565  mulsprop  27566  tgldimor  27733  tglnfn  27778  axlowdimlem4  28183  axlowdimlem16  28195  axlowdim  28199  upgrfi  28331  lfgrnloop  28365  lfuhgr1v0e  28491  usgrexmplef  28496  usgrres  28545  vdegp1bi  28774  vtxdginducedm1lem2  28777  pthdlem2  29005  wpthswwlks2on  29195  0ewlk  29347  0pth  29358  konigsbergiedgw  29481  konigsberglem1  29485  konigsberglem2  29486  konigsberglem3  29487  konigsberglem4  29488  konigsberglem5  29489  ex-dif  29656  ex-un  29657  ex-in  29658  ex-fl  29680  avril1  29696  9p10ne21fool  29704  n0lplig  29714  cnidOLD  29813  cnnvm  29913  ipasslem8  30068  ipasslem10  30070  hvsubf  30246  normlem1  30341  normlem6  30346  normlem7  30347  norm-ii-i  30368  norm3adifii  30379  hilid  30392  hlimf  30468  hhssabloi  30493  hhssnv  30495  hhshsslem1  30498  shincli  30593  shsval2i  30618  shs0i  30680  chj0i  30686  chm1i  30687  chincli  30691  chdmm1i  30708  shjshsi  30723  chsup0  30779  h1de2bi  30785  spansnpji  30809  cmcmlem  30822  cmcmii  30828  cmcm2ii  30829  cmcm3ii  30830  pjidmi  30904  pjssmii  30912  pj0i  30924  pjocini  30929  mayetes3i  30960  df0op2  30983  hoaddcomi  31003  hoaddassi  31007  hocadddiri  31010  hocsubdiri  31011  hoaddridi  31017  ho0coi  31019  hoid1i  31020  hoid1ri  31021  hodseqi  31025  honegsubi  31027  adj1o  31125  hoddii  31220  lnopunilem1  31241  lnopunilem2  31242  nmcopexi  31258  nmcopex  31260  nmcoplb  31261  nmcfnexi  31282  nmcfnex  31284  nmcfnlb  31285  adjbd1o  31316  adjcoi  31331  nmopcoadji  31332  opsqrlem6  31376  pjsdii  31386  pjddii  31387  pjidmcoi  31408  pjtoi  31410  pjin1i  31423  pjclem1  31426  stji1i  31473  reuxfrdf  31709  inindif  31732  iuninc  31770  fnresin  31828  rinvf1o  31832  suppss2f  31841  xppreima  31849  ofoprabco  31867  fressupp  31888  supppreima  31891  fsupprnfi  31892  gtiso  31900  df1stres  31903  df2ndres  31904  snct  31916  padct  31922  fsuppcurry1  31928  fsuppcurry2  31929  ffsrn  31932  fpwrelmapffs  31937  fzodif1  31982  nnindf  32003  nn0min  32004  dp2lt  32029  dp2ltsuc  32030  dp2ltc  32031  dplti  32049  dpmul  32057  dpmul4  32058  ressplusf  32105  xrsclat  32159  xrge0base  32164  xrge00  32165  xrnarchi  32308  1fldgenq  32381  xrge0slmod  32432  ply1degltdimlem  32652  ccfldsrarelvec  32690  ccfldextdgrr  32691  locfinreflem  32758  locfinref  32759  unicls  32821  sqsscirc1  32826  mhmhmeotmd  32845  rmulccn  32846  raddcn  32847  xrge0iifiso  32853  xrge0iifhmeo  32854  lmxrge0  32870  cnzh  32888  rezh  32889  qqh0  32902  qqh1  32903  qqhre  32938  rrhre  32939  esumnul  32984  esum0  32985  esumsnf  33000  esumpfinvallem  33010  esumpfinvalf  33012  esumpcvgval  33014  esumcvgsum  33024  esumsup  33025  esumcvgre  33027  sigaclfu2  33057  dmsigagen  33080  ddemeas  33172  mbfmvolf  33203  br2base  33206  omssubadd  33237  sibfof  33277  sitg0  33283  eulerpartlemt  33308  eulerpartgbij  33309  0rrv  33388  coinfliplem  33415  coinflipprob  33416  coinfliprv  33419  ballotlem2  33425  ballotlem4  33435  ballotlem5  33436  ballotlemi1  33439  ballotlem7  33472  ballotth  33474  signsplypnf  33499  signsply0  33500  signsw0g  33505  signswch  33510  signsvf0  33529  hashreprin  33570  reprfz1  33574  chtvalz  33579  hgt750lemd  33598  hgt750lem  33601  hgt750lem2  33602  bnj1098  33732  bnj1109  33735  bnj1131  33736  bnj1533  33801  bnj151  33826  bnj580  33862  bnj852  33870  bnj864  33871  bnj865  33872  bnj978  33898  bnj1021  33915  bnj907  33916  bnj1093  33929  bnj1145  33942  bnj1172  33950  bnj1174  33952  bnj1176  33954  bnj1186  33956  fineqvac  34035  subfacf  34104  subfacp1lem1  34108  subfacp1lem5  34113  subfacp1lem6  34114  subfacval3  34118  erdszelem2  34121  kur14lem4  34138  ioosconn  34176  iccllysconn  34179  satfn  34284  fmlaomn0  34319  gonan0  34321  goaln0  34322  elnanelprv  34358  msrfo  34475  mthmpps  34511  problem5  34592  quad3  34593  circum  34597  axextprim  34608  axrepprim  34609  axunprim  34610  axinfprim  34613  axacprim  34614  logi  34642  bcneg1  34644  setinds  34688  dfon2lem2  34694  dfon2lem4  34696  axextdfeq  34707  fobigcup  34810  snelsingles  34832  fullfunfnv  34856  fullfunfv  34857  rankaltopb  34889  rank0  35080  rankeq1o  35081  hfuni  35094  gg-iimulcn  35107  fneer  35176  neibastop1  35182  nabi1i  35217  nabi2i  35218  limsucncmpi  35268  knoppcnlem8  35314  knoppcnlem11  35317  cnndvlem1  35351  bj-consensusALT  35394  bj-sbidmOLD  35667  bj-n0i  35770  bj-snsetex  35782  bj-tagss  35799  bj-2upln0  35842  bj-2upln1upl  35843  bj-nuliota  35876  bj-0int  35920  bj-elid5  35988  bj-inftyexpitaufo  36021  bj-pinftyccb  36040  bj-minftyccb  36044  bj-pinftynminfty  36046  bj-isrvec  36113  iccioo01  36146  f1omptsnlem  36155  mptsnunlem  36157  topdifinffinlem  36166  relowlpssretop  36183  1oequni2o  36187  pibt2  36236  imadifss  36401  tan2h  36418  poimirlem3  36429  poimirlem9  36435  poimirlem16  36442  poimirlem17  36443  poimirlem18  36444  poimirlem19  36445  poimirlem20  36446  poimirlem22  36448  poimirlem30  36456  mblfinlem1  36463  mblfinlem2  36464  ovoliunnfl  36468  voliunnfl  36470  itg2addnclem  36477  itg2addnclem2  36478  asindmre  36509  areacirclem1  36514  fdc  36551  cntotbnd  36602  heiborlem6  36622  rrnval  36633  reheibor  36645  rngosn3  36730  brcnvrabga  37149  cnvresrn  37155  moantr  37171  inxp2  37174  dfxrn2  37184  cnvcosseq  37245  refrelcosslem  37270  1cosscnvxrn  37283  redundss3  37436  refrelsredund3  37442  refrelredund3  37445  eqvrel0  37594  eqvrelid  37597  prter2  37689  renegclALT  37771  mapdunirnN  40459  lcmeprodgcdi  40810  3factsumint2  40825  3factsumint3  40826  3factsumint4  40827  3factsumint  40828  lcmineqlem4  40835  3lexlogpow5ineq1  40857  3lexlogpow2ineq1  40861  dvrelogpow2b  40871  aks4d1p1p4  40874  aks4d1p8  40890  aks6d1c2p2  40895  2ap1caineq  40899  sticksstones1  40900  sticksstones2  40901  metakunt6  40928  metakunt24  40946  sqdeccom12  41151  resubf  41198  sn-0ne2  41223  sn-subf  41245  sn-nnne0  41265  sn-0lt1  41279  reneg1lt0  41281  rntrclfvOAI  41362  diophrw  41430  rabren3dioph  41486  pellexlem6  41505  pellex  41506  frmx  41585  frmy  41586  jm2.23  41668  jm2.27dlem3  41683  axac10  41705  pw2f1ocnv  41709  kelac2lem  41739  lmhmlnmsplit  41762  pwfi2f1o  41771  frlmpwfi  41773  insucid  42087  nla0003  42109  ifpbiidcor  42158  sucomisnotcard  42228  alephiso2  42242  alephiso3  42243  cnvnonrel  42272  rnnonrel  42275  resnonrel  42276  cononrel1  42278  cononrel2  42279  fvnonrel  42281  cnvcnvintabd  42284  cnvintabd  42287  rclexi  42299  rtrclex  42301  clcnvlem  42307  cnvrcl0  42309  dmtrcl  42311  rntrcl  42312  dfrtrcl5  42313  iunrelexp0  42386  dmtrclfvRP  42414  rntrclfv  42416  corcltrcl  42423  cotrclrcl  42426  0heALT  42467  frege54cor1a  42548  uneqsn  42709  clsk3nimkb  42724  int-sqdefd  42866  int-sqgeq0d  42871  rr-groth  42991  rr-grothprim  42992  rr-grothshort  42996  seff  43001  expgrowthi  43025  expgrowth  43027  binomcxplemnotnn0  43048  ee233  43213  ax6e2nd  43252  in1  43265  dfvd2ani  43277  dfvd2i  43279  dfvd3i  43286  dfvd3ani  43289  e0bi  43470  uun2221  43507  uun2221p1  43508  uun2221p2  43509  en3lpVD  43539  relopabVD  43595  ax6e2ndVD  43602  ax6e2ndALT  43624  pssnssi  43723  nnf1oxpnn  43827  icof  43851  fnmptif  43905  rn1st  43913  negpilt0  43925  xrgtso  43990  supxrleubrnmptf  44096  xrpnf  44131  rexanuz2nf  44138  ioontr  44159  iccdifioo  44163  iccdifprioo  44164  uzinico2  44210  fsummulc1f  44222  fsumiunss  44226  fnlimfvre2  44328  limsupreuz  44388  limsupvaluz2  44389  limsup10ex  44424  icccncfext  44538  dvcosre  44563  dvsinax  44564  ioodvbdlimc1lem2  44583  ioodvbdlimc2lem  44585  dvmptmulf  44588  dvnmul  44594  dvmptfprodlem  44595  dvnprodlem2  44598  stoweidlem1  44652  stoweidlem26  44677  stoweidlem34  44685  stoweidlem44  44695  stoweid  44714  stirlinglem5  44729  dirkercncflem1  44754  fourierdlem44  44802  fourierdlem56  44813  fourierdlem62  44819  fourierdlem89  44846  fourierdlem91  44848  fourierdlem100  44857  fourierdlem102  44859  fourierdlem103  44860  fourierdlem104  44861  fourierdlem108  44865  fourierdlem112  44869  fourierdlem114  44871  fouriersw  44882  rrndistlt  44941  gsumge0cl  45022  sge0tsms  45031  sge0ltfirpmpt2  45077  ovn0  45217  hoidmv1le  45245  hoidmvle  45251  ovnsubadd2lem  45296  ovolval4lem1  45300  vonioolem2  45332  smflimlem3  45424  nsssmfmbf  45430  axorbtnotaiffb  45548  axorbciffatcxorb  45550  abnotbtaxb  45560  euabsneu  45673  sprval  46082  fmtnoinf  46139  1nevenALTV  46294  nfermltl8rev  46345  nfermltl2rev  46346  nnsum3primes4  46391  tgblthelfgott  46418  tgoldbachlt  46419  ldepslinc  47092  ackval42  47284  rrx2plordso  47312  vsn  47398  sepfsepc  47462  alimp-no-surprise  47730  aacllem  47750  amgmwlem  47751  amgmlemALT  47752