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  1426  cadan  1610  nic-dfim  1670  nic-dfneg  1671  nic-mp  1672  nic-mpALT  1673  tbw-negdf  1700  rb-imdf  1751  nfri  1790  mpgbi  1799  19.35i  1879  nfim1  2204  19.36i  2236  ax6  2386  sbie  2504  datisi  2677  disamis  2678  dimatis  2685  fresison  2686  bamalip  2689  axi12  2703  eqcomi  2742  eqtri  2756  eleqtri  2831  nfnfc  2908  neii  2931  necomi  2983  neeqtri  3001  neli  3035  nrex  3061  rexlimi  3233  eueqi  3664  euxfr2w  3675  euxfr2  3677  reuxfrd  3703  cdeqri  3721  sseqtri  3979  pssn2lp  4053  equncomi  4109  unssi  4140  ssini  4189  unabs  4214  inabs  4215  dfin4  4227  vn0  4294  inindif  4324  difidALT  4326  ab0orv  4332  ab0orvALT  4333  disjdif  4421  difin0  4423  pwundif  4573  snid  4614  rabrsn  4676  iinrab2  5020  symdifv  5036  rintn0  5059  breqtri  5118  axsepgfromrep  5234  bm1.3iiOLD  5242  ax6vsep  5243  notzfaus  5303  zfpow  5306  dtruALT2  5310  dtruALT  5328  reusv2lem4  5341  dtru  5381  el  5382  op1stb  5414  copsexgw  5433  copsexg  5434  uniop  5458  rn0  5870  dmresi  6005  somincom  6085  cnvimassrndm  6104  cnvcnv  6144  elid  6151  rescnvcnv  6156  cnvcnvres  6157  cocnvcnv2  6211  cores2  6212  co01  6214  cnviin  6238  predres  6291  iota4an  6468  fnopab  6624  mpt0  6628  fnmpti  6629  f1cnvcnv  6733  f1ovi  6808  eliman0  6865  fvco4i  6929  cnvimainrn  7006  fmpti  7051  funiunfv  7188  oprabss  7460  relmptopab  7602  zfun  7675  tfinds2  7800  omon  7814  2nd0  7934  f1stres  7951  f2ndres  7952  cnvoprab  7998  relmpoopab  8030  df1st2  8034  df2nd2  8035  fsplit  8053  frpoins3xpg  8076  frpoins3xp3g  8077  poxp2  8079  poseq  8094  reldmtpos  8170  dftpos4  8181  tpostpos  8182  tpos0  8192  frrlem4  8225  smo0  8284  tfrlem14  8316  tfrlem16  8318  rdgsucg  8348  rdglimg  8350  frfnom  8360  oawordeulem  8475  uniixp  8851  dfdom2  8907  ssdomg  8929  xpcomf1o  8986  sbthlem5  9011  sdom0  9029  limensuci  9073  1sdom2  9139  fiint  9218  fidomdm  9225  residfi  9229  mptfi  9242  fisn  9318  dffi3  9322  ordtypelem6  9416  ordtypelem7  9417  wemaplem2  9440  harwdom  9484  nelaneq  9494  suc11reg  9516  zfinf  9536  axinf2  9537  noinfep  9557  cantnfvalf  9562  cantnflt  9569  cantnf0  9572  cantnf  9590  ttrclco  9615  tz9.1c  9627  tc2  9637  setinds  9646  r111  9675  r1tr2  9677  r1ordg  9678  r1sssuc  9683  r1val1  9686  tz9.13  9691  r1elssi  9705  pwwf  9707  rankopb  9752  rankeq0b  9760  ranksuc  9765  rankmapu  9778  rankxplim3  9781  rankxpsuc  9782  cp  9791  karden  9795  card0  9858  cardlim  9872  cardom  9886  infxpenlem  9911  alephsuc2  9978  alephgeom  9980  unialeph  9999  dfac4  10020  dfacacn  10040  dju1dif  10071  dju1p1e2  10072  infdju1  10088  ackbij1lem13  10129  ackbij2  10140  cf0  10149  cfsuc  10155  cfom  10162  cfslb2n  10166  ominf4  10210  fin23lem17  10236  fin23lem28  10238  fin23lem30  10240  fin23lem31  10241  fin23lem40  10249  isfin1-3  10284  dfacfin7  10297  fin1a2lem6  10303  itunitc1  10318  axcc3  10336  dcomex  10345  axdc2lem  10346  axcclem  10355  zfac  10358  ac3  10360  ackm  10363  axac2  10364  axac  10365  axaci  10366  cardeqv  10367  numth2  10369  numth  10370  dmct  10422  brdom3  10426  fin71ac  10431  cardf  10448  aleph1  10469  cfpwsdom  10482  smobeth  10484  zfcndrep  10512  zfcndpow  10514  zfcndac  10517  gch2  10573  wunex3  10639  tskpr  10668  inar1  10673  rankcf  10675  tskcard  10679  tskuni  10681  grothpw  10724  axgroth4  10730  grothprim  10732  inaprc  10734  dmaddpi  10788  dmmulpi  10789  1lt2pi  10803  addpqf  10842  mulpqf  10844  1lt2nq  10871  supsrlem  11009  ssxr  11189  gtso  11201  subf  11369  negne0i  11443  mulnzcnf  11770  infrenegsup  12112  neg1lt0  12120  nnne0  12166  halflt1  12345  nn0ssz  12498  3halfnz  12558  zeo  12565  numlt  12619  numltc  12620  le9lt10  12621  decle  12628  uzf  12741  xaddf  13125  xsubge0  13162  xmulf  13173  ixxf  13257  ixxssxr  13259  iooval2  13280  ioof  13349  unirnioo  13351  dfioo2  13352  fzval2  13412  fzf  13413  0nelfz1  13445  fz10  13447  fzpreddisj  13475  4fvwrd4  13550  fzof  13558  fzo0  13585  fldiv4p1lem1div2  13741  fldiv4lem1div2  13743  om2uzoi  13864  faclbnd4lem1  14202  hashkf  14241  hashgval  14242  hashinf  14244  hashresfn  14249  hashnn0n0nn  14300  hashge3el3dif  14396  hash3tpde  14402  rev0  14673  s2dm  14799  f1oun2prg  14826  trclublem  14904  sqrt2gt1lt2  15183  limsupgord  15381  fclim  15462  fsumrelem  15716  ackbijnn  15737  incexclem  15745  incexc  15746  arisum2  15770  georeclim  15781  geoisumr  15787  0.999...  15790  risefall0lem  15935  ege2le3  15999  sin0  16060  ef01bndlem  16095  cos2bnd  16099  cos01gt0  16102  sincos2sgn  16105  sin4lt0  16106  rpnnen2lem3  16127  rpnnen2lem9  16133  rexpen  16139  cnso  16158  dvdslelem  16222  divalglem1  16307  divalglem5  16310  divalglem6  16311  divalglem10  16315  flodddiv4  16328  0bits  16352  sadcf  16366  sadcadd  16371  bitsshft  16388  smupf  16391  gcdf  16425  eucalgf  16496  2prm  16605  dfphi2  16687  pockthi  16821  prmrec  16836  vdwapf  16886  vdwlem6  16900  karatsuba  16997  1259lem5  17048  2503lem3  17052  4001lem4  17057  structcnvcnv  17066  structfn  17069  strleun  17070  imasvscafn  17443  xpsff1o  17473  xrge0base  17513  wunnat  17868  dfinito3  17914  dftermo3  17915  eldmcoa  17974  coapm  17980  catcfuccl  18027  catcxpccl  18115  yonedainv  18189  chnub  18530  smndex1bas  18816  smndex1n0mnd  18822  grpinvfvi  18897  mulgfvi  18988  ressmulgnnd  18993  symgsssg  19381  symgfisg  19382  psgnunilem5  19408  sylow3lem2  19542  oppglsm  19556  efgmf  19627  efgval  19631  efgsf  19643  0frgp  19693  dmdprd  19914  dprdval  19919  invrfval  20309  drngui  20652  rmodislmod  20865  lssintcl  20899  cnfldadd  21299  cnfldmul  21301  cnfldfunALT  21308  dfcnfldOLD  21309  cnfldfunALTOLD  21321  cnfld0  21331  cnfld1  21332  cnfld1OLD  21333  cnfldsub  21336  xrsds  21348  pzriprnglem4  21423  pzriprnglem9  21428  pzriprnglem14  21433  psgnghm  21519  zrhpsgnmhm  21523  ocv1  21618  dsmmbas2  21676  mplsubrglem  21942  opsrtoslem2  21992  evl1maprhm  22295  mdetralt  22524  maducoeval2  22556  eltpsi  22860  unitg  22883  fctop  22920  cctop  22922  ppttop  22923  epttop  22925  leordtvallem1  23126  leordtvallem2  23127  iccordt  23130  iscnp2  23155  discmp  23314  conncompcld  23350  1stcrestlem  23368  2ndcdisj  23372  topnlly  23407  disllycmp  23414  dis1stc  23415  txuni2  23481  xkotf  23501  dfac14lem  23533  prdstps  23545  txindis  23550  tx1stc  23566  xkohaus  23569  xkoptsub  23570  cnmpt1st  23584  cnmpt2nd  23585  ptcmpfi  23729  trfil1  23802  fin1aufil  23848  tgpconncompeqg  24028  tgpconncomp  24029  trust  24145  met1stc  24437  dscmet  24488  retopon  24679  cnfldtopon  24698  xrsxmet  24726  xrsmopn  24729  iimulcn  24862  iimulcnOLD  24863  icopnfhmeo  24869  iccpnfhmeo  24871  xrhmeo  24872  cnheiborlem  24881  lebnumii  24893  ishtpy  24899  htpycc  24907  pco1  24943  pcohtpylem  24947  pcopt  24950  pcopt2  24951  pcoass  24952  pcorevlem  24954  rrxcph  25320  rrx0el  25326  ovoliunlem3  25433  ovolicc1  25445  ovolicc2  25451  volf  25458  ioorf  25502  dyadf  25520  dyadmbl  25529  vitalilem5  25541  vitali  25542  mbfimaopnlem  25584  mbflimsup  25595  0plef  25601  i1fima  25607  i1fima2  25608  i1fd  25610  itg1ge0  25615  itg10  25617  i1f1lem  25618  i1fadd  25624  i1fmul  25625  i1fmulc  25632  mbfi1fseqlem5  25648  itg2addlem  25687  reldv  25799  dvbsss  25831  dvef  25912  lhop1lem  25946  deg1fvi  26018  plypf1  26145  coeeulem  26157  coeeu  26158  vieta1lem2  26247  aannenlem3  26266  aalioulem3  26270  dvradcnv  26358  pserulm  26359  pserdvlem2  26366  sinhalfpilem  26400  sincos4thpi  26450  tan4thpiOLD  26452  sincos6thpi  26453  pige3ALT  26457  resinf1o  26473  tanord1  26474  tanregt0  26476  efabl  26487  relogrn  26498  dfrelog  26502  logi  26524  logneg  26525  logltb  26537  logcn  26584  logf1o2  26587  dvlog  26588  efopnlem2  26594  efopn  26595  logccv  26600  dvsqrt  26679  dvcnsqrt  26681  cxpcn3  26686  logblog  26730  angpined  26768  1cubr  26780  asinsin  26830  asin1  26832  reasinsin  26834  atan0  26846  atanbnd  26864  atan1  26866  log2cnv  26882  log2ub  26887  log2le1  26888  birthday  26892  amgmlem  26928  emcllem5  26938  emgt0  26945  harmonicbnd3  26946  ftalem3  27013  basellem4  27022  sgmf  27083  ppi1  27102  cht1  27103  vma1  27104  ppiltx  27115  sqff1o  27120  ppiublem1  27141  ppiublem2  27142  ppiub  27143  chtub  27151  dchreq  27197  bposlem7  27229  bposlem8  27230  bposlem9  27231  lgsdir2lem2  27265  lgsdir2lem3  27266  chebbnd1  27411  chto1ub  27415  chpo1ubb  27420  pntibndlem1  27528  nosgnn0  27598  sltsolem1  27615  bdayfo  27617  nolt02o  27635  nogt01o  27636  noetasuplem4  27676  noetainflem4  27680  scutbdaybnd2lim  27759  madeun  27830  scutfo  27851  addsproplem2  27914  addsproplem7  27919  addsprop  27920  negsprop  27978  subsf  28005  mulsproplem13  28068  mulsproplem14  28069  mulsprop  28070  onsiso  28206  n0scut  28263  bdayn0sf1o  28296  twocut  28347  0reno  28400  tgldimor  28481  tglnfn  28526  axlowdimlem4  28925  axlowdimlem16  28937  axlowdim  28941  upgrfi  29071  lfgrnloop  29105  lfuhgr1v0e  29234  usgrexmplef  29239  usgrres  29288  vdegp1bi  29518  vtxdginducedm1lem2  29521  dfpth2  29709  pthdlem2  29748  wpthswwlks2on  29944  0ewlk  30096  0pth  30107  konigsbergiedgw  30230  konigsberglem1  30234  konigsberglem2  30235  konigsberglem3  30236  konigsberglem4  30237  konigsberglem5  30238  ex-dif  30405  ex-un  30406  ex-in  30407  ex-fl  30429  avril1  30445  9p10ne21fool  30453  n0lplig  30465  cnidOLD  30564  cnnvm  30664  ipasslem8  30819  ipasslem10  30821  hvsubf  30997  normlem1  31092  normlem6  31097  normlem7  31098  norm-ii-i  31119  norm3adifii  31130  hilid  31143  hlimf  31219  hhssabloi  31244  hhssnv  31246  hhshsslem1  31249  shincli  31344  shsval2i  31369  shs0i  31431  chj0i  31437  chm1i  31438  chincli  31442  chdmm1i  31459  shjshsi  31474  chsup0  31530  h1de2bi  31536  spansnpji  31560  cmcmlem  31573  cmcmii  31579  cmcm2ii  31580  cmcm3ii  31581  pjidmi  31655  pjssmii  31663  pj0i  31675  pjocini  31680  mayetes3i  31711  df0op2  31734  hoaddcomi  31754  hoaddassi  31758  hocadddiri  31761  hocsubdiri  31762  hoaddridi  31768  ho0coi  31770  hoid1i  31771  hoid1ri  31772  hodseqi  31776  honegsubi  31778  adj1o  31876  hoddii  31971  lnopunilem1  31992  lnopunilem2  31993  nmcopexi  32009  nmcopex  32011  nmcoplb  32012  nmcfnexi  32033  nmcfnex  32035  nmcfnlb  32036  adjbd1o  32067  adjcoi  32082  nmopcoadji  32083  opsqrlem6  32127  pjsdii  32137  pjddii  32138  pjidmcoi  32159  pjtoi  32161  pjin1i  32174  pjclem1  32177  stji1i  32224  reuxfrdf  32472  iuninc  32542  fnresin  32609  rinvf1o  32614  suppss2f  32622  xppreima  32629  ofoprabco  32648  partfun2  32661  fressupp  32673  supppreima  32676  fsupprnfi  32677  gtiso  32686  df1stres  32689  df2ndres  32690  snct  32699  padct  32705  fsuppcurry1  32711  fsuppcurry2  32712  ffsrn  32715  fpwrelmapffs  32721  fzodif1  32779  nnindf  32807  nn0min  32808  dp2lt  32872  dp2ltsuc  32873  dp2ltc  32874  dplti  32892  dpmul  32900  dpmul4  32901  ressplusf  32951  xrsclat  32999  xrge00  33002  xrnarchi  33160  elrgspnlem2  33217  1fldgenq  33295  xrge0slmod  33320  zringfrac  33526  esplyind  33613  ply1degltdimlem  33656  ccfldsrarelvec  33705  ccfldextdgrr  33706  locfinreflem  33874  locfinref  33875  unicls  33937  sqsscirc1  33942  mhmhmeotmd  33961  raddcn  33963  xrge0iifiso  33969  xrge0iifhmeo  33970  lmxrge0  33986  cnzh  34002  rezh  34003  qqh0  34018  qqh1  34019  qqhre  34054  rrhre  34055  esumnul  34082  esum0  34083  esumsnf  34098  esumpfinvallem  34108  esumpfinvalf  34110  esumpcvgval  34112  esumcvgsum  34122  esumsup  34123  esumcvgre  34125  sigaclfu2  34155  dmsigagen  34178  ddemeas  34270  mbfmvolf  34300  br2base  34303  omssubadd  34334  sibfof  34374  sitg0  34380  eulerpartlemt  34405  eulerpartgbij  34406  0rrv  34485  coinfliplem  34513  coinflipprob  34514  coinfliprv  34517  ballotlem2  34523  ballotlem4  34533  ballotlem5  34534  ballotlemi1  34537  ballotlem7  34570  ballotth  34572  signsplypnf  34584  signsply0  34585  signsw0g  34590  signswch  34595  signsvf0  34614  hashreprin  34654  reprfz1  34658  chtvalz  34663  hgt750lemd  34682  hgt750lem  34685  hgt750lem2  34686  bnj1098  34816  bnj1109  34819  bnj1131  34820  bnj1533  34885  bnj151  34910  bnj580  34946  bnj852  34954  bnj864  34955  bnj865  34956  bnj978  34982  bnj1021  34999  bnj907  35000  bnj1093  35013  bnj1145  35026  bnj1172  35034  bnj1174  35036  bnj1176  35038  bnj1186  35040  nfan1c  35106  tz9.1regs  35151  fineqvac  35160  onvf1odlem4  35171  onvf1od  35172  subfacf  35240  subfacp1lem1  35244  subfacp1lem5  35249  subfacp1lem6  35250  subfacval3  35254  erdszelem2  35257  kur14lem4  35274  ioosconn  35312  iccllysconn  35315  satfn  35420  fmlaomn0  35455  gonan0  35457  goaln0  35458  elnanelprv  35494  msrfo  35611  mthmpps  35647  problem5  35734  quad3  35735  circum  35739  antnestALT  35759  axextprim  35766  axrepprim  35767  axunprim  35768  axinfprim  35771  axacprim  35772  bcneg1  35801  dfon2lem2  35847  dfon2lem4  35849  axextdfeq  35860  fobigcup  35963  snelsingles  35985  fullfunfnv  36011  fullfunfv  36012  rankaltopb  36044  rank0  36235  rankeq1o  36236  hfuni  36249  in-ax8  36289  fneer  36418  neibastop1  36424  nabi1i  36459  nabi2i  36460  limsucncmpi  36510  knoppcnlem8  36565  knoppcnlem11  36568  cnndvlem1  36602  bj-consensusALT  36644  bj-sbidmOLD  36915  bj-n0i  37016  bj-snsetex  37028  bj-tagss  37045  bj-2upln0  37088  bj-2upln1upl  37089  bj-nuliota  37122  bj-0int  37166  bj-elid5  37234  bj-inftyexpitaufo  37267  bj-pinftyccb  37286  bj-minftyccb  37290  bj-pinftynminfty  37292  bj-isrvec  37359  iccioo01  37392  f1omptsnlem  37401  mptsnunlem  37403  topdifinffinlem  37412  relowlpssretop  37429  1oequni2o  37433  pibt2  37482  imadifss  37655  tan2h  37672  poimirlem3  37683  poimirlem9  37689  poimirlem16  37696  poimirlem17  37697  poimirlem18  37698  poimirlem19  37699  poimirlem20  37700  poimirlem22  37702  poimirlem30  37710  mblfinlem1  37717  mblfinlem2  37718  ovoliunnfl  37722  voliunnfl  37724  itg2addnclem  37731  itg2addnclem2  37732  asindmre  37763  areacirclem1  37768  fdc  37805  cntotbnd  37856  heiborlem6  37876  rrnval  37887  reheibor  37899  rngosn3  37984  brcnvrabga  38394  cnvresrn  38400  moantr  38416  inxp2  38419  dfxrn2  38429  dfsucmap3  38496  dfpre4  38513  cnvcosseq  38559  refrelcosslem  38584  1cosscnvxrn  38597  redundss3  38744  refrelsredund3  38750  refrelredund3  38753  eqvrel0  38904  eqvrelid  38907  prter2  39000  renegclALT  39082  mapdunirnN  41769  lcmeprodgcdi  42120  3factsumint2  42135  3factsumint3  42136  3factsumint4  42137  3factsumint  42138  lcmineqlem4  42145  3lexlogpow5ineq1  42167  3lexlogpow2ineq1  42171  dvrelogpow2b  42181  aks4d1p1p4  42184  aks4d1p8  42200  aks6d1c1  42229  aks6d1c2p2  42232  aks6d1c4  42237  2ap1caineq  42258  sticksstones1  42259  sticksstones2  42260  aks6d1c7lem2  42294  aks5lem3a  42302  aks5lem6  42305  unitscyglem2  42309  unitscyglem3  42310  sqdeccom12  42407  readvrec2  42479  readvcot  42482  resubf  42499  sn-0ne2  42524  sn-subf  42547  sn-nnne0  42578  sn-0lt1  42593  reneg1lt0  42598  rntrclfvOAI  42808  diophrw  42876  rabren3dioph  42932  pellexlem6  42951  pellex  42952  frmx  43030  frmy  43031  jm2.23  43113  jm2.27dlem3  43128  axac10  43150  pw2f1ocnv  43154  kelac2lem  43181  lmhmlnmsplit  43204  pwfi2f1o  43213  frlmpwfi  43215  insucid  43520  nla0003  43542  ifpbiidcor  43591  sucomisnotcard  43661  alephiso2  43675  alephiso3  43676  cnvnonrel  43705  rnnonrel  43708  resnonrel  43709  cononrel1  43711  cononrel2  43712  fvnonrel  43714  cnvcnvintabd  43717  cnvintabd  43720  rclexi  43732  rtrclex  43734  clcnvlem  43740  cnvrcl0  43742  dmtrcl  43744  rntrcl  43745  dfrtrcl5  43746  iunrelexp0  43819  dmtrclfvRP  43847  rntrclfv  43849  corcltrcl  43856  cotrclrcl  43859  0heALT  43900  frege54cor1a  43981  uneqsn  44142  clsk3nimkb  44157  int-sqdefd  44298  int-sqgeq0d  44303  rr-groth  44416  rr-grothprim  44417  rr-grothshort  44421  seff  44426  expgrowthi  44450  expgrowth  44452  binomcxplemnotnn0  44473  ee233  44636  ax6e2nd  44675  in1  44688  dfvd2ani  44700  dfvd2i  44702  dfvd3i  44709  dfvd3ani  44712  e0bi  44892  uun2221  44929  uun2221p1  44930  uun2221p2  44931  en3lpVD  44961  relopabVD  45017  ax6e2ndVD  45024  ax6e2ndALT  45046  permaxpow  45126  pssnssi  45222  nnf1oxpnn  45316  icof  45340  fnmptif  45386  rn1st  45394  negpilt0  45406  xrgtso  45468  supxrleubrnmptf  45573  xrpnf  45607  rexanuz2nf  45614  ioontr  45635  iccdifioo  45639  iccdifprioo  45640  uzinico2  45685  fsummulc1f  45695  fsumiunss  45699  fnlimfvre2  45799  limsupreuz  45859  limsup10ex  45895  icccncfext  46009  dvcosre  46034  dvsinax  46035  ioodvbdlimc1lem2  46054  ioodvbdlimc2lem  46056  dvmptmulf  46059  dvnmul  46065  dvmptfprodlem  46066  dvnprodlem2  46069  stoweidlem1  46123  stoweidlem26  46148  stoweidlem34  46156  stoweidlem44  46166  stoweid  46185  stirlinglem5  46200  dirkercncflem1  46225  fourierdlem44  46273  fourierdlem56  46284  fourierdlem62  46290  fourierdlem89  46317  fourierdlem91  46319  fourierdlem100  46328  fourierdlem102  46330  fourierdlem103  46331  fourierdlem104  46332  fourierdlem108  46336  fourierdlem112  46340  fourierdlem114  46342  fouriersw  46353  rrndistlt  46412  gsumge0cl  46493  sge0tsms  46502  sge0ltfirpmpt2  46548  ovn0  46688  hoidmv1le  46716  hoidmvle  46722  ovnsubadd2lem  46767  ovolval4lem1  46771  vonioolem2  46803  smflimlem3  46895  nsssmfmbf  46901  chnerlem1  47004  nthrucw  47008  sinnpoly  47015  axorbtnotaiffb  47027  axorbciffatcxorb  47029  abnotbtaxb  47039  euabsneu  47152  ceilhalf1  47458  sprval  47603  fmtnoinf  47660  1nevenALTV  47815  nfermltl8rev  47866  nfermltl2rev  47867  nnsum3primes4  47912  tgblthelfgott  47939  tgoldbachlt  47940  cycl3grtri  48071  isubgr3stgrlem3  48092  usgrexmpl1lem  48145  usgrexmpl2lem  48150  usgrexmpl2trifr  48161  gpgprismgr4cycllem7  48225  ldepslinc  48634  ackval42  48821  rrx2plordso  48849  vsn  48936  dmtposss  49000  sepfsepc  49052  basresposfo  49102  rescofuf  49218  oppff1  49273  idfth  49283  idsubc  49285  fuco2eld2  49439  fuco22a  49475  setc1onsubc  49727  alimp-no-surprise  49906  aacllem  49926  amgmwlem  49927  amgmlemALT  49928