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  385  pm5.19  386  pm3.24  402  dfbi  475  pm4.71i  559  pm5.32i  574  biadani  819  biadanii  821  imori  853  ori  860  pm5.16  1012  dn1  1056  3ori  1422  cadan  1603  nic-dfim  1664  nic-dfneg  1665  nic-mp  1666  nic-mpALT  1667  tbw-negdf  1694  rb-imdf  1745  nfri  1784  mpgbi  1793  19.35i  1874  nfim1  2188  19.36i  2220  ax6  2379  sbie  2497  datisi  2671  disamis  2672  dimatis  2679  fresison  2680  bamalip  2683  axi12  2697  eqcomi  2737  eqtri  2756  eleqtri  2827  nfnfc  2911  neii  2938  necomi  2991  neeqtri  3009  neli  3044  nrex  3070  rexlimivOLD  3180  rexlimi  3252  nfra2wOLD  3293  eueqi  3703  euxfr2w  3714  euxfr2  3716  reuxfrd  3742  cdeqri  3760  sseqtri  4015  3sstr3i  4021  pssn2lp  4098  equncomi  4152  unssi  4182  ssini  4228  unabs  4251  inabs  4252  dfin4  4264  vn0  4335  difidALT  4368  ab0orv  4375  ab0orvALT  4376  disjdif  4468  difin0  4470  pwundif  4623  snid  4661  rabrsn  4725  iinrab2  5068  symdifv  5084  rintn0  5107  breqtri  5168  axsepgfromrep  5292  bm1.3ii  5297  ax6vsep  5298  notzfaus  5358  zfpow  5361  dtruALT2  5365  dtruALT  5383  reusv2lem4  5396  dtru  5433  el  5434  dtruOLD  5438  op1stb  5468  copsexgw  5487  copsexg  5488  uniop  5512  rn0  5923  dmresi  6050  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  6798  f1ovi  6873  eliman0  6932  fvco4i  6994  cnvimainrn  7071  fmpti  7117  funiunfv  7253  oprabss  7522  relmptopab  7666  zfun  7736  tfinds2  7863  omon  7877  2nd0  7995  f1stres  8012  f2ndres  8013  cnvoprab  8059  relmpoopab  8094  df1st2  8098  df2nd2  8099  fsplit  8117  frpoins3xpg  8140  frpoins3xp3g  8141  poxp2  8143  poseq  8158  reldmtpos  8234  dftpos4  8245  tpostpos  8246  tpos0  8256  frrlem4  8289  wfrlem4OLD  8327  smo0  8373  tfrlem14  8406  tfrlem16  8408  rdgsucg  8438  rdglimg  8440  frfnom  8450  oawordeulem  8569  uniixp  8934  dfdom2  8993  ssdomg  9015  xpcomf1o  9080  sbthlem5  9106  sdom0  9127  limensuci  9172  1sdom2  9259  fiint  9343  fidomdm  9348  residfi  9352  pwfilemOLD  9365  mptfi  9370  fisn  9445  dffi3  9449  ordtypelem6  9541  ordtypelem7  9542  wemaplem2  9565  harwdom  9609  suc11reg  9637  zfinf  9657  axinf2  9658  noinfep  9678  cantnfvalf  9683  cantnflt  9690  cantnf0  9693  cantnf  9711  ttrclco  9736  tz9.1c  9748  tc2  9760  r111  9793  r1tr2  9795  r1ordg  9796  r1sssuc  9801  r1val1  9804  tz9.13  9809  r1elssi  9823  pwwf  9825  rankopb  9870  rankeq0b  9878  ranksuc  9883  rankmapu  9896  rankxplim3  9899  rankxpsuc  9900  cp  9909  karden  9913  card0  9976  cardlim  9990  cardom  10004  infxpenlem  10031  alephsuc2  10098  alephgeom  10100  unialeph  10119  dfac4  10140  dfacacn  10159  dju1dif  10190  dju1p1e2  10191  infdju1  10207  ackbij1lem13  10250  ackbij2  10261  cf0  10269  cfsuc  10275  cfom  10282  cfslb2n  10286  ominf4  10330  fin23lem17  10356  fin23lem28  10358  fin23lem30  10360  fin23lem31  10361  fin23lem40  10369  isfin1-3  10404  dfacfin7  10417  fin1a2lem6  10423  itunitc1  10438  axcc3  10456  dcomex  10465  axdc2lem  10466  axcclem  10475  zfac  10478  ac3  10480  ackm  10483  axac2  10484  axac  10485  axaci  10486  cardeqv  10487  numth2  10489  numth  10490  dmct  10542  brdom3  10546  fin71ac  10551  cardf  10568  aleph1  10589  cfpwsdom  10602  smobeth  10604  zfcndrep  10632  zfcndpow  10634  zfcndac  10637  gch2  10693  wunex3  10759  tskpr  10788  inar1  10793  rankcf  10795  tskcard  10799  tskuni  10801  grothpw  10844  axgroth4  10850  grothprim  10852  inaprc  10854  dmaddpi  10908  dmmulpi  10909  1lt2pi  10923  addpqf  10962  mulpqf  10964  1lt2nq  10991  supsrlem  11129  ssxr  11308  gtso  11320  subf  11487  negne0i  11560  mulnzcnf  11885  infrenegsup  12222  nnne0  12271  halflt1  12455  nn0ssz  12606  3halfnz  12666  zeo  12673  numlt  12727  numltc  12728  le9lt10  12729  decle  12736  uzf  12850  xaddf  13230  xsubge0  13267  xmulf  13278  ixxf  13361  ixxssxr  13363  iooval2  13384  ioof  13451  unirnioo  13453  dfioo2  13454  fzval2  13514  fzf  13515  0nelfz1  13547  fz10  13549  fzpreddisj  13577  4fvwrd4  13648  fzof  13656  fzo0  13683  fldiv4p1lem1div2  13827  fldiv4lem1div2  13829  om2uzoi  13947  faclbnd4lem1  14279  hashkf  14318  hashgval  14319  hashinf  14321  hashresfn  14326  hashnn0n0nn  14377  hashge3el3dif  14474  rev0  14741  s2dm  14868  f1oun2prg  14895  trclublem  14969  sqrt2gt1lt2  15248  limsupgord  15443  fclim  15524  fsumrelem  15780  ackbijnn  15801  incexclem  15809  incexc  15810  arisum2  15834  georeclim  15845  geoisumr  15851  0.999...  15854  risefall0lem  15997  ege2le3  16061  sin0  16120  ef01bndlem  16155  cos2bnd  16159  cos01gt0  16162  sincos2sgn  16165  sin4lt0  16166  rpnnen2lem3  16187  rpnnen2lem9  16193  rexpen  16199  cnso  16218  dvdslelem  16280  divalglem1  16365  divalglem5  16368  divalglem6  16369  divalglem10  16373  flodddiv4  16384  0bits  16408  sadcf  16422  sadcadd  16427  bitsshft  16444  smupf  16447  gcdf  16481  eucalgf  16548  2prm  16657  dfphi2  16737  pockthi  16870  prmrec  16885  vdwapf  16935  vdwlem6  16949  karatsuba  17047  1259lem5  17098  2503lem3  17102  4001lem4  17107  structcnvcnv  17116  structfn  17119  strleun  17120  imasvscafn  17513  xpsff1o  17543  wunnat  17940  wunnatOLD  17941  dfinito3  17988  dftermo3  17989  eldmcoa  18048  coapm  18054  catcfuccl  18102  catcfucclOLD  18103  catcxpccl  18192  catcxpcclOLD  18193  yonedainv  18267  smndex1bas  18852  smndex1n0mnd  18858  grpinvfvi  18933  mulgfvi  19023  symgsssg  19416  symgfisg  19417  psgnunilem5  19443  sylow3lem2  19577  oppglsm  19591  efgmf  19662  efgval  19666  efgsf  19678  0frgp  19728  dmdprd  19949  dprdval  19954  invrfval  20322  drngui  20624  rmodislmod  20807  rmodislmodOLD  20808  lssintcl  20842  cnfldadd  21279  cnfldmul  21281  cnfldfunALT  21288  dfcnfldOLD  21289  cnfldfunALTOLD  21301  cnfldfunALTOLDOLD  21302  cnfld0  21314  cnfld1  21315  cnfld1OLD  21316  cnfldsub  21319  xrsds  21336  pzriprnglem4  21404  pzriprnglem9  21409  pzriprnglem14  21414  psgnghm  21506  zrhpsgnmhm  21510  ocv1  21605  dsmmbas2  21665  mplsubrglem  21940  opsrtoslem2  21994  mdetralt  22504  maducoeval2  22536  eltpsi  22841  unitg  22864  fctop  22901  cctop  22903  ppttop  22904  epttop  22906  leordtvallem1  23108  leordtvallem2  23109  iccordt  23112  iscnp2  23137  discmp  23296  conncompcld  23332  1stcrestlem  23350  2ndcdisj  23354  topnlly  23389  disllycmp  23396  dis1stc  23397  txuni2  23463  xkotf  23483  dfac14lem  23515  prdstps  23527  txindis  23532  tx1stc  23548  xkohaus  23551  xkoptsub  23552  cnmpt1st  23566  cnmpt2nd  23567  ptcmpfi  23711  trfil1  23784  fin1aufil  23830  tgpconncompeqg  24010  tgpconncomp  24011  trust  24128  met1stc  24424  dscmet  24475  retopon  24674  cnfldtopon  24693  xrsxmet  24719  xrsmopn  24722  iimulcn  24855  iimulcnOLD  24856  icopnfhmeo  24862  iccpnfhmeo  24864  xrhmeo  24865  cnheiborlem  24874  lebnumii  24886  ishtpy  24892  htpycc  24900  pco1  24936  pcohtpylem  24940  pcopt  24943  pcopt2  24944  pcoass  24945  pcorevlem  24947  rrxcph  25314  rrx0el  25320  ovoliunlem3  25427  ovolicc1  25439  ovolicc2  25445  volf  25452  ioorf  25496  dyadf  25514  dyadmbl  25523  vitalilem5  25535  vitali  25536  mbfimaopnlem  25578  mbflimsup  25589  0plef  25595  i1fima  25601  i1fima2  25602  i1fd  25604  itg1ge0  25609  itg10  25611  i1f1lem  25612  i1fadd  25618  i1fmul  25619  i1fmulc  25627  mbfi1fseqlem5  25643  itg2addlem  25682  reldv  25793  dvbsss  25825  dvef  25906  lhop1lem  25940  deg1fvi  26015  plypf1  26140  coeeulem  26152  coeeu  26153  vieta1lem2  26240  aannenlem3  26259  aalioulem3  26263  dvradcnv  26351  pserulm  26352  pserdvlem2  26359  sinhalfpilem  26392  sincos4thpi  26442  tan4thpi  26443  sincos6thpi  26444  pige3ALT  26448  resinf1o  26464  tanord1  26465  tanregt0  26467  efabl  26478  relogrn  26489  dfrelog  26493  logi  26515  logneg  26516  logltb  26528  logcn  26575  logf1o2  26578  dvlog  26579  efopnlem2  26585  efopn  26586  logccv  26591  dvsqrt  26670  dvcnsqrt  26672  cxpcn3  26677  logblog  26718  angpined  26756  1cubr  26768  asinsin  26818  asin1  26820  reasinsin  26822  atan0  26834  atanbnd  26852  atan1  26854  log2cnv  26870  log2ub  26875  log2le1  26876  birthday  26880  amgmlem  26916  emcllem5  26926  emgt0  26933  harmonicbnd3  26934  ftalem3  27001  basellem4  27010  sgmf  27071  ppi1  27090  cht1  27091  vma1  27092  ppiltx  27103  sqff1o  27108  ppiublem1  27129  ppiublem2  27130  ppiub  27131  chtub  27139  dchreq  27185  bposlem7  27217  bposlem8  27218  bposlem9  27219  lgsdir2lem2  27253  lgsdir2lem3  27254  chebbnd1  27399  chto1ub  27403  chpo1ubb  27408  pntibndlem1  27516  nosgnn0  27585  sltsolem1  27602  bdayfo  27604  nolt02o  27622  nogt01o  27623  noetasuplem4  27663  noetainflem4  27667  scutbdaybnd2lim  27744  madeun  27804  scutfo  27824  addsproplem2  27881  addsproplem7  27886  addsprop  27887  negsprop  27941  mulsproplem13  28022  mulsproplem14  28023  mulsprop  28024  n0scut  28197  0reno  28219  tgldimor  28300  tglnfn  28345  axlowdimlem4  28750  axlowdimlem16  28762  axlowdim  28766  upgrfi  28898  lfgrnloop  28932  lfuhgr1v0e  29061  usgrexmplef  29066  usgrres  29115  vdegp1bi  29345  vtxdginducedm1lem2  29348  pthdlem2  29576  wpthswwlks2on  29766  0ewlk  29918  0pth  29929  konigsbergiedgw  30052  konigsberglem1  30056  konigsberglem2  30057  konigsberglem3  30058  konigsberglem4  30059  konigsberglem5  30060  ex-dif  30227  ex-un  30228  ex-in  30229  ex-fl  30251  avril1  30267  9p10ne21fool  30275  n0lplig  30287  cnidOLD  30386  cnnvm  30486  ipasslem8  30641  ipasslem10  30643  hvsubf  30819  normlem1  30914  normlem6  30919  normlem7  30920  norm-ii-i  30941  norm3adifii  30952  hilid  30965  hlimf  31041  hhssabloi  31066  hhssnv  31068  hhshsslem1  31071  shincli  31166  shsval2i  31191  shs0i  31253  chj0i  31259  chm1i  31260  chincli  31264  chdmm1i  31281  shjshsi  31296  chsup0  31352  h1de2bi  31358  spansnpji  31382  cmcmlem  31395  cmcmii  31401  cmcm2ii  31402  cmcm3ii  31403  pjidmi  31477  pjssmii  31485  pj0i  31497  pjocini  31502  mayetes3i  31533  df0op2  31556  hoaddcomi  31576  hoaddassi  31580  hocadddiri  31583  hocsubdiri  31584  hoaddridi  31590  ho0coi  31592  hoid1i  31593  hoid1ri  31594  hodseqi  31598  honegsubi  31600  adj1o  31698  hoddii  31793  lnopunilem1  31814  lnopunilem2  31815  nmcopexi  31831  nmcopex  31833  nmcoplb  31834  nmcfnexi  31855  nmcfnex  31857  nmcfnlb  31858  adjbd1o  31889  adjcoi  31904  nmopcoadji  31905  opsqrlem6  31949  pjsdii  31959  pjddii  31960  pjidmcoi  31981  pjtoi  31983  pjin1i  31996  pjclem1  31999  stji1i  32046  reuxfrdf  32283  inindif  32306  iuninc  32345  fnresin  32405  rinvf1o  32409  suppss2f  32418  xppreima  32426  ofoprabco  32444  fressupp  32463  supppreima  32466  fsupprnfi  32467  gtiso  32475  df1stres  32478  df2ndres  32479  snct  32490  padct  32496  fsuppcurry1  32502  fsuppcurry2  32503  ffsrn  32506  fpwrelmapffs  32511  fzodif1  32556  nnindf  32577  nn0min  32578  dp2lt  32603  dp2ltsuc  32604  dp2ltc  32605  dplti  32623  dpmul  32631  dpmul4  32632  ressplusf  32679  xrsclat  32733  xrge0base  32736  xrge00  32737  xrnarchi  32887  zringfrac  32991  1fldgenq  33004  xrge0slmod  33055  ply1degltdimlem  33311  ccfldsrarelvec  33350  ccfldextdgrr  33351  locfinreflem  33436  locfinref  33437  unicls  33499  sqsscirc1  33504  mhmhmeotmd  33523  raddcn  33525  xrge0iifiso  33531  xrge0iifhmeo  33532  lmxrge0  33548  cnzh  33566  rezh  33567  qqh0  33580  qqh1  33581  qqhre  33616  rrhre  33617  esumnul  33662  esum0  33663  esumsnf  33678  esumpfinvallem  33688  esumpfinvalf  33690  esumpcvgval  33692  esumcvgsum  33702  esumsup  33703  esumcvgre  33705  sigaclfu2  33735  dmsigagen  33758  ddemeas  33850  mbfmvolf  33881  br2base  33884  omssubadd  33915  sibfof  33955  sitg0  33961  eulerpartlemt  33986  eulerpartgbij  33987  0rrv  34066  coinfliplem  34093  coinflipprob  34094  coinfliprv  34097  ballotlem2  34103  ballotlem4  34113  ballotlem5  34114  ballotlemi1  34117  ballotlem7  34150  ballotth  34152  signsplypnf  34177  signsply0  34178  signsw0g  34183  signswch  34188  signsvf0  34207  hashreprin  34247  reprfz1  34251  chtvalz  34256  hgt750lemd  34275  hgt750lem  34278  hgt750lem2  34279  bnj1098  34409  bnj1109  34412  bnj1131  34413  bnj1533  34478  bnj151  34503  bnj580  34539  bnj852  34547  bnj864  34548  bnj865  34549  bnj978  34575  bnj1021  34592  bnj907  34593  bnj1093  34606  bnj1145  34619  bnj1172  34627  bnj1174  34629  bnj1176  34631  bnj1186  34633  fineqvac  34712  subfacf  34780  subfacp1lem1  34784  subfacp1lem5  34789  subfacp1lem6  34790  subfacval3  34794  erdszelem2  34797  kur14lem4  34814  ioosconn  34852  iccllysconn  34855  satfn  34960  fmlaomn0  34995  gonan0  34997  goaln0  34998  elnanelprv  35034  msrfo  35151  mthmpps  35187  problem5  35268  quad3  35269  circum  35273  axextprim  35290  axrepprim  35291  axunprim  35292  axinfprim  35295  axacprim  35296  bcneg1  35325  setinds  35369  dfon2lem2  35375  dfon2lem4  35377  axextdfeq  35388  fobigcup  35491  snelsingles  35513  fullfunfnv  35537  fullfunfv  35538  rankaltopb  35570  rank0  35761  rankeq1o  35762  hfuni  35775  fneer  35832  neibastop1  35838  nabi1i  35873  nabi2i  35874  limsucncmpi  35924  knoppcnlem8  35970  knoppcnlem11  35973  cnndvlem1  36007  bj-consensusALT  36050  bj-sbidmOLD  36322  bj-n0i  36425  bj-snsetex  36437  bj-tagss  36454  bj-2upln0  36497  bj-2upln1upl  36498  bj-nuliota  36531  bj-0int  36575  bj-elid5  36643  bj-inftyexpitaufo  36676  bj-pinftyccb  36695  bj-minftyccb  36699  bj-pinftynminfty  36701  bj-isrvec  36768  iccioo01  36801  f1omptsnlem  36810  mptsnunlem  36812  topdifinffinlem  36821  relowlpssretop  36838  1oequni2o  36842  pibt2  36891  imadifss  37063  tan2h  37080  poimirlem3  37091  poimirlem9  37097  poimirlem16  37104  poimirlem17  37105  poimirlem18  37106  poimirlem19  37107  poimirlem20  37108  poimirlem22  37110  poimirlem30  37118  mblfinlem1  37125  mblfinlem2  37126  ovoliunnfl  37130  voliunnfl  37132  itg2addnclem  37139  itg2addnclem2  37140  asindmre  37171  areacirclem1  37176  fdc  37213  cntotbnd  37264  heiborlem6  37284  rrnval  37295  reheibor  37307  rngosn3  37392  brcnvrabga  37809  cnvresrn  37815  moantr  37831  inxp2  37834  dfxrn2  37843  cnvcosseq  37904  refrelcosslem  37929  1cosscnvxrn  37942  redundss3  38095  refrelsredund3  38101  refrelredund3  38104  eqvrel0  38253  eqvrelid  38256  prter2  38348  renegclALT  38430  mapdunirnN  41118  lcmeprodgcdi  41473  3factsumint2  41488  3factsumint3  41489  3factsumint4  41490  3factsumint  41491  lcmineqlem4  41498  3lexlogpow5ineq1  41520  3lexlogpow2ineq1  41524  dvrelogpow2b  41534  aks4d1p1p4  41537  aks4d1p8  41553  ressmulgnnd  41564  aks6d1c1  41582  aks6d1c2p2  41585  aks6d1c4  41590  2ap1caineq  41612  sticksstones1  41613  sticksstones2  41614  metakunt6  41653  metakunt24  41671  sqdeccom12  41854  resubf  41927  sn-0ne2  41952  sn-subf  41974  sn-nnne0  41994  sn-0lt1  42008  reneg1lt0  42010  rntrclfvOAI  42102  diophrw  42170  rabren3dioph  42226  pellexlem6  42245  pellex  42246  frmx  42325  frmy  42326  jm2.23  42408  jm2.27dlem3  42423  axac10  42445  pw2f1ocnv  42449  kelac2lem  42479  lmhmlnmsplit  42502  pwfi2f1o  42511  frlmpwfi  42513  insucid  42824  nla0003  42846  ifpbiidcor  42895  sucomisnotcard  42965  alephiso2  42979  alephiso3  42980  cnvnonrel  43009  rnnonrel  43012  resnonrel  43013  cononrel1  43015  cononrel2  43016  fvnonrel  43018  cnvcnvintabd  43021  cnvintabd  43024  rclexi  43036  rtrclex  43038  clcnvlem  43044  cnvrcl0  43046  dmtrcl  43048  rntrcl  43049  dfrtrcl5  43050  iunrelexp0  43123  dmtrclfvRP  43151  rntrclfv  43153  corcltrcl  43160  cotrclrcl  43163  0heALT  43204  frege54cor1a  43285  uneqsn  43446  clsk3nimkb  43461  int-sqdefd  43602  int-sqgeq0d  43607  rr-groth  43727  rr-grothprim  43728  rr-grothshort  43732  seff  43737  expgrowthi  43761  expgrowth  43763  binomcxplemnotnn0  43784  ee233  43949  ax6e2nd  43988  in1  44001  dfvd2ani  44013  dfvd2i  44015  dfvd3i  44022  dfvd3ani  44025  e0bi  44206  uun2221  44243  uun2221p1  44244  uun2221p2  44245  en3lpVD  44275  relopabVD  44331  ax6e2ndVD  44338  ax6e2ndALT  44360  pssnssi  44458  nnf1oxpnn  44559  icof  44583  fnmptif  44633  rn1st  44641  negpilt0  44653  xrgtso  44718  supxrleubrnmptf  44824  xrpnf  44859  rexanuz2nf  44866  ioontr  44887  iccdifioo  44891  iccdifprioo  44892  uzinico2  44938  fsummulc1f  44950  fsumiunss  44954  fnlimfvre2  45056  limsupreuz  45116  limsupvaluz2  45117  limsup10ex  45152  icccncfext  45266  dvcosre  45291  dvsinax  45292  ioodvbdlimc1lem2  45311  ioodvbdlimc2lem  45313  dvmptmulf  45316  dvnmul  45322  dvmptfprodlem  45323  dvnprodlem2  45326  stoweidlem1  45380  stoweidlem26  45405  stoweidlem34  45413  stoweidlem44  45423  stoweid  45442  stirlinglem5  45457  dirkercncflem1  45482  fourierdlem44  45530  fourierdlem56  45541  fourierdlem62  45547  fourierdlem89  45574  fourierdlem91  45576  fourierdlem100  45585  fourierdlem102  45587  fourierdlem103  45588  fourierdlem104  45589  fourierdlem108  45593  fourierdlem112  45597  fourierdlem114  45599  fouriersw  45610  rrndistlt  45669  gsumge0cl  45750  sge0tsms  45759  sge0ltfirpmpt2  45805  ovn0  45945  hoidmv1le  45973  hoidmvle  45979  ovnsubadd2lem  46024  ovolval4lem1  46028  vonioolem2  46060  smflimlem3  46152  nsssmfmbf  46158  axorbtnotaiffb  46276  axorbciffatcxorb  46278  abnotbtaxb  46288  euabsneu  46401  sprval  46810  fmtnoinf  46867  1nevenALTV  47022  nfermltl8rev  47073  nfermltl2rev  47074  nnsum3primes4  47119  tgblthelfgott  47146  tgoldbachlt  47147  ldepslinc  47568  ackval42  47760  rrx2plordso  47788  vsn  47873  sepfsepc  47937  alimp-no-surprise  48205  aacllem  48225  amgmwlem  48226  amgmlemALT  48227