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  819  biadanii  821  imori  854  ori  861  pm5.16  1015  dn1  1057  3ori  1425  cadan  1608  nic-dfim  1668  nic-dfneg  1669  nic-mp  1670  nic-mpALT  1671  tbw-negdf  1698  rb-imdf  1749  nfri  1788  mpgbi  1797  19.35i  1877  nfim1  2198  19.36i  2230  ax6  2387  sbie  2505  datisi  2678  disamis  2679  dimatis  2686  fresison  2687  bamalip  2690  axi12  2704  eqcomi  2743  eqtri  2757  eleqtri  2831  nfnfc  2910  neii  2933  necomi  2985  neeqtri  3003  neli  3037  nrex  3063  rexlimivOLD  3168  rexlimi  3240  eueqi  3690  euxfr2w  3701  euxfr2  3703  reuxfrd  3729  cdeqri  3747  sseqtri  4005  pssn2lp  4077  equncomi  4133  unssi  4164  ssini  4213  unabs  4238  inabs  4239  dfin4  4251  vn0  4318  inindif  4348  difidALT  4350  ab0orv  4356  ab0orvALT  4357  disjdif  4445  difin0  4447  pwundif  4597  snid  4636  rabrsn  4698  iinrab2  5044  symdifv  5060  rintn0  5083  breqtri  5142  axsepgfromrep  5262  bm1.3iiOLD  5270  ax6vsep  5271  notzfaus  5331  zfpow  5334  dtruALT2  5338  dtruALT  5356  reusv2lem4  5369  dtru  5409  el  5410  dtruOLD  5414  op1stb  5444  copsexgw  5463  copsexg  5464  uniop  5488  rn0  5903  dmresi  6037  somincom  6121  cnvimassrndm  6139  cnvcnv  6179  elid  6186  rescnvcnv  6191  cnvcnvres  6192  cocnvcnv2  6245  cores2  6246  co01  6248  cnviin  6273  predres  6326  iota4an  6510  fnopab  6673  mpt0  6677  fnmpti  6678  f1cnvcnv  6780  f1ovi  6854  eliman0  6913  fvco4i  6977  cnvimainrn  7054  fmpti  7099  funiunfv  7237  oprabss  7510  relmptopab  7652  zfun  7725  tfinds2  7854  omon  7868  2nd0  7990  f1stres  8007  f2ndres  8008  cnvoprab  8054  relmpoopab  8088  df1st2  8092  df2nd2  8093  fsplit  8111  frpoins3xpg  8134  frpoins3xp3g  8135  poxp2  8137  poseq  8152  reldmtpos  8228  dftpos4  8239  tpostpos  8240  tpos0  8250  frrlem4  8283  wfrlem4OLD  8321  smo0  8367  tfrlem14  8400  tfrlem16  8402  rdgsucg  8432  rdglimg  8434  frfnom  8444  oawordeulem  8561  uniixp  8930  dfdom2  8987  ssdomg  9009  xpcomf1o  9070  sbthlem5  9096  sdom0  9117  limensuci  9162  1sdom2  9243  fiint  9333  fiintOLD  9334  fidomdm  9341  residfi  9345  mptfi  9358  fisn  9434  dffi3  9438  ordtypelem6  9530  ordtypelem7  9531  wemaplem2  9554  harwdom  9598  suc11reg  9626  zfinf  9646  axinf2  9647  noinfep  9667  cantnfvalf  9672  cantnflt  9679  cantnf0  9682  cantnf  9700  ttrclco  9725  tz9.1c  9737  tc2  9749  r111  9782  r1tr2  9784  r1ordg  9785  r1sssuc  9790  r1val1  9793  tz9.13  9798  r1elssi  9812  pwwf  9814  rankopb  9859  rankeq0b  9867  ranksuc  9872  rankmapu  9885  rankxplim3  9888  rankxpsuc  9889  cp  9898  karden  9902  card0  9965  cardlim  9979  cardom  9993  infxpenlem  10020  alephsuc2  10087  alephgeom  10089  unialeph  10108  dfac4  10129  dfacacn  10149  dju1dif  10180  dju1p1e2  10181  infdju1  10197  ackbij1lem13  10238  ackbij2  10249  cf0  10258  cfsuc  10264  cfom  10271  cfslb2n  10275  ominf4  10319  fin23lem17  10345  fin23lem28  10347  fin23lem30  10349  fin23lem31  10350  fin23lem40  10358  isfin1-3  10393  dfacfin7  10406  fin1a2lem6  10412  itunitc1  10427  axcc3  10445  dcomex  10454  axdc2lem  10455  axcclem  10464  zfac  10467  ac3  10469  ackm  10472  axac2  10473  axac  10474  axaci  10475  cardeqv  10476  numth2  10478  numth  10479  dmct  10531  brdom3  10535  fin71ac  10540  cardf  10557  aleph1  10578  cfpwsdom  10591  smobeth  10593  zfcndrep  10621  zfcndpow  10623  zfcndac  10626  gch2  10682  wunex3  10748  tskpr  10777  inar1  10782  rankcf  10784  tskcard  10788  tskuni  10790  grothpw  10833  axgroth4  10839  grothprim  10841  inaprc  10843  dmaddpi  10897  dmmulpi  10898  1lt2pi  10912  addpqf  10951  mulpqf  10953  1lt2nq  10980  supsrlem  11118  ssxr  11297  gtso  11309  subf  11477  negne0i  11551  mulnzcnf  11876  infrenegsup  12218  nnne0  12267  halflt1  12451  nn0ssz  12604  3halfnz  12665  zeo  12672  numlt  12726  numltc  12727  le9lt10  12728  decle  12735  uzf  12848  xaddf  13233  xsubge0  13270  xmulf  13281  ixxf  13364  ixxssxr  13366  iooval2  13387  ioof  13454  unirnioo  13456  dfioo2  13457  fzval2  13517  fzf  13518  0nelfz1  13550  fz10  13552  fzpreddisj  13580  4fvwrd4  13655  fzof  13663  fzo0  13690  fldiv4p1lem1div2  13842  fldiv4lem1div2  13844  om2uzoi  13963  faclbnd4lem1  14301  hashkf  14340  hashgval  14341  hashinf  14343  hashresfn  14348  hashnn0n0nn  14399  hashge3el3dif  14495  hash3tpde  14501  rev0  14771  s2dm  14898  f1oun2prg  14925  trclublem  15003  sqrt2gt1lt2  15282  limsupgord  15477  fclim  15558  fsumrelem  15812  ackbijnn  15833  incexclem  15841  incexc  15842  arisum2  15866  georeclim  15877  geoisumr  15883  0.999...  15886  risefall0lem  16031  ege2le3  16095  sin0  16154  ef01bndlem  16189  cos2bnd  16193  cos01gt0  16196  sincos2sgn  16199  sin4lt0  16200  rpnnen2lem3  16221  rpnnen2lem9  16227  rexpen  16233  cnso  16252  dvdslelem  16315  divalglem1  16400  divalglem5  16403  divalglem6  16404  divalglem10  16408  flodddiv4  16421  0bits  16445  sadcf  16459  sadcadd  16464  bitsshft  16481  smupf  16484  gcdf  16518  eucalgf  16589  2prm  16698  dfphi2  16780  pockthi  16914  prmrec  16929  vdwapf  16979  vdwlem6  16993  karatsuba  17090  1259lem5  17141  2503lem3  17145  4001lem4  17150  structcnvcnv  17159  structfn  17162  strleun  17163  imasvscafn  17538  xpsff1o  17568  wunnat  17959  dfinito3  18005  dftermo3  18006  eldmcoa  18065  coapm  18071  catcfuccl  18118  catcxpccl  18206  yonedainv  18280  smndex1bas  18871  smndex1n0mnd  18877  grpinvfvi  18952  mulgfvi  19043  ressmulgnnd  19048  symgsssg  19435  symgfisg  19436  psgnunilem5  19462  sylow3lem2  19596  oppglsm  19610  efgmf  19681  efgval  19685  efgsf  19697  0frgp  19747  dmdprd  19968  dprdval  19973  invrfval  20336  drngui  20682  rmodislmod  20874  lssintcl  20908  cnfldadd  21308  cnfldmul  21310  cnfldfunALT  21317  dfcnfldOLD  21318  cnfldfunALTOLD  21330  cnfld0  21342  cnfld1  21343  cnfld1OLD  21344  cnfldsub  21347  xrsds  21364  pzriprnglem4  21432  pzriprnglem9  21437  pzriprnglem14  21442  psgnghm  21527  zrhpsgnmhm  21531  ocv1  21626  dsmmbas2  21684  mplsubrglem  21951  opsrtoslem2  22001  evl1maprhm  22304  mdetralt  22533  maducoeval2  22565  eltpsi  22869  unitg  22892  fctop  22929  cctop  22931  ppttop  22932  epttop  22934  leordtvallem1  23135  leordtvallem2  23136  iccordt  23139  iscnp2  23164  discmp  23323  conncompcld  23359  1stcrestlem  23377  2ndcdisj  23381  topnlly  23416  disllycmp  23423  dis1stc  23424  txuni2  23490  xkotf  23510  dfac14lem  23542  prdstps  23554  txindis  23559  tx1stc  23575  xkohaus  23578  xkoptsub  23579  cnmpt1st  23593  cnmpt2nd  23594  ptcmpfi  23738  trfil1  23811  fin1aufil  23857  tgpconncompeqg  24037  tgpconncomp  24038  trust  24155  met1stc  24447  dscmet  24498  retopon  24689  cnfldtopon  24708  xrsxmet  24736  xrsmopn  24739  iimulcn  24872  iimulcnOLD  24873  icopnfhmeo  24879  iccpnfhmeo  24881  xrhmeo  24882  cnheiborlem  24891  lebnumii  24903  ishtpy  24909  htpycc  24917  pco1  24953  pcohtpylem  24957  pcopt  24960  pcopt2  24961  pcoass  24962  pcorevlem  24964  rrxcph  25331  rrx0el  25337  ovoliunlem3  25444  ovolicc1  25456  ovolicc2  25462  volf  25469  ioorf  25513  dyadf  25531  dyadmbl  25540  vitalilem5  25552  vitali  25553  mbfimaopnlem  25595  mbflimsup  25606  0plef  25612  i1fima  25618  i1fima2  25619  i1fd  25621  itg1ge0  25626  itg10  25628  i1f1lem  25629  i1fadd  25635  i1fmul  25636  i1fmulc  25643  mbfi1fseqlem5  25659  itg2addlem  25698  reldv  25810  dvbsss  25842  dvef  25923  lhop1lem  25957  deg1fvi  26029  plypf1  26156  coeeulem  26168  coeeu  26169  vieta1lem2  26258  aannenlem3  26277  aalioulem3  26281  dvradcnv  26369  pserulm  26370  pserdvlem2  26377  sinhalfpilem  26410  sincos4thpi  26460  tan4thpiOLD  26462  sincos6thpi  26463  pige3ALT  26467  resinf1o  26483  tanord1  26484  tanregt0  26486  efabl  26497  relogrn  26508  dfrelog  26512  logi  26534  logneg  26535  logltb  26547  logcn  26594  logf1o2  26597  dvlog  26598  efopnlem2  26604  efopn  26605  logccv  26610  dvsqrt  26689  dvcnsqrt  26691  cxpcn3  26696  logblog  26740  angpined  26778  1cubr  26790  asinsin  26840  asin1  26842  reasinsin  26844  atan0  26856  atanbnd  26874  atan1  26876  log2cnv  26892  log2ub  26897  log2le1  26898  birthday  26902  amgmlem  26938  emcllem5  26948  emgt0  26955  harmonicbnd3  26956  ftalem3  27023  basellem4  27032  sgmf  27093  ppi1  27112  cht1  27113  vma1  27114  ppiltx  27125  sqff1o  27130  ppiublem1  27151  ppiublem2  27152  ppiub  27153  chtub  27161  dchreq  27207  bposlem7  27239  bposlem8  27240  bposlem9  27241  lgsdir2lem2  27275  lgsdir2lem3  27276  chebbnd1  27421  chto1ub  27425  chpo1ubb  27430  pntibndlem1  27538  nosgnn0  27608  sltsolem1  27625  bdayfo  27627  nolt02o  27645  nogt01o  27646  noetasuplem4  27686  noetainflem4  27690  scutbdaybnd2lim  27767  madeun  27827  scutfo  27847  addsproplem2  27908  addsproplem7  27913  addsprop  27914  negsprop  27972  subsf  27999  mulsproplem13  28059  mulsproplem14  28060  mulsprop  28061  n0scut  28243  nohalf  28312  pw2bday  28323  0reno  28334  tgldimor  28415  tglnfn  28460  axlowdimlem4  28858  axlowdimlem16  28870  axlowdim  28874  upgrfi  29004  lfgrnloop  29038  lfuhgr1v0e  29167  usgrexmplef  29172  usgrres  29221  vdegp1bi  29451  vtxdginducedm1lem2  29454  dfpth2  29645  pthdlem2  29684  wpthswwlks2on  29877  0ewlk  30029  0pth  30040  konigsbergiedgw  30163  konigsberglem1  30167  konigsberglem2  30168  konigsberglem3  30169  konigsberglem4  30170  konigsberglem5  30171  ex-dif  30338  ex-un  30339  ex-in  30340  ex-fl  30362  avril1  30378  9p10ne21fool  30386  n0lplig  30398  cnidOLD  30497  cnnvm  30597  ipasslem8  30752  ipasslem10  30754  hvsubf  30930  normlem1  31025  normlem6  31030  normlem7  31031  norm-ii-i  31052  norm3adifii  31063  hilid  31076  hlimf  31152  hhssabloi  31177  hhssnv  31179  hhshsslem1  31182  shincli  31277  shsval2i  31302  shs0i  31364  chj0i  31370  chm1i  31371  chincli  31375  chdmm1i  31392  shjshsi  31407  chsup0  31463  h1de2bi  31469  spansnpji  31493  cmcmlem  31506  cmcmii  31512  cmcm2ii  31513  cmcm3ii  31514  pjidmi  31588  pjssmii  31596  pj0i  31608  pjocini  31613  mayetes3i  31644  df0op2  31667  hoaddcomi  31687  hoaddassi  31691  hocadddiri  31694  hocsubdiri  31695  hoaddridi  31701  ho0coi  31703  hoid1i  31704  hoid1ri  31705  hodseqi  31709  honegsubi  31711  adj1o  31809  hoddii  31904  lnopunilem1  31925  lnopunilem2  31926  nmcopexi  31942  nmcopex  31944  nmcoplb  31945  nmcfnexi  31966  nmcfnex  31968  nmcfnlb  31969  adjbd1o  32000  adjcoi  32015  nmopcoadji  32016  opsqrlem6  32060  pjsdii  32070  pjddii  32071  pjidmcoi  32092  pjtoi  32094  pjin1i  32107  pjclem1  32110  stji1i  32157  reuxfrdf  32406  iuninc  32475  fnresin  32538  rinvf1o  32542  suppss2f  32550  xppreima  32557  ofoprabco  32576  fressupp  32599  supppreima  32602  fsupprnfi  32603  gtiso  32612  df1stres  32615  df2ndres  32616  snct  32627  padct  32633  fsuppcurry1  32638  fsuppcurry2  32639  ffsrn  32642  fpwrelmapffs  32647  fzodif1  32706  nnindf  32735  nn0min  32736  dp2lt  32796  dp2ltsuc  32797  dp2ltc  32798  dplti  32816  dpmul  32824  dpmul4  32825  ressplusf  32877  chnub  32930  xrsclat  32941  xrge0base  32944  xrge00  32945  xrnarchi  33119  elrgspnlem2  33175  1fldgenq  33253  xrge0slmod  33300  zringfrac  33506  ply1degltdimlem  33597  ccfldsrarelvec  33647  ccfldextdgrr  33648  locfinreflem  33800  locfinref  33801  unicls  33863  sqsscirc1  33868  mhmhmeotmd  33887  raddcn  33889  xrge0iifiso  33895  xrge0iifhmeo  33896  lmxrge0  33912  cnzh  33928  rezh  33929  qqh0  33944  qqh1  33945  qqhre  33980  rrhre  33981  esumnul  34008  esum0  34009  esumsnf  34024  esumpfinvallem  34034  esumpfinvalf  34036  esumpcvgval  34038  esumcvgsum  34048  esumsup  34049  esumcvgre  34051  sigaclfu2  34081  dmsigagen  34104  ddemeas  34196  mbfmvolf  34227  br2base  34230  omssubadd  34261  sibfof  34301  sitg0  34307  eulerpartlemt  34332  eulerpartgbij  34333  0rrv  34412  coinfliplem  34440  coinflipprob  34441  coinfliprv  34444  ballotlem2  34450  ballotlem4  34460  ballotlem5  34461  ballotlemi1  34464  ballotlem7  34497  ballotth  34499  signsplypnf  34511  signsply0  34512  signsw0g  34517  signswch  34522  signsvf0  34541  hashreprin  34581  reprfz1  34585  chtvalz  34590  hgt750lemd  34609  hgt750lem  34612  hgt750lem2  34613  bnj1098  34743  bnj1109  34746  bnj1131  34747  bnj1533  34812  bnj151  34837  bnj580  34873  bnj852  34881  bnj864  34882  bnj865  34883  bnj978  34909  bnj1021  34926  bnj907  34927  bnj1093  34940  bnj1145  34953  bnj1172  34961  bnj1174  34963  bnj1176  34965  bnj1186  34967  nfan1c  35033  fineqvac  35057  subfacf  35126  subfacp1lem1  35130  subfacp1lem5  35135  subfacp1lem6  35136  subfacval3  35140  erdszelem2  35143  kur14lem4  35160  ioosconn  35198  iccllysconn  35201  satfn  35306  fmlaomn0  35341  gonan0  35343  goaln0  35344  elnanelprv  35380  msrfo  35497  mthmpps  35533  problem5  35620  quad3  35621  circum  35625  axextprim  35647  axrepprim  35648  axunprim  35649  axinfprim  35652  axacprim  35653  bcneg1  35682  setinds  35725  dfon2lem2  35731  dfon2lem4  35733  axextdfeq  35744  fobigcup  35847  snelsingles  35869  fullfunfnv  35893  fullfunfv  35894  rankaltopb  35926  rank0  36117  rankeq1o  36118  hfuni  36131  in-ax8  36171  fneer  36300  neibastop1  36306  nabi1i  36341  nabi2i  36342  limsucncmpi  36392  knoppcnlem8  36447  knoppcnlem11  36450  cnndvlem1  36484  bj-consensusALT  36526  bj-sbidmOLD  36797  bj-n0i  36898  bj-snsetex  36910  bj-tagss  36927  bj-2upln0  36970  bj-2upln1upl  36971  bj-nuliota  37004  bj-0int  37048  bj-elid5  37116  bj-inftyexpitaufo  37149  bj-pinftyccb  37168  bj-minftyccb  37172  bj-pinftynminfty  37174  bj-isrvec  37241  iccioo01  37274  f1omptsnlem  37283  mptsnunlem  37285  topdifinffinlem  37294  relowlpssretop  37311  1oequni2o  37315  pibt2  37364  imadifss  37548  tan2h  37565  poimirlem3  37576  poimirlem9  37582  poimirlem16  37589  poimirlem17  37590  poimirlem18  37591  poimirlem19  37592  poimirlem20  37593  poimirlem22  37595  poimirlem30  37603  mblfinlem1  37610  mblfinlem2  37611  ovoliunnfl  37615  voliunnfl  37617  itg2addnclem  37624  itg2addnclem2  37625  asindmre  37656  areacirclem1  37661  fdc  37698  cntotbnd  37749  heiborlem6  37769  rrnval  37780  reheibor  37792  rngosn3  37877  brcnvrabga  38289  cnvresrn  38295  moantr  38311  inxp2  38314  dfxrn2  38323  cnvcosseq  38384  refrelcosslem  38409  1cosscnvxrn  38422  redundss3  38575  refrelsredund3  38581  refrelredund3  38584  eqvrel0  38733  eqvrelid  38736  prter2  38828  renegclALT  38910  mapdunirnN  41598  lcmeprodgcdi  41949  3factsumint2  41964  3factsumint3  41965  3factsumint4  41966  3factsumint  41967  lcmineqlem4  41974  3lexlogpow5ineq1  41996  3lexlogpow2ineq1  42000  dvrelogpow2b  42010  aks4d1p1p4  42013  aks4d1p8  42029  aks6d1c1  42058  aks6d1c2p2  42061  aks6d1c4  42066  2ap1caineq  42087  sticksstones1  42088  sticksstones2  42089  aks6d1c7lem2  42123  aks5lem3a  42131  aks5lem6  42134  unitscyglem2  42138  unitscyglem3  42139  metakunt6  42152  metakunt24  42170  sqdeccom12  42269  readvrec2  42336  readvcot  42339  resubf  42356  sn-0ne2  42381  sn-subf  42403  sn-nnne0  42423  sn-0lt1  42438  reneg1lt0  42441  rntrclfvOAI  42646  diophrw  42714  rabren3dioph  42770  pellexlem6  42789  pellex  42790  frmx  42869  frmy  42870  jm2.23  42952  jm2.27dlem3  42967  axac10  42989  pw2f1ocnv  42993  kelac2lem  43020  lmhmlnmsplit  43043  pwfi2f1o  43052  frlmpwfi  43054  insucid  43359  nla0003  43381  ifpbiidcor  43430  sucomisnotcard  43500  alephiso2  43514  alephiso3  43515  cnvnonrel  43544  rnnonrel  43547  resnonrel  43548  cononrel1  43550  cononrel2  43551  fvnonrel  43553  cnvcnvintabd  43556  cnvintabd  43559  rclexi  43571  rtrclex  43573  clcnvlem  43579  cnvrcl0  43581  dmtrcl  43583  rntrcl  43584  dfrtrcl5  43585  iunrelexp0  43658  dmtrclfvRP  43686  rntrclfv  43688  corcltrcl  43695  cotrclrcl  43698  0heALT  43739  frege54cor1a  43820  uneqsn  43981  clsk3nimkb  43996  int-sqdefd  44137  int-sqgeq0d  44142  rr-groth  44256  rr-grothprim  44257  rr-grothshort  44261  seff  44266  expgrowthi  44290  expgrowth  44292  binomcxplemnotnn0  44313  ee233  44477  ax6e2nd  44516  in1  44529  dfvd2ani  44541  dfvd2i  44543  dfvd3i  44550  dfvd3ani  44553  e0bi  44734  uun2221  44771  uun2221p1  44772  uun2221p2  44773  en3lpVD  44803  relopabVD  44859  ax6e2ndVD  44866  ax6e2ndALT  44888  permaxpow  44968  pssnssi  45059  nnf1oxpnn  45153  icof  45177  fnmptif  45223  rn1st  45231  negpilt0  45243  xrgtso  45306  supxrleubrnmptf  45412  xrpnf  45446  rexanuz2nf  45453  ioontr  45474  iccdifioo  45478  iccdifprioo  45479  uzinico2  45525  fsummulc1f  45536  fsumiunss  45540  fnlimfvre2  45642  limsupreuz  45702  limsup10ex  45738  icccncfext  45852  dvcosre  45877  dvsinax  45878  ioodvbdlimc1lem2  45897  ioodvbdlimc2lem  45899  dvmptmulf  45902  dvnmul  45908  dvmptfprodlem  45909  dvnprodlem2  45912  stoweidlem1  45966  stoweidlem26  45991  stoweidlem34  45999  stoweidlem44  46009  stoweid  46028  stirlinglem5  46043  dirkercncflem1  46068  fourierdlem44  46116  fourierdlem56  46127  fourierdlem62  46133  fourierdlem89  46160  fourierdlem91  46162  fourierdlem100  46171  fourierdlem102  46173  fourierdlem103  46174  fourierdlem104  46175  fourierdlem108  46179  fourierdlem112  46183  fourierdlem114  46185  fouriersw  46196  rrndistlt  46255  gsumge0cl  46336  sge0tsms  46345  sge0ltfirpmpt2  46391  ovn0  46531  hoidmv1le  46559  hoidmvle  46565  ovnsubadd2lem  46610  ovolval4lem1  46614  vonioolem2  46646  smflimlem3  46738  nsssmfmbf  46744  axorbtnotaiffb  46868  axorbciffatcxorb  46870  abnotbtaxb  46880  euabsneu  46993  sprval  47419  fmtnoinf  47476  1nevenALTV  47631  nfermltl8rev  47682  nfermltl2rev  47683  nnsum3primes4  47728  tgblthelfgott  47755  tgoldbachlt  47756  cycl3grtri  47867  isubgr3stgrlem3  47888  usgrexmpl1lem  47933  usgrexmpl2lem  47938  usgrexmpl2trifr  47949  ldepslinc  48379  ackval42  48570  rrx2plordso  48598  vsn  48684  dmtposss  48745  sepfsepc  48796  basresposfo  48846  rescofuf  48949  fuco2eld2  49088  fuco22a  49124  setc1onsubc  49340  alimp-no-surprise  49486  aacllem  49506  amgmwlem  49507  amgmlemALT  49508