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  854  ori  861  pm5.16  1015  dn1  1057  3ori  1423  cadan  1605  nic-dfim  1665  nic-dfneg  1666  nic-mp  1667  nic-mpALT  1668  tbw-negdf  1695  rb-imdf  1746  nfri  1785  mpgbi  1794  19.35i  1875  nfim1  2196  19.36i  2228  ax6  2386  sbie  2504  datisi  2677  disamis  2678  dimatis  2685  fresison  2686  bamalip  2689  axi12  2703  eqcomi  2743  eqtri  2762  eleqtri  2836  nfnfc  2915  neii  2939  necomi  2992  neeqtri  3010  neli  3045  nrex  3071  rexlimivOLD  3182  rexlimi  3256  nfra2wOLD  3297  eueqi  3717  euxfr2w  3728  euxfr2  3730  reuxfrd  3756  cdeqri  3774  sseqtri  4031  3sstr3i  4037  pssn2lp  4113  equncomi  4169  unssi  4200  ssini  4247  unabs  4270  inabs  4271  dfin4  4283  vn0  4350  inindif  4380  difidALT  4382  ab0orv  4388  ab0orvALT  4389  disjdif  4477  difin0  4479  pwundif  4628  snid  4666  rabrsn  4728  iinrab2  5074  symdifv  5090  rintn0  5113  breqtri  5172  axsepgfromrep  5299  bm1.3iiOLD  5307  ax6vsep  5308  notzfaus  5368  zfpow  5371  dtruALT2  5375  dtruALT  5393  reusv2lem4  5406  dtru  5446  el  5447  dtruOLD  5451  op1stb  5481  copsexgw  5500  copsexg  5501  uniop  5524  rn0  5938  dmresi  6071  somincom  6156  cnvimassrndm  6173  cnvcnv  6213  elid  6220  rescnvcnv  6225  cnvcnvres  6226  cocnvcnv2  6279  cores2  6280  co01  6282  cnviin  6307  predres  6361  iota4an  6544  fnopab  6706  mpt0  6710  fnmpti  6711  f1cnvcnv  6813  f1ovi  6887  eliman0  6946  fvco4i  7009  cnvimainrn  7086  fmpti  7131  funiunfv  7267  oprabss  7539  relmptopab  7682  zfun  7754  tfinds2  7884  omon  7898  2nd0  8019  f1stres  8036  f2ndres  8037  cnvoprab  8083  relmpoopab  8117  df1st2  8121  df2nd2  8122  fsplit  8140  frpoins3xpg  8163  frpoins3xp3g  8164  poxp2  8166  poseq  8181  reldmtpos  8257  dftpos4  8268  tpostpos  8269  tpos0  8279  frrlem4  8312  wfrlem4OLD  8350  smo0  8396  tfrlem14  8429  tfrlem16  8431  rdgsucg  8461  rdglimg  8463  frfnom  8473  oawordeulem  8590  uniixp  8959  dfdom2  9016  ssdomg  9038  xpcomf1o  9099  sbthlem5  9125  sdom0  9146  limensuci  9191  1sdom2  9273  fiint  9363  fiintOLD  9364  fidomdm  9371  residfi  9375  mptfi  9388  fisn  9464  dffi3  9468  ordtypelem6  9560  ordtypelem7  9561  wemaplem2  9584  harwdom  9628  suc11reg  9656  zfinf  9676  axinf2  9677  noinfep  9697  cantnfvalf  9702  cantnflt  9709  cantnf0  9712  cantnf  9730  ttrclco  9755  tz9.1c  9767  tc2  9779  r111  9812  r1tr2  9814  r1ordg  9815  r1sssuc  9820  r1val1  9823  tz9.13  9828  r1elssi  9842  pwwf  9844  rankopb  9889  rankeq0b  9897  ranksuc  9902  rankmapu  9915  rankxplim3  9918  rankxpsuc  9919  cp  9928  karden  9932  card0  9995  cardlim  10009  cardom  10023  infxpenlem  10050  alephsuc2  10117  alephgeom  10119  unialeph  10138  dfac4  10159  dfacacn  10179  dju1dif  10210  dju1p1e2  10211  infdju1  10227  ackbij1lem13  10268  ackbij2  10279  cf0  10288  cfsuc  10294  cfom  10301  cfslb2n  10305  ominf4  10349  fin23lem17  10375  fin23lem28  10377  fin23lem30  10379  fin23lem31  10380  fin23lem40  10388  isfin1-3  10423  dfacfin7  10436  fin1a2lem6  10442  itunitc1  10457  axcc3  10475  dcomex  10484  axdc2lem  10485  axcclem  10494  zfac  10497  ac3  10499  ackm  10502  axac2  10503  axac  10504  axaci  10505  cardeqv  10506  numth2  10508  numth  10509  dmct  10561  brdom3  10565  fin71ac  10570  cardf  10587  aleph1  10608  cfpwsdom  10621  smobeth  10623  zfcndrep  10651  zfcndpow  10653  zfcndac  10656  gch2  10712  wunex3  10778  tskpr  10807  inar1  10812  rankcf  10814  tskcard  10818  tskuni  10820  grothpw  10863  axgroth4  10869  grothprim  10871  inaprc  10873  dmaddpi  10927  dmmulpi  10928  1lt2pi  10942  addpqf  10981  mulpqf  10983  1lt2nq  11010  supsrlem  11148  ssxr  11327  gtso  11339  subf  11507  negne0i  11581  mulnzcnf  11906  infrenegsup  12248  nnne0  12297  halflt1  12481  nn0ssz  12633  3halfnz  12694  zeo  12701  numlt  12755  numltc  12756  le9lt10  12757  decle  12764  uzf  12878  xaddf  13262  xsubge0  13299  xmulf  13310  ixxf  13393  ixxssxr  13395  iooval2  13416  ioof  13483  unirnioo  13485  dfioo2  13486  fzval2  13546  fzf  13547  0nelfz1  13579  fz10  13581  fzpreddisj  13609  4fvwrd4  13684  fzof  13692  fzo0  13719  fldiv4p1lem1div2  13871  fldiv4lem1div2  13873  om2uzoi  13992  faclbnd4lem1  14328  hashkf  14367  hashgval  14368  hashinf  14370  hashresfn  14375  hashnn0n0nn  14426  hashge3el3dif  14522  hash3tpde  14528  rev0  14798  s2dm  14925  f1oun2prg  14952  trclublem  15030  sqrt2gt1lt2  15309  limsupgord  15504  fclim  15585  fsumrelem  15839  ackbijnn  15860  incexclem  15868  incexc  15869  arisum2  15893  georeclim  15904  geoisumr  15910  0.999...  15913  risefall0lem  16058  ege2le3  16122  sin0  16181  ef01bndlem  16216  cos2bnd  16220  cos01gt0  16223  sincos2sgn  16226  sin4lt0  16227  rpnnen2lem3  16248  rpnnen2lem9  16254  rexpen  16260  cnso  16279  dvdslelem  16342  divalglem1  16427  divalglem5  16430  divalglem6  16431  divalglem10  16435  flodddiv4  16448  0bits  16472  sadcf  16486  sadcadd  16491  bitsshft  16508  smupf  16511  gcdf  16545  eucalgf  16616  2prm  16725  dfphi2  16807  pockthi  16940  prmrec  16955  vdwapf  17005  vdwlem6  17019  karatsuba  17117  1259lem5  17168  2503lem3  17172  4001lem4  17177  structcnvcnv  17186  structfn  17189  strleun  17190  imasvscafn  17583  xpsff1o  17613  wunnat  18010  wunnatOLD  18011  dfinito3  18058  dftermo3  18059  eldmcoa  18118  coapm  18124  catcfuccl  18172  catcfucclOLD  18173  catcxpccl  18262  catcxpcclOLD  18263  yonedainv  18337  smndex1bas  18931  smndex1n0mnd  18937  grpinvfvi  19012  mulgfvi  19103  ressmulgnnd  19108  symgsssg  19499  symgfisg  19500  psgnunilem5  19526  sylow3lem2  19660  oppglsm  19674  efgmf  19745  efgval  19749  efgsf  19761  0frgp  19811  dmdprd  20032  dprdval  20037  invrfval  20405  drngui  20751  rmodislmod  20944  rmodislmodOLD  20945  lssintcl  20979  cnfldadd  21387  cnfldmul  21389  cnfldfunALT  21396  dfcnfldOLD  21397  cnfldfunALTOLD  21409  cnfldfunALTOLDOLD  21410  cnfld0  21422  cnfld1  21423  cnfld1OLD  21424  cnfldsub  21427  xrsds  21444  pzriprnglem4  21512  pzriprnglem9  21517  pzriprnglem14  21522  psgnghm  21615  zrhpsgnmhm  21619  ocv1  21714  dsmmbas2  21774  mplsubrglem  22041  opsrtoslem2  22097  evl1maprhm  22398  mdetralt  22629  maducoeval2  22661  eltpsi  22966  unitg  22989  fctop  23026  cctop  23028  ppttop  23029  epttop  23031  leordtvallem1  23233  leordtvallem2  23234  iccordt  23237  iscnp2  23262  discmp  23421  conncompcld  23457  1stcrestlem  23475  2ndcdisj  23479  topnlly  23514  disllycmp  23521  dis1stc  23522  txuni2  23588  xkotf  23608  dfac14lem  23640  prdstps  23652  txindis  23657  tx1stc  23673  xkohaus  23676  xkoptsub  23677  cnmpt1st  23691  cnmpt2nd  23692  ptcmpfi  23836  trfil1  23909  fin1aufil  23955  tgpconncompeqg  24135  tgpconncomp  24136  trust  24253  met1stc  24549  dscmet  24600  retopon  24799  cnfldtopon  24818  xrsxmet  24844  xrsmopn  24847  iimulcn  24980  iimulcnOLD  24981  icopnfhmeo  24987  iccpnfhmeo  24989  xrhmeo  24990  cnheiborlem  24999  lebnumii  25011  ishtpy  25017  htpycc  25025  pco1  25061  pcohtpylem  25065  pcopt  25068  pcopt2  25069  pcoass  25070  pcorevlem  25072  rrxcph  25439  rrx0el  25445  ovoliunlem3  25552  ovolicc1  25564  ovolicc2  25570  volf  25577  ioorf  25621  dyadf  25639  dyadmbl  25648  vitalilem5  25660  vitali  25661  mbfimaopnlem  25703  mbflimsup  25714  0plef  25720  i1fima  25726  i1fima2  25727  i1fd  25729  itg1ge0  25734  itg10  25736  i1f1lem  25737  i1fadd  25743  i1fmul  25744  i1fmulc  25752  mbfi1fseqlem5  25768  itg2addlem  25807  reldv  25919  dvbsss  25951  dvef  26032  lhop1lem  26066  deg1fvi  26138  plypf1  26265  coeeulem  26277  coeeu  26278  vieta1lem2  26367  aannenlem3  26386  aalioulem3  26390  dvradcnv  26478  pserulm  26479  pserdvlem2  26486  sinhalfpilem  26519  sincos4thpi  26569  tan4thpiOLD  26571  sincos6thpi  26572  pige3ALT  26576  resinf1o  26592  tanord1  26593  tanregt0  26595  efabl  26606  relogrn  26617  dfrelog  26621  logi  26643  logneg  26644  logltb  26656  logcn  26703  logf1o2  26706  dvlog  26707  efopnlem2  26713  efopn  26714  logccv  26719  dvsqrt  26798  dvcnsqrt  26800  cxpcn3  26805  logblog  26849  angpined  26887  1cubr  26899  asinsin  26949  asin1  26951  reasinsin  26953  atan0  26965  atanbnd  26983  atan1  26985  log2cnv  27001  log2ub  27006  log2le1  27007  birthday  27011  amgmlem  27047  emcllem5  27057  emgt0  27064  harmonicbnd3  27065  ftalem3  27132  basellem4  27141  sgmf  27202  ppi1  27221  cht1  27222  vma1  27223  ppiltx  27234  sqff1o  27239  ppiublem1  27260  ppiublem2  27261  ppiub  27262  chtub  27270  dchreq  27316  bposlem7  27348  bposlem8  27349  bposlem9  27350  lgsdir2lem2  27384  lgsdir2lem3  27385  chebbnd1  27530  chto1ub  27534  chpo1ubb  27539  pntibndlem1  27647  nosgnn0  27717  sltsolem1  27734  bdayfo  27736  nolt02o  27754  nogt01o  27755  noetasuplem4  27795  noetainflem4  27799  scutbdaybnd2lim  27876  madeun  27936  scutfo  27956  addsproplem2  28017  addsproplem7  28022  addsprop  28023  negsprop  28081  subsf  28108  mulsproplem13  28168  mulsproplem14  28169  mulsprop  28170  n0scut  28352  nohalf  28421  pw2bday  28432  0reno  28443  tgldimor  28524  tglnfn  28569  axlowdimlem4  28974  axlowdimlem16  28986  axlowdim  28990  upgrfi  29122  lfgrnloop  29156  lfuhgr1v0e  29285  usgrexmplef  29290  usgrres  29339  vdegp1bi  29569  vtxdginducedm1lem2  29572  pthdlem2  29800  wpthswwlks2on  29990  0ewlk  30142  0pth  30153  konigsbergiedgw  30276  konigsberglem1  30280  konigsberglem2  30281  konigsberglem3  30282  konigsberglem4  30283  konigsberglem5  30284  ex-dif  30451  ex-un  30452  ex-in  30453  ex-fl  30475  avril1  30491  9p10ne21fool  30499  n0lplig  30511  cnidOLD  30610  cnnvm  30710  ipasslem8  30865  ipasslem10  30867  hvsubf  31043  normlem1  31138  normlem6  31143  normlem7  31144  norm-ii-i  31165  norm3adifii  31176  hilid  31189  hlimf  31265  hhssabloi  31290  hhssnv  31292  hhshsslem1  31295  shincli  31390  shsval2i  31415  shs0i  31477  chj0i  31483  chm1i  31484  chincli  31488  chdmm1i  31505  shjshsi  31520  chsup0  31576  h1de2bi  31582  spansnpji  31606  cmcmlem  31619  cmcmii  31625  cmcm2ii  31626  cmcm3ii  31627  pjidmi  31701  pjssmii  31709  pj0i  31721  pjocini  31726  mayetes3i  31757  df0op2  31780  hoaddcomi  31800  hoaddassi  31804  hocadddiri  31807  hocsubdiri  31808  hoaddridi  31814  ho0coi  31816  hoid1i  31817  hoid1ri  31818  hodseqi  31822  honegsubi  31824  adj1o  31922  hoddii  32017  lnopunilem1  32038  lnopunilem2  32039  nmcopexi  32055  nmcopex  32057  nmcoplb  32058  nmcfnexi  32079  nmcfnex  32081  nmcfnlb  32082  adjbd1o  32113  adjcoi  32128  nmopcoadji  32129  opsqrlem6  32173  pjsdii  32183  pjddii  32184  pjidmcoi  32205  pjtoi  32207  pjin1i  32220  pjclem1  32223  stji1i  32270  reuxfrdf  32518  iuninc  32580  fnresin  32642  rinvf1o  32646  suppss2f  32654  xppreima  32661  ofoprabco  32680  fressupp  32702  supppreima  32705  fsupprnfi  32706  gtiso  32715  df1stres  32718  df2ndres  32719  snct  32730  padct  32736  fsuppcurry1  32742  fsuppcurry2  32743  ffsrn  32746  fpwrelmapffs  32751  fzodif1  32800  nnindf  32825  nn0min  32826  dp2lt  32851  dp2ltsuc  32852  dp2ltc  32853  dplti  32871  dpmul  32879  dpmul4  32880  ressplusf  32932  chnub  32985  xrsclat  32995  xrge0base  32998  xrge00  32999  xrnarchi  33173  elrgspnlem2  33232  1fldgenq  33303  xrge0slmod  33355  zringfrac  33561  ply1degltdimlem  33649  ccfldsrarelvec  33695  ccfldextdgrr  33696  locfinreflem  33800  locfinref  33801  unicls  33863  sqsscirc1  33868  mhmhmeotmd  33887  raddcn  33889  xrge0iifiso  33895  xrge0iifhmeo  33896  lmxrge0  33912  cnzh  33930  rezh  33931  qqh0  33946  qqh1  33947  qqhre  33982  rrhre  33983  esumnul  34028  esum0  34029  esumsnf  34044  esumpfinvallem  34054  esumpfinvalf  34056  esumpcvgval  34058  esumcvgsum  34068  esumsup  34069  esumcvgre  34071  sigaclfu2  34101  dmsigagen  34124  ddemeas  34216  mbfmvolf  34247  br2base  34250  omssubadd  34281  sibfof  34321  sitg0  34327  eulerpartlemt  34352  eulerpartgbij  34353  0rrv  34432  coinfliplem  34459  coinflipprob  34460  coinfliprv  34463  ballotlem2  34469  ballotlem4  34479  ballotlem5  34480  ballotlemi1  34483  ballotlem7  34516  ballotth  34518  signsplypnf  34543  signsply0  34544  signsw0g  34549  signswch  34554  signsvf0  34573  hashreprin  34613  reprfz1  34617  chtvalz  34622  hgt750lemd  34641  hgt750lem  34644  hgt750lem2  34645  bnj1098  34775  bnj1109  34778  bnj1131  34779  bnj1533  34844  bnj151  34869  bnj580  34905  bnj852  34913  bnj864  34914  bnj865  34915  bnj978  34941  bnj1021  34958  bnj907  34959  bnj1093  34972  bnj1145  34985  bnj1172  34993  bnj1174  34995  bnj1176  34997  bnj1186  34999  nfan1c  35065  fineqvac  35089  subfacf  35159  subfacp1lem1  35163  subfacp1lem5  35168  subfacp1lem6  35169  subfacval3  35173  erdszelem2  35176  kur14lem4  35193  ioosconn  35231  iccllysconn  35234  satfn  35339  fmlaomn0  35374  gonan0  35376  goaln0  35377  elnanelprv  35413  msrfo  35530  mthmpps  35566  problem5  35653  quad3  35654  circum  35658  axextprim  35680  axrepprim  35681  axunprim  35682  axinfprim  35685  axacprim  35686  bcneg1  35715  setinds  35759  dfon2lem2  35765  dfon2lem4  35767  axextdfeq  35778  fobigcup  35881  snelsingles  35903  fullfunfnv  35927  fullfunfv  35928  rankaltopb  35960  rank0  36151  rankeq1o  36152  hfuni  36165  in-ax8  36206  fneer  36335  neibastop1  36341  nabi1i  36376  nabi2i  36377  limsucncmpi  36427  knoppcnlem8  36482  knoppcnlem11  36485  cnndvlem1  36519  bj-consensusALT  36561  bj-sbidmOLD  36832  bj-n0i  36933  bj-snsetex  36945  bj-tagss  36962  bj-2upln0  37005  bj-2upln1upl  37006  bj-nuliota  37039  bj-0int  37083  bj-elid5  37151  bj-inftyexpitaufo  37184  bj-pinftyccb  37203  bj-minftyccb  37207  bj-pinftynminfty  37209  bj-isrvec  37276  iccioo01  37309  f1omptsnlem  37318  mptsnunlem  37320  topdifinffinlem  37329  relowlpssretop  37346  1oequni2o  37350  pibt2  37399  imadifss  37581  tan2h  37598  poimirlem3  37609  poimirlem9  37615  poimirlem16  37622  poimirlem17  37623  poimirlem18  37624  poimirlem19  37625  poimirlem20  37626  poimirlem22  37628  poimirlem30  37636  mblfinlem1  37643  mblfinlem2  37644  ovoliunnfl  37648  voliunnfl  37650  itg2addnclem  37657  itg2addnclem2  37658  asindmre  37689  areacirclem1  37694  fdc  37731  cntotbnd  37782  heiborlem6  37802  rrnval  37813  reheibor  37825  rngosn3  37910  brcnvrabga  38323  cnvresrn  38329  moantr  38345  inxp2  38348  dfxrn2  38357  cnvcosseq  38418  refrelcosslem  38443  1cosscnvxrn  38456  redundss3  38609  refrelsredund3  38615  refrelredund3  38618  eqvrel0  38767  eqvrelid  38770  prter2  38862  renegclALT  38944  mapdunirnN  41632  lcmeprodgcdi  41988  3factsumint2  42003  3factsumint3  42004  3factsumint4  42005  3factsumint  42006  lcmineqlem4  42013  3lexlogpow5ineq1  42035  3lexlogpow2ineq1  42039  dvrelogpow2b  42049  aks4d1p1p4  42052  aks4d1p8  42068  aks6d1c1  42097  aks6d1c2p2  42100  aks6d1c4  42105  2ap1caineq  42126  sticksstones1  42127  sticksstones2  42128  aks6d1c7lem2  42162  aks5lem3a  42170  aks5lem6  42173  unitscyglem2  42177  unitscyglem3  42178  metakunt6  42191  metakunt24  42209  sqdeccom12  42302  readvrec2  42369  readvrec  42370  resubf  42387  sn-0ne2  42412  sn-subf  42434  sn-nnne0  42454  sn-0lt1  42469  reneg1lt0  42472  rntrclfvOAI  42678  diophrw  42746  rabren3dioph  42802  pellexlem6  42821  pellex  42822  frmx  42901  frmy  42902  jm2.23  42984  jm2.27dlem3  42999  axac10  43021  pw2f1ocnv  43025  kelac2lem  43052  lmhmlnmsplit  43075  pwfi2f1o  43084  frlmpwfi  43086  insucid  43392  nla0003  43414  ifpbiidcor  43463  sucomisnotcard  43533  alephiso2  43547  alephiso3  43548  cnvnonrel  43577  rnnonrel  43580  resnonrel  43581  cononrel1  43583  cononrel2  43584  fvnonrel  43586  cnvcnvintabd  43589  cnvintabd  43592  rclexi  43604  rtrclex  43606  clcnvlem  43612  cnvrcl0  43614  dmtrcl  43616  rntrcl  43617  dfrtrcl5  43618  iunrelexp0  43691  dmtrclfvRP  43719  rntrclfv  43721  corcltrcl  43728  cotrclrcl  43731  0heALT  43772  frege54cor1a  43853  uneqsn  44014  clsk3nimkb  44029  int-sqdefd  44170  int-sqgeq0d  44175  rr-groth  44294  rr-grothprim  44295  rr-grothshort  44299  seff  44304  expgrowthi  44328  expgrowth  44330  binomcxplemnotnn0  44351  ee233  44516  ax6e2nd  44555  in1  44568  dfvd2ani  44580  dfvd2i  44582  dfvd3i  44589  dfvd3ani  44592  e0bi  44773  uun2221  44810  uun2221p1  44811  uun2221p2  44812  en3lpVD  44842  relopabVD  44898  ax6e2ndVD  44905  ax6e2ndALT  44927  pssnssi  45040  nnf1oxpnn  45137  icof  45161  fnmptif  45210  rn1st  45218  negpilt0  45230  xrgtso  45294  supxrleubrnmptf  45400  xrpnf  45435  rexanuz2nf  45442  ioontr  45463  iccdifioo  45467  iccdifprioo  45468  uzinico2  45514  fsummulc1f  45526  fsumiunss  45530  fnlimfvre2  45632  limsupreuz  45692  limsup10ex  45728  icccncfext  45842  dvcosre  45867  dvsinax  45868  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  dvmptmulf  45892  dvnmul  45898  dvmptfprodlem  45899  dvnprodlem2  45902  stoweidlem1  45956  stoweidlem26  45981  stoweidlem34  45989  stoweidlem44  45999  stoweid  46018  stirlinglem5  46033  dirkercncflem1  46058  fourierdlem44  46106  fourierdlem56  46117  fourierdlem62  46123  fourierdlem89  46150  fourierdlem91  46152  fourierdlem100  46161  fourierdlem102  46163  fourierdlem103  46164  fourierdlem104  46165  fourierdlem108  46169  fourierdlem112  46173  fourierdlem114  46175  fouriersw  46186  rrndistlt  46245  gsumge0cl  46326  sge0tsms  46335  sge0ltfirpmpt2  46381  ovn0  46521  hoidmv1le  46549  hoidmvle  46555  ovnsubadd2lem  46600  ovolval4lem1  46604  vonioolem2  46636  smflimlem3  46728  nsssmfmbf  46734  axorbtnotaiffb  46852  axorbciffatcxorb  46854  abnotbtaxb  46864  euabsneu  46977  sprval  47403  fmtnoinf  47460  1nevenALTV  47615  nfermltl8rev  47666  nfermltl2rev  47667  nnsum3primes4  47712  tgblthelfgott  47739  tgoldbachlt  47740  isubgr3stgrlem3  47870  usgrexmpl1lem  47915  usgrexmpl2lem  47920  usgrexmpl2trifr  47931  ldepslinc  48354  ackval42  48545  rrx2plordso  48573  vsn  48659  sepfsepc  48723  alimp-no-surprise  49011  aacllem  49031  amgmwlem  49032  amgmlemALT  49033