Theorem mpbi 230

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 216	. 2 ⊢ (𝜑 → 𝜓)
4	1, 3	ax-mp 5	1 ⊢ 𝜓

Syntax hints:   ↔ wb 206

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 207

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  820  biadanii  822  imori  855  ori  862  pm5.16  1016  dn1  1058  3ori  1426  cadan  1609  nic-dfim  1669  nic-dfneg  1670  nic-mp  1671  nic-mpALT  1672  tbw-negdf  1699  rb-imdf  1750  nfri  1789  mpgbi  1798  19.35i  1878  nfim1  2199  19.36i  2231  ax6  2389  sbie  2507  datisi  2680  disamis  2681  dimatis  2688  fresison  2689  bamalip  2692  axi12  2706  eqcomi  2746  eqtri  2765  eleqtri  2839  nfnfc  2918  neii  2942  necomi  2995  neeqtri  3013  neli  3048  nrex  3074  rexlimivOLD  3185  rexlimi  3259  nfra2wOLD  3300  eueqi  3715  euxfr2w  3726  euxfr2  3728  reuxfrd  3754  cdeqri  3772  sseqtri  4032  pssn2lp  4104  equncomi  4160  unssi  4191  ssini  4240  unabs  4265  inabs  4266  dfin4  4278  vn0  4345  inindif  4375  difidALT  4377  ab0orv  4383  ab0orvALT  4384  disjdif  4472  difin0  4474  pwundif  4624  snid  4662  rabrsn  4724  iinrab2  5070  symdifv  5086  rintn0  5109  breqtri  5168  axsepgfromrep  5294  bm1.3iiOLD  5302  ax6vsep  5303  notzfaus  5363  zfpow  5366  dtruALT2  5370  dtruALT  5388  reusv2lem4  5401  dtru  5441  el  5442  dtruOLD  5446  op1stb  5476  copsexgw  5495  copsexg  5496  uniop  5520  rn0  5936  dmresi  6070  somincom  6154  cnvimassrndm  6172  cnvcnv  6212  elid  6219  rescnvcnv  6224  cnvcnvres  6225  cocnvcnv2  6278  cores2  6279  co01  6281  cnviin  6306  predres  6360  iota4an  6543  fnopab  6706  mpt0  6710  fnmpti  6711  f1cnvcnv  6813  f1ovi  6887  eliman0  6946  fvco4i  7010  cnvimainrn  7087  fmpti  7132  funiunfv  7268  oprabss  7541  relmptopab  7683  zfun  7756  tfinds2  7885  omon  7899  2nd0  8021  f1stres  8038  f2ndres  8039  cnvoprab  8085  relmpoopab  8119  df1st2  8123  df2nd2  8124  fsplit  8142  frpoins3xpg  8165  frpoins3xp3g  8166  poxp2  8168  poseq  8183  reldmtpos  8259  dftpos4  8270  tpostpos  8271  tpos0  8281  frrlem4  8314  wfrlem4OLD  8352  smo0  8398  tfrlem14  8431  tfrlem16  8433  rdgsucg  8463  rdglimg  8465  frfnom  8475  oawordeulem  8592  uniixp  8961  dfdom2  9018  ssdomg  9040  xpcomf1o  9101  sbthlem5  9127  sdom0  9148  limensuci  9193  1sdom2  9276  fiint  9366  fiintOLD  9367  fidomdm  9374  residfi  9378  mptfi  9391  fisn  9467  dffi3  9471  ordtypelem6  9563  ordtypelem7  9564  wemaplem2  9587  harwdom  9631  suc11reg  9659  zfinf  9679  axinf2  9680  noinfep  9700  cantnfvalf  9705  cantnflt  9712  cantnf0  9715  cantnf  9733  ttrclco  9758  tz9.1c  9770  tc2  9782  r111  9815  r1tr2  9817  r1ordg  9818  r1sssuc  9823  r1val1  9826  tz9.13  9831  r1elssi  9845  pwwf  9847  rankopb  9892  rankeq0b  9900  ranksuc  9905  rankmapu  9918  rankxplim3  9921  rankxpsuc  9922  cp  9931  karden  9935  card0  9998  cardlim  10012  cardom  10026  infxpenlem  10053  alephsuc2  10120  alephgeom  10122  unialeph  10141  dfac4  10162  dfacacn  10182  dju1dif  10213  dju1p1e2  10214  infdju1  10230  ackbij1lem13  10271  ackbij2  10282  cf0  10291  cfsuc  10297  cfom  10304  cfslb2n  10308  ominf4  10352  fin23lem17  10378  fin23lem28  10380  fin23lem30  10382  fin23lem31  10383  fin23lem40  10391  isfin1-3  10426  dfacfin7  10439  fin1a2lem6  10445  itunitc1  10460  axcc3  10478  dcomex  10487  axdc2lem  10488  axcclem  10497  zfac  10500  ac3  10502  ackm  10505  axac2  10506  axac  10507  axaci  10508  cardeqv  10509  numth2  10511  numth  10512  dmct  10564  brdom3  10568  fin71ac  10573  cardf  10590  aleph1  10611  cfpwsdom  10624  smobeth  10626  zfcndrep  10654  zfcndpow  10656  zfcndac  10659  gch2  10715  wunex3  10781  tskpr  10810  inar1  10815  rankcf  10817  tskcard  10821  tskuni  10823  grothpw  10866  axgroth4  10872  grothprim  10874  inaprc  10876  dmaddpi  10930  dmmulpi  10931  1lt2pi  10945  addpqf  10984  mulpqf  10986  1lt2nq  11013  supsrlem  11151  ssxr  11330  gtso  11342  subf  11510  negne0i  11584  mulnzcnf  11909  infrenegsup  12251  nnne0  12300  halflt1  12484  nn0ssz  12636  3halfnz  12697  zeo  12704  numlt  12758  numltc  12759  le9lt10  12760  decle  12767  uzf  12881  xaddf  13266  xsubge0  13303  xmulf  13314  ixxf  13397  ixxssxr  13399  iooval2  13420  ioof  13487  unirnioo  13489  dfioo2  13490  fzval2  13550  fzf  13551  0nelfz1  13583  fz10  13585  fzpreddisj  13613  4fvwrd4  13688  fzof  13696  fzo0  13723  fldiv4p1lem1div2  13875  fldiv4lem1div2  13877  om2uzoi  13996  faclbnd4lem1  14332  hashkf  14371  hashgval  14372  hashinf  14374  hashresfn  14379  hashnn0n0nn  14430  hashge3el3dif  14526  hash3tpde  14532  rev0  14802  s2dm  14929  f1oun2prg  14956  trclublem  15034  sqrt2gt1lt2  15313  limsupgord  15508  fclim  15589  fsumrelem  15843  ackbijnn  15864  incexclem  15872  incexc  15873  arisum2  15897  georeclim  15908  geoisumr  15914  0.999...  15917  risefall0lem  16062  ege2le3  16126  sin0  16185  ef01bndlem  16220  cos2bnd  16224  cos01gt0  16227  sincos2sgn  16230  sin4lt0  16231  rpnnen2lem3  16252  rpnnen2lem9  16258  rexpen  16264  cnso  16283  dvdslelem  16346  divalglem1  16431  divalglem5  16434  divalglem6  16435  divalglem10  16439  flodddiv4  16452  0bits  16476  sadcf  16490  sadcadd  16495  bitsshft  16512  smupf  16515  gcdf  16549  eucalgf  16620  2prm  16729  dfphi2  16811  pockthi  16945  prmrec  16960  vdwapf  17010  vdwlem6  17024  karatsuba  17121  1259lem5  17172  2503lem3  17176  4001lem4  17181  structcnvcnv  17190  structfn  17193  strleun  17194  imasvscafn  17582  xpsff1o  17612  wunnat  18004  dfinito3  18050  dftermo3  18051  eldmcoa  18110  coapm  18116  catcfuccl  18163  catcxpccl  18252  yonedainv  18326  smndex1bas  18919  smndex1n0mnd  18925  grpinvfvi  19000  mulgfvi  19091  ressmulgnnd  19096  symgsssg  19485  symgfisg  19486  psgnunilem5  19512  sylow3lem2  19646  oppglsm  19660  efgmf  19731  efgval  19735  efgsf  19747  0frgp  19797  dmdprd  20018  dprdval  20023  invrfval  20389  drngui  20735  rmodislmod  20928  lssintcl  20962  cnfldadd  21370  cnfldmul  21372  cnfldfunALT  21379  dfcnfldOLD  21380  cnfldfunALTOLD  21392  cnfldfunALTOLDOLD  21393  cnfld0  21405  cnfld1  21406  cnfld1OLD  21407  cnfldsub  21410  xrsds  21427  pzriprnglem4  21495  pzriprnglem9  21500  pzriprnglem14  21505  psgnghm  21598  zrhpsgnmhm  21602  ocv1  21697  dsmmbas2  21757  mplsubrglem  22024  opsrtoslem2  22080  evl1maprhm  22383  mdetralt  22614  maducoeval2  22646  eltpsi  22951  unitg  22974  fctop  23011  cctop  23013  ppttop  23014  epttop  23016  leordtvallem1  23218  leordtvallem2  23219  iccordt  23222  iscnp2  23247  discmp  23406  conncompcld  23442  1stcrestlem  23460  2ndcdisj  23464  topnlly  23499  disllycmp  23506  dis1stc  23507  txuni2  23573  xkotf  23593  dfac14lem  23625  prdstps  23637  txindis  23642  tx1stc  23658  xkohaus  23661  xkoptsub  23662  cnmpt1st  23676  cnmpt2nd  23677  ptcmpfi  23821  trfil1  23894  fin1aufil  23940  tgpconncompeqg  24120  tgpconncomp  24121  trust  24238  met1stc  24534  dscmet  24585  retopon  24784  cnfldtopon  24803  xrsxmet  24831  xrsmopn  24834  iimulcn  24967  iimulcnOLD  24968  icopnfhmeo  24974  iccpnfhmeo  24976  xrhmeo  24977  cnheiborlem  24986  lebnumii  24998  ishtpy  25004  htpycc  25012  pco1  25048  pcohtpylem  25052  pcopt  25055  pcopt2  25056  pcoass  25057  pcorevlem  25059  rrxcph  25426  rrx0el  25432  ovoliunlem3  25539  ovolicc1  25551  ovolicc2  25557  volf  25564  ioorf  25608  dyadf  25626  dyadmbl  25635  vitalilem5  25647  vitali  25648  mbfimaopnlem  25690  mbflimsup  25701  0plef  25707  i1fima  25713  i1fima2  25714  i1fd  25716  itg1ge0  25721  itg10  25723  i1f1lem  25724  i1fadd  25730  i1fmul  25731  i1fmulc  25738  mbfi1fseqlem5  25754  itg2addlem  25793  reldv  25905  dvbsss  25937  dvef  26018  lhop1lem  26052  deg1fvi  26124  plypf1  26251  coeeulem  26263  coeeu  26264  vieta1lem2  26353  aannenlem3  26372  aalioulem3  26376  dvradcnv  26464  pserulm  26465  pserdvlem2  26472  sinhalfpilem  26505  sincos4thpi  26555  tan4thpiOLD  26557  sincos6thpi  26558  pige3ALT  26562  resinf1o  26578  tanord1  26579  tanregt0  26581  efabl  26592  relogrn  26603  dfrelog  26607  logi  26629  logneg  26630  logltb  26642  logcn  26689  logf1o2  26692  dvlog  26693  efopnlem2  26699  efopn  26700  logccv  26705  dvsqrt  26784  dvcnsqrt  26786  cxpcn3  26791  logblog  26835  angpined  26873  1cubr  26885  asinsin  26935  asin1  26937  reasinsin  26939  atan0  26951  atanbnd  26969  atan1  26971  log2cnv  26987  log2ub  26992  log2le1  26993  birthday  26997  amgmlem  27033  emcllem5  27043  emgt0  27050  harmonicbnd3  27051  ftalem3  27118  basellem4  27127  sgmf  27188  ppi1  27207  cht1  27208  vma1  27209  ppiltx  27220  sqff1o  27225  ppiublem1  27246  ppiublem2  27247  ppiub  27248  chtub  27256  dchreq  27302  bposlem7  27334  bposlem8  27335  bposlem9  27336  lgsdir2lem2  27370  lgsdir2lem3  27371  chebbnd1  27516  chto1ub  27520  chpo1ubb  27525  pntibndlem1  27633  nosgnn0  27703  sltsolem1  27720  bdayfo  27722  nolt02o  27740  nogt01o  27741  noetasuplem4  27781  noetainflem4  27785  scutbdaybnd2lim  27862  madeun  27922  scutfo  27942  addsproplem2  28003  addsproplem7  28008  addsprop  28009  negsprop  28067  subsf  28094  mulsproplem13  28154  mulsproplem14  28155  mulsprop  28156  n0scut  28338  nohalf  28407  pw2bday  28418  0reno  28429  tgldimor  28510  tglnfn  28555  axlowdimlem4  28960  axlowdimlem16  28972  axlowdim  28976  upgrfi  29108  lfgrnloop  29142  lfuhgr1v0e  29271  usgrexmplef  29276  usgrres  29325  vdegp1bi  29555  vtxdginducedm1lem2  29558  dfpth2  29749  pthdlem2  29788  wpthswwlks2on  29981  0ewlk  30133  0pth  30144  konigsbergiedgw  30267  konigsberglem1  30271  konigsberglem2  30272  konigsberglem3  30273  konigsberglem4  30274  konigsberglem5  30275  ex-dif  30442  ex-un  30443  ex-in  30444  ex-fl  30466  avril1  30482  9p10ne21fool  30490  n0lplig  30502  cnidOLD  30601  cnnvm  30701  ipasslem8  30856  ipasslem10  30858  hvsubf  31034  normlem1  31129  normlem6  31134  normlem7  31135  norm-ii-i  31156  norm3adifii  31167  hilid  31180  hlimf  31256  hhssabloi  31281  hhssnv  31283  hhshsslem1  31286  shincli  31381  shsval2i  31406  shs0i  31468  chj0i  31474  chm1i  31475  chincli  31479  chdmm1i  31496  shjshsi  31511  chsup0  31567  h1de2bi  31573  spansnpji  31597  cmcmlem  31610  cmcmii  31616  cmcm2ii  31617  cmcm3ii  31618  pjidmi  31692  pjssmii  31700  pj0i  31712  pjocini  31717  mayetes3i  31748  df0op2  31771  hoaddcomi  31791  hoaddassi  31795  hocadddiri  31798  hocsubdiri  31799  hoaddridi  31805  ho0coi  31807  hoid1i  31808  hoid1ri  31809  hodseqi  31813  honegsubi  31815  adj1o  31913  hoddii  32008  lnopunilem1  32029  lnopunilem2  32030  nmcopexi  32046  nmcopex  32048  nmcoplb  32049  nmcfnexi  32070  nmcfnex  32072  nmcfnlb  32073  adjbd1o  32104  adjcoi  32119  nmopcoadji  32120  opsqrlem6  32164  pjsdii  32174  pjddii  32175  pjidmcoi  32196  pjtoi  32198  pjin1i  32211  pjclem1  32214  stji1i  32261  reuxfrdf  32510  iuninc  32573  fnresin  32636  rinvf1o  32640  suppss2f  32648  xppreima  32655  ofoprabco  32674  fressupp  32697  supppreima  32700  fsupprnfi  32701  gtiso  32710  df1stres  32713  df2ndres  32714  snct  32725  padct  32731  fsuppcurry1  32736  fsuppcurry2  32737  ffsrn  32740  fpwrelmapffs  32745  fzodif1  32794  nnindf  32821  nn0min  32822  dp2lt  32867  dp2ltsuc  32868  dp2ltc  32869  dplti  32887  dpmul  32895  dpmul4  32896  ressplusf  32948  chnub  33002  xrsclat  33013  xrge0base  33016  xrge00  33017  xrnarchi  33191  elrgspnlem2  33247  1fldgenq  33324  xrge0slmod  33376  zringfrac  33582  ply1degltdimlem  33673  ccfldsrarelvec  33721  ccfldextdgrr  33722  locfinreflem  33839  locfinref  33840  unicls  33902  sqsscirc1  33907  mhmhmeotmd  33926  raddcn  33928  xrge0iifiso  33934  xrge0iifhmeo  33935  lmxrge0  33951  cnzh  33969  rezh  33970  qqh0  33985  qqh1  33986  qqhre  34021  rrhre  34022  esumnul  34049  esum0  34050  esumsnf  34065  esumpfinvallem  34075  esumpfinvalf  34077  esumpcvgval  34079  esumcvgsum  34089  esumsup  34090  esumcvgre  34092  sigaclfu2  34122  dmsigagen  34145  ddemeas  34237  mbfmvolf  34268  br2base  34271  omssubadd  34302  sibfof  34342  sitg0  34348  eulerpartlemt  34373  eulerpartgbij  34374  0rrv  34453  coinfliplem  34481  coinflipprob  34482  coinfliprv  34485  ballotlem2  34491  ballotlem4  34501  ballotlem5  34502  ballotlemi1  34505  ballotlem7  34538  ballotth  34540  signsplypnf  34565  signsply0  34566  signsw0g  34571  signswch  34576  signsvf0  34595  hashreprin  34635  reprfz1  34639  chtvalz  34644  hgt750lemd  34663  hgt750lem  34666  hgt750lem2  34667  bnj1098  34797  bnj1109  34800  bnj1131  34801  bnj1533  34866  bnj151  34891  bnj580  34927  bnj852  34935  bnj864  34936  bnj865  34937  bnj978  34963  bnj1021  34980  bnj907  34981  bnj1093  34994  bnj1145  35007  bnj1172  35015  bnj1174  35017  bnj1176  35019  bnj1186  35021  nfan1c  35087  fineqvac  35111  subfacf  35180  subfacp1lem1  35184  subfacp1lem5  35189  subfacp1lem6  35190  subfacval3  35194  erdszelem2  35197  kur14lem4  35214  ioosconn  35252  iccllysconn  35255  satfn  35360  fmlaomn0  35395  gonan0  35397  goaln0  35398  elnanelprv  35434  msrfo  35551  mthmpps  35587  problem5  35674  quad3  35675  circum  35679  axextprim  35701  axrepprim  35702  axunprim  35703  axinfprim  35706  axacprim  35707  bcneg1  35736  setinds  35779  dfon2lem2  35785  dfon2lem4  35787  axextdfeq  35798  fobigcup  35901  snelsingles  35923  fullfunfnv  35947  fullfunfv  35948  rankaltopb  35980  rank0  36171  rankeq1o  36172  hfuni  36185  in-ax8  36225  fneer  36354  neibastop1  36360  nabi1i  36395  nabi2i  36396  limsucncmpi  36446  knoppcnlem8  36501  knoppcnlem11  36504  cnndvlem1  36538  bj-consensusALT  36580  bj-sbidmOLD  36851  bj-n0i  36952  bj-snsetex  36964  bj-tagss  36981  bj-2upln0  37024  bj-2upln1upl  37025  bj-nuliota  37058  bj-0int  37102  bj-elid5  37170  bj-inftyexpitaufo  37203  bj-pinftyccb  37222  bj-minftyccb  37226  bj-pinftynminfty  37228  bj-isrvec  37295  iccioo01  37328  f1omptsnlem  37337  mptsnunlem  37339  topdifinffinlem  37348  relowlpssretop  37365  1oequni2o  37369  pibt2  37418  imadifss  37602  tan2h  37619  poimirlem3  37630  poimirlem9  37636  poimirlem16  37643  poimirlem17  37644  poimirlem18  37645  poimirlem19  37646  poimirlem20  37647  poimirlem22  37649  poimirlem30  37657  mblfinlem1  37664  mblfinlem2  37665  ovoliunnfl  37669  voliunnfl  37671  itg2addnclem  37678  itg2addnclem2  37679  asindmre  37710  areacirclem1  37715  fdc  37752  cntotbnd  37803  heiborlem6  37823  rrnval  37834  reheibor  37846  rngosn3  37931  brcnvrabga  38343  cnvresrn  38349  moantr  38365  inxp2  38368  dfxrn2  38377  cnvcosseq  38438  refrelcosslem  38463  1cosscnvxrn  38476  redundss3  38629  refrelsredund3  38635  refrelredund3  38638  eqvrel0  38787  eqvrelid  38790  prter2  38882  renegclALT  38964  mapdunirnN  41652  lcmeprodgcdi  42008  3factsumint2  42023  3factsumint3  42024  3factsumint4  42025  3factsumint  42026  lcmineqlem4  42033  3lexlogpow5ineq1  42055  3lexlogpow2ineq1  42059  dvrelogpow2b  42069  aks4d1p1p4  42072  aks4d1p8  42088  aks6d1c1  42117  aks6d1c2p2  42120  aks6d1c4  42125  2ap1caineq  42146  sticksstones1  42147  sticksstones2  42148  aks6d1c7lem2  42182  aks5lem3a  42190  aks5lem6  42193  unitscyglem2  42197  unitscyglem3  42198  metakunt6  42211  metakunt24  42229  sqdeccom12  42324  readvrec2  42391  readvcot  42394  resubf  42411  sn-0ne2  42436  sn-subf  42458  sn-nnne0  42478  sn-0lt1  42493  reneg1lt0  42496  rntrclfvOAI  42702  diophrw  42770  rabren3dioph  42826  pellexlem6  42845  pellex  42846  frmx  42925  frmy  42926  jm2.23  43008  jm2.27dlem3  43023  axac10  43045  pw2f1ocnv  43049  kelac2lem  43076  lmhmlnmsplit  43099  pwfi2f1o  43108  frlmpwfi  43110  insucid  43416  nla0003  43438  ifpbiidcor  43487  sucomisnotcard  43557  alephiso2  43571  alephiso3  43572  cnvnonrel  43601  rnnonrel  43604  resnonrel  43605  cononrel1  43607  cononrel2  43608  fvnonrel  43610  cnvcnvintabd  43613  cnvintabd  43616  rclexi  43628  rtrclex  43630  clcnvlem  43636  cnvrcl0  43638  dmtrcl  43640  rntrcl  43641  dfrtrcl5  43642  iunrelexp0  43715  dmtrclfvRP  43743  rntrclfv  43745  corcltrcl  43752  cotrclrcl  43755  0heALT  43796  frege54cor1a  43877  uneqsn  44038  clsk3nimkb  44053  int-sqdefd  44194  int-sqgeq0d  44199  rr-groth  44318  rr-grothprim  44319  rr-grothshort  44323  seff  44328  expgrowthi  44352  expgrowth  44354  binomcxplemnotnn0  44375  ee233  44539  ax6e2nd  44578  in1  44591  dfvd2ani  44603  dfvd2i  44605  dfvd3i  44612  dfvd3ani  44615  e0bi  44796  uun2221  44833  uun2221p1  44834  uun2221p2  44835  en3lpVD  44865  relopabVD  44921  ax6e2ndVD  44928  ax6e2ndALT  44950  pssnssi  45106  nnf1oxpnn  45200  icof  45224  fnmptif  45272  rn1st  45280  negpilt0  45292  xrgtso  45356  supxrleubrnmptf  45462  xrpnf  45496  rexanuz2nf  45503  ioontr  45524  iccdifioo  45528  iccdifprioo  45529  uzinico2  45575  fsummulc1f  45586  fsumiunss  45590  fnlimfvre2  45692  limsupreuz  45752  limsup10ex  45788  icccncfext  45902  dvcosre  45927  dvsinax  45928  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  dvmptmulf  45952  dvnmul  45958  dvmptfprodlem  45959  dvnprodlem2  45962  stoweidlem1  46016  stoweidlem26  46041  stoweidlem34  46049  stoweidlem44  46059  stoweid  46078  stirlinglem5  46093  dirkercncflem1  46118  fourierdlem44  46166  fourierdlem56  46177  fourierdlem62  46183  fourierdlem89  46210  fourierdlem91  46212  fourierdlem100  46221  fourierdlem102  46223  fourierdlem103  46224  fourierdlem104  46225  fourierdlem108  46229  fourierdlem112  46233  fourierdlem114  46235  fouriersw  46246  rrndistlt  46305  gsumge0cl  46386  sge0tsms  46395  sge0ltfirpmpt2  46441  ovn0  46581  hoidmv1le  46609  hoidmvle  46615  ovnsubadd2lem  46660  ovolval4lem1  46664  vonioolem2  46696  smflimlem3  46788  nsssmfmbf  46794  axorbtnotaiffb  46915  axorbciffatcxorb  46917  abnotbtaxb  46927  euabsneu  47040  sprval  47466  fmtnoinf  47523  1nevenALTV  47678  nfermltl8rev  47729  nfermltl2rev  47730  nnsum3primes4  47775  tgblthelfgott  47802  tgoldbachlt  47803  cycl3grtri  47914  isubgr3stgrlem3  47935  usgrexmpl1lem  47980  usgrexmpl2lem  47985  usgrexmpl2trifr  47996  ldepslinc  48426  ackval42  48617  rrx2plordso  48645  vsn  48731  dmtposss  48776  sepfsepc  48825  rescofuf  48922  fuco2eld2  49009  fuco22a  49045  alimp-no-surprise  49300  aacllem  49320  amgmwlem  49321  amgmlemALT  49322