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  1427  cadan  1611  nic-dfim  1671  nic-dfneg  1672  nic-mp  1673  nic-mpALT  1674  tbw-negdf  1701  rb-imdf  1752  nfri  1791  mpgbi  1800  19.35i  1880  nfim1  2207  19.36i  2239  ax6  2388  sbie  2506  datisi  2680  disamis  2681  dimatis  2688  fresison  2689  bamalip  2692  axi12  2706  eqcomi  2745  eqtri  2759  eleqtri  2834  nfnfc  2911  neii  2934  necomi  2986  neeqtri  3004  neli  3038  nrex  3065  rexlimi  3237  eueqi  3655  euxfr2w  3666  euxfr2  3668  reuxfrd  3694  cdeqri  3712  sseqtri  3970  pssn2lp  4044  equncomi  4100  unssi  4131  ssini  4180  unabs  4205  inabs  4206  dfin4  4218  vn0  4285  inindif  4315  difidALT  4317  ab0orv  4323  ab0orvALT  4324  disjdif  4412  difin0  4414  pwundif  4565  snid  4606  rabrsn  4668  iinrab2  5012  symdifv  5028  rintn0  5051  breqtri  5110  axsepgfromrep  5229  bm1.3iiOLD  5237  ax6vsep  5238  notzfaus  5305  zfpow  5308  dtruALT2  5312  dtruALT  5330  reusv2lem4  5343  dtru  5389  elOLD  5391  op1stb  5424  copsexgw  5443  copsexgwOLD  5444  copsexg  5445  uniop  5469  rn0  5881  dmresi  6017  somincom  6097  cnvimassrndm  6116  cnvcnv  6156  elid  6163  rescnvcnv  6168  cnvcnvres  6169  cocnvcnv2  6223  cores2  6224  co01  6226  cnviin  6250  predres  6303  iota4an  6480  fnopab  6636  mpt0  6640  fnmpti  6641  f1cnvcnv  6745  f1ovi  6820  eliman0  6877  fvco4i  6941  cnvimainrn  7019  fmpti  7064  funiunfv  7203  oprabss  7475  relmptopab  7617  zfun  7690  tfinds2  7815  omon  7829  2nd0  7949  f1stres  7966  f2ndres  7967  cnvoprab  8013  relmpoopab  8044  df1st2  8048  df2nd2  8049  fsplit  8067  frpoins3xpg  8090  frpoins3xp3g  8091  poxp2  8093  poseq  8108  reldmtpos  8184  dftpos4  8195  tpostpos  8196  tpos0  8206  frrlem4  8239  smo0  8298  tfrlem14  8330  tfrlem16  8332  rdgsucg  8362  rdglimg  8364  frfnom  8374  oawordeulem  8489  uniixp  8869  dfdom2  8925  ssdomg  8947  xpcomf1o  9004  sbthlem5  9029  sdom0  9047  limensuci  9091  1sdom2  9158  fiint  9237  fidomdm  9244  residfi  9248  mptfi  9261  fisn  9340  dffi3  9344  ordtypelem6  9438  ordtypelem7  9439  wemaplem2  9462  harwdom  9506  nelaneqOLD  9517  suc11reg  9540  zfinf  9560  axinf2  9561  noinfep  9581  cantnfvalf  9586  cantnflt  9593  cantnf0  9596  cantnf  9614  ttrclco  9639  tz9.1c  9651  tc2  9661  setinds  9670  r111  9699  r1tr2  9701  r1ordg  9702  r1sssuc  9707  r1val1  9710  tz9.13  9715  r1elssi  9729  pwwf  9731  rankopb  9776  rankeq0b  9784  ranksuc  9789  rankmapu  9802  rankxplim3  9805  rankxpsuc  9806  cp  9815  karden  9819  card0  9882  cardlim  9896  cardom  9910  infxpenlem  9935  alephsuc2  10002  alephgeom  10004  unialeph  10023  dfac4  10044  dfacacn  10064  dju1dif  10095  dju1p1e2  10096  infdju1  10112  ackbij1lem13  10153  ackbij2  10164  cf0  10173  cfsuc  10179  cfom  10186  cfslb2n  10190  ominf4  10234  fin23lem17  10260  fin23lem28  10262  fin23lem30  10264  fin23lem31  10265  fin23lem40  10273  isfin1-3  10308  dfacfin7  10321  fin1a2lem6  10327  itunitc1  10342  axcc3  10360  dcomex  10369  axdc2lem  10370  axcclem  10379  zfac  10382  ac3  10384  ackm  10387  axac2  10388  axac  10389  axaci  10390  cardeqv  10391  numth2  10393  numth  10394  dmct  10446  brdom3  10450  fin71ac  10455  cardf  10472  aleph1  10494  cfpwsdom  10507  smobeth  10509  zfcndrep  10537  zfcndpow  10539  zfcndac  10542  gch2  10598  wunex3  10664  tskpr  10693  inar1  10698  rankcf  10700  tskcard  10704  tskuni  10706  grothpw  10749  axgroth4  10755  grothprim  10757  inaprc  10759  dmaddpi  10813  dmmulpi  10814  1lt2pi  10828  addpqf  10867  mulpqf  10869  1lt2nq  10896  supsrlem  11034  ssxr  11215  gtso  11227  subf  11395  negne0i  11469  mulnzcnf  11796  infrenegsup  12139  neg1lt0  12147  nnne0  12211  halflt1  12394  nn0ssz  12547  3halfnz  12608  zeo  12615  numlt  12669  numltc  12670  le9lt10  12671  decle  12678  uzf  12791  xaddf  13176  xsubge0  13213  xmulf  13224  ixxf  13308  ixxssxr  13310  iooval2  13331  ioof  13400  unirnioo  13402  dfioo2  13403  fzval2  13464  fzf  13465  0nelfz1  13497  fz10  13499  fzpreddisj  13527  4fvwrd4  13602  fzof  13610  fzo0  13638  fldiv4p1lem1div2  13794  fldiv4lem1div2  13796  om2uzoi  13917  faclbnd4lem1  14255  hashkf  14294  hashgval  14295  hashinf  14297  hashresfn  14302  hashnn0n0nn  14353  hashge3el3dif  14449  hash3tpde  14455  rev0  14726  s2dm  14852  f1oun2prg  14879  trclublem  14957  sqrt2gt1lt2  15236  limsupgord  15434  fclim  15515  fsumrelem  15770  ackbijnn  15793  incexclem  15801  incexc  15802  arisum2  15826  georeclim  15837  geoisumr  15843  0.999...  15846  risefall0lem  15991  ege2le3  16055  sin0  16116  ef01bndlem  16151  cos2bnd  16155  cos01gt0  16158  sincos2sgn  16161  sin4lt0  16162  rpnnen2lem3  16183  rpnnen2lem9  16189  rexpen  16195  cnso  16214  dvdslelem  16278  divalglem1  16363  divalglem5  16366  divalglem6  16367  divalglem10  16371  flodddiv4  16384  0bits  16408  sadcf  16422  sadcadd  16427  bitsshft  16444  smupf  16447  gcdf  16481  eucalgf  16552  2prm  16661  dfphi2  16744  pockthi  16878  prmrec  16893  vdwapf  16943  vdwlem6  16957  karatsuba  17054  1259lem5  17105  2503lem3  17109  4001lem4  17114  structcnvcnv  17123  structfn  17126  strleun  17127  imasvscafn  17501  xpsff1o  17531  xrge0base  17571  wunnat  17926  dfinito3  17972  dftermo3  17973  eldmcoa  18032  coapm  18038  catcfuccl  18085  catcxpccl  18173  yonedainv  18247  chnub  18588  smndex1bas  18877  smndex1n0mnd  18883  grpinvfvi  18958  mulgfvi  19049  ressmulgnnd  19054  symgsssg  19442  symgfisg  19443  psgnunilem5  19469  sylow3lem2  19603  oppglsm  19617  efgmf  19688  efgval  19692  efgsf  19704  0frgp  19754  dmdprd  19975  dprdval  19980  invrfval  20369  drngui  20712  rmodislmod  20925  lssintcl  20959  cnfldadd  21358  cnfldmul  21360  cnfldfunALT  21367  cnfld0  21376  cnfld1  21377  cnfldsub  21380  xrsds  21390  pzriprnglem4  21464  pzriprnglem9  21469  pzriprnglem14  21474  psgnghm  21560  zrhpsgnmhm  21564  ocv1  21659  dsmmbas2  21717  mplsubrglem  21982  opsrtoslem2  22034  evl1maprhm  22344  mdetralt  22573  maducoeval2  22605  eltpsi  22909  unitg  22932  fctop  22969  cctop  22971  ppttop  22972  epttop  22974  leordtvallem1  23175  leordtvallem2  23176  iccordt  23179  iscnp2  23204  discmp  23363  conncompcld  23399  1stcrestlem  23417  2ndcdisj  23421  topnlly  23456  disllycmp  23463  dis1stc  23464  txuni2  23530  xkotf  23550  dfac14lem  23582  prdstps  23594  txindis  23599  tx1stc  23615  xkohaus  23618  xkoptsub  23619  cnmpt1st  23633  cnmpt2nd  23634  ptcmpfi  23778  trfil1  23851  fin1aufil  23897  tgpconncompeqg  24077  tgpconncomp  24078  trust  24194  met1stc  24486  dscmet  24537  retopon  24728  cnfldtopon  24747  xrsxmet  24775  xrsmopn  24778  iimulcn  24905  icopnfhmeo  24910  iccpnfhmeo  24912  xrhmeo  24913  cnheiborlem  24921  lebnumii  24933  ishtpy  24939  htpycc  24947  pco1  24982  pcohtpylem  24986  pcopt  24989  pcopt2  24990  pcoass  24991  pcorevlem  24993  rrxcph  25359  rrx0el  25365  ovoliunlem3  25471  ovolicc1  25483  ovolicc2  25489  volf  25496  ioorf  25540  dyadf  25558  dyadmbl  25567  vitalilem5  25579  vitali  25580  mbfimaopnlem  25622  mbflimsup  25633  0plef  25639  i1fima  25645  i1fima2  25646  i1fd  25648  itg1ge0  25653  itg10  25655  i1f1lem  25656  i1fadd  25662  i1fmul  25663  i1fmulc  25670  mbfi1fseqlem5  25686  itg2addlem  25725  reldv  25837  dvbsss  25869  dvef  25947  lhop1lem  25980  deg1fvi  26050  plypf1  26177  coeeulem  26189  coeeu  26190  vieta1lem2  26277  aannenlem3  26296  aalioulem3  26300  dvradcnv  26386  pserulm  26387  pserdvlem2  26393  sinhalfpilem  26427  sincos4thpi  26477  tan4thpiOLD  26479  sincos6thpi  26480  pige3ALT  26484  resinf1o  26500  tanord1  26501  tanregt0  26503  efabl  26514  relogrn  26525  dfrelog  26529  logi  26551  logneg  26552  logltb  26564  logcn  26611  logf1o2  26614  dvlog  26615  efopnlem2  26621  efopn  26622  logccv  26627  dvsqrt  26706  dvcnsqrt  26708  cxpcn3  26712  logblog  26756  angpined  26794  1cubr  26806  asinsin  26856  asin1  26858  reasinsin  26860  atan0  26872  atanbnd  26890  atan1  26892  log2cnv  26908  log2ub  26913  log2le1  26914  birthday  26918  amgmlem  26953  emcllem5  26963  emgt0  26970  harmonicbnd3  26971  ftalem3  27038  basellem4  27047  sgmf  27108  ppi1  27127  cht1  27128  vma1  27129  ppiltx  27140  sqff1o  27145  ppiublem1  27165  ppiublem2  27166  ppiub  27167  chtub  27175  dchreq  27221  bposlem7  27253  bposlem8  27254  bposlem9  27255  lgsdir2lem2  27289  lgsdir2lem3  27290  chebbnd1  27435  chto1ub  27439  chpo1ubb  27444  pntibndlem1  27552  nosgnn0  27622  ltssolem1  27639  bdayfo  27641  nolt02o  27659  nogt01o  27660  noetasuplem4  27700  noetainflem4  27704  cutbdaybnd2lim  27789  madeun  27876  cutsfo  27897  addsproplem2  27962  addsproplem7  27967  addsprop  27968  negsprop  28027  subsf  28056  mulsproplem13  28120  mulsproplem14  28121  mulsprop  28122  oniso  28263  n0cut  28326  bdayn0sf1o  28362  twocut  28415  bdaypw2n0bndlem  28455  bdayfinbndlem1  28459  0reno  28488  tgldimor  28570  tglnfn  28615  axlowdimlem4  29014  axlowdimlem16  29026  axlowdim  29030  upgrfi  29160  lfgrnloop  29194  lfuhgr1v0e  29323  usgrexmplef  29328  usgrres  29377  vdegp1bi  29606  vtxdginducedm1lem2  29609  dfpth2  29797  pthdlem2  29836  wpthswwlks2on  30032  0ewlk  30184  0pth  30195  konigsbergiedgw  30318  konigsberglem1  30322  konigsberglem2  30323  konigsberglem3  30324  konigsberglem4  30325  konigsberglem5  30326  ex-dif  30493  ex-un  30494  ex-in  30495  ex-fl  30517  avril1  30533  9p10ne21fool  30541  n0lplig  30554  cnidOLD  30653  cnnvm  30753  ipasslem8  30908  ipasslem10  30910  hvsubf  31086  normlem1  31181  normlem6  31186  normlem7  31187  norm-ii-i  31208  norm3adifii  31219  hilid  31232  hlimf  31308  hhssabloi  31333  hhssnv  31335  hhshsslem1  31338  shincli  31433  shsval2i  31458  shs0i  31520  chj0i  31526  chm1i  31527  chincli  31531  chdmm1i  31548  shjshsi  31563  chsup0  31619  h1de2bi  31625  spansnpji  31649  cmcmlem  31662  cmcmii  31668  cmcm2ii  31669  cmcm3ii  31670  pjidmi  31744  pjssmii  31752  pj0i  31764  pjocini  31769  mayetes3i  31800  df0op2  31823  hoaddcomi  31843  hoaddassi  31847  hocadddiri  31850  hocsubdiri  31851  hoaddridi  31857  ho0coi  31859  hoid1i  31860  hoid1ri  31861  hodseqi  31865  honegsubi  31867  adj1o  31965  hoddii  32060  lnopunilem1  32081  lnopunilem2  32082  nmcopexi  32098  nmcopex  32100  nmcoplb  32101  nmcfnexi  32122  nmcfnex  32124  nmcfnlb  32125  adjbd1o  32156  adjcoi  32171  nmopcoadji  32172  opsqrlem6  32216  pjsdii  32226  pjddii  32227  pjidmcoi  32248  pjtoi  32250  pjin1i  32263  pjclem1  32266  stji1i  32313  reuxfrdf  32560  iuninc  32630  fnresin  32697  rinvf1o  32703  suppss2f  32711  xppreima  32718  ofoprabco  32737  partfun2  32749  fressupp  32761  supppreima  32764  fsupprnfi  32765  gtiso  32774  df1stres  32777  df2ndres  32778  snct  32785  padct  32791  fsuppcurry1  32797  fsuppcurry2  32798  ffsrn  32801  fpwrelmapffs  32807  fzodif1  32865  nnindf  32893  nn0min  32894  dp2lt  32944  dp2ltsuc  32945  dp2ltc  32946  dplti  32964  dpmul  32972  dpmul4  32973  ressplusf  33023  xrsclat  33071  xrge00  33074  xrnarchi  33245  elrgspnlem2  33304  1fldgenq  33383  xrge0slmod  33408  zringfrac  33614  esplyind  33719  ply1degltdimlem  33766  ccfldsrarelvec  33815  ccfldextdgrr  33816  locfinreflem  33984  locfinref  33985  unicls  34047  sqsscirc1  34052  mhmhmeotmd  34071  raddcn  34073  xrge0iifiso  34079  xrge0iifhmeo  34080  lmxrge0  34096  cnzh  34112  rezh  34113  qqh0  34128  qqh1  34129  qqhre  34164  rrhre  34165  esumnul  34192  esum0  34193  esumsnf  34208  esumpfinvallem  34218  esumpfinvalf  34220  esumpcvgval  34222  esumcvgsum  34232  esumsup  34233  esumcvgre  34235  sigaclfu2  34265  dmsigagen  34288  ddemeas  34380  mbfmvolf  34410  br2base  34413  omssubadd  34444  sibfof  34484  sitg0  34490  eulerpartlemt  34515  eulerpartgbij  34516  0rrv  34595  coinfliplem  34623  coinflipprob  34624  coinfliprv  34627  ballotlem2  34633  ballotlem4  34643  ballotlem5  34644  ballotlemi1  34647  ballotlem7  34680  ballotth  34682  signsplypnf  34694  signsply0  34695  signsw0g  34700  signswch  34705  signsvf0  34724  hashreprin  34764  reprfz1  34768  chtvalz  34773  hgt750lemd  34792  hgt750lem  34795  hgt750lem2  34796  bnj1098  34926  bnj1109  34929  bnj1131  34930  bnj1533  34994  bnj151  35019  bnj580  35055  bnj852  35063  bnj864  35064  bnj865  35065  bnj978  35091  bnj1021  35108  bnj907  35109  bnj1093  35122  bnj1145  35135  bnj1172  35143  bnj1174  35145  bnj1176  35147  bnj1186  35149  nfan1c  35215  xoromon  35232  fineqvac  35260  tz9.1regs  35278  onvf1odlem4  35288  onvf1od  35289  subfacf  35357  subfacp1lem1  35361  subfacp1lem5  35366  subfacp1lem6  35367  subfacval3  35371  erdszelem2  35374  kur14lem4  35391  ioosconn  35429  iccllysconn  35432  satfn  35537  fmlaomn0  35572  gonan0  35574  goaln0  35575  elnanelprv  35611  msrfo  35728  mthmpps  35764  problem5  35851  quad3  35852  circum  35856  antnestALT  35876  axextprim  35883  axrepprim  35884  axunprim  35885  axinfprim  35888  axacprim  35889  bcneg1  35918  dfon2lem2  35964  dfon2lem4  35966  axextdfeq  35977  fobigcup  36080  snelsingles  36102  fullfunfnv  36128  fullfunfv  36129  rankaltopb  36161  rank0  36352  rankeq1o  36353  hfuni  36366  in-ax8  36406  fneer  36535  neibastop1  36541  nabi1i  36576  nabi2i  36577  limsucncmpi  36627  tz9.1ctco  36664  ttctr3  36677  ttcpwss  36697  knoppcnlem8  36760  knoppcnlem11  36763  cnndvlem1  36797  bj-consensusALT  36844  bj-sbidmOLD  37157  bj-n0i  37258  bj-snsetex  37270  bj-tagss  37287  bj-2upln0  37330  bj-2upln1upl  37331  bj-nuliota  37364  bj-axseprep  37381  bj-0int  37413  bj-elid5  37483  bj-inftyexpitaufo  37516  bj-pinftyccb  37535  bj-minftyccb  37539  bj-pinftynminfty  37541  bj-isrvec  37608  iccioo01  37643  f1omptsnlem  37652  mptsnunlem  37654  topdifinffinlem  37663  relowlpssretop  37680  1oequni2o  37684  pibt2  37733  imadifss  37916  tan2h  37933  poimirlem3  37944  poimirlem9  37950  poimirlem16  37957  poimirlem17  37958  poimirlem18  37959  poimirlem19  37960  poimirlem20  37961  poimirlem22  37963  poimirlem30  37971  mblfinlem1  37978  mblfinlem2  37979  ovoliunnfl  37983  voliunnfl  37985  itg2addnclem  37992  itg2addnclem2  37993  asindmre  38024  areacirclem1  38029  fdc  38066  cntotbnd  38117  heiborlem6  38137  rrnval  38148  reheibor  38160  rngosn3  38245  brcnvrabga  38663  cnvresrn  38669  moantr  38693  inxp2  38696  dfxrn2  38706  dfsucmap3  38784  dfpre4  38801  cnvcosseq  38848  refrelcosslem  38873  1cosscnvxrn  38886  redundss3  39033  refrelsredund3  39039  refrelredund3  39042  disjimeceqim  39125  eqvrel0  39210  eqvrelid  39213  prter2  39327  renegclALT  39409  mapdunirnN  42096  lcmeprodgcdi  42446  3factsumint2  42461  3factsumint3  42462  3factsumint4  42463  3factsumint  42464  lcmineqlem4  42471  3lexlogpow5ineq1  42493  3lexlogpow2ineq1  42497  dvrelogpow2b  42507  aks4d1p1p4  42510  aks4d1p8  42526  aks6d1c1  42555  aks6d1c2p2  42558  aks6d1c4  42563  2ap1caineq  42584  sticksstones1  42585  sticksstones2  42586  aks6d1c7lem2  42620  aks5lem3a  42628  aks5lem6  42631  unitscyglem2  42635  unitscyglem3  42636  sqdeccom12  42721  readvrec2  42793  readvcot  42796  resubf  42813  sn-0ne2  42838  sn-subf  42861  sn-nnne0  42905  sn-0lt1  42920  reneg1lt0  42925  rntrclfvOAI  43123  diophrw  43191  rabren3dioph  43243  pellexlem6  43262  pellex  43263  frmx  43341  frmy  43342  jm2.23  43424  jm2.27dlem3  43439  axac10  43461  pw2f1ocnv  43465  kelac2lem  43492  lmhmlnmsplit  43515  pwfi2f1o  43524  frlmpwfi  43526  insucid  43831  nla0003  43852  ifpbiidcor  43901  sucomisnotcard  43971  alephiso2  43985  alephiso3  43986  cnvnonrel  44015  rnnonrel  44018  resnonrel  44019  cononrel1  44021  cononrel2  44022  fvnonrel  44024  cnvcnvintabd  44027  cnvintabd  44030  rclexi  44042  rtrclex  44044  clcnvlem  44050  cnvrcl0  44052  dmtrcl  44054  rntrcl  44055  dfrtrcl5  44056  iunrelexp0  44129  dmtrclfvRP  44157  rntrclfv  44159  corcltrcl  44166  cotrclrcl  44169  0heALT  44210  frege54cor1a  44291  uneqsn  44452  clsk3nimkb  44467  int-sqdefd  44608  int-sqgeq0d  44613  rr-groth  44726  rr-grothprim  44727  rr-grothshort  44731  seff  44736  expgrowthi  44760  expgrowth  44762  binomcxplemnotnn0  44783  ee233  44946  ax6e2nd  44985  in1  44998  dfvd2ani  45010  dfvd2i  45012  dfvd3i  45019  dfvd3ani  45022  e0bi  45202  uun2221  45239  uun2221p1  45240  uun2221p2  45241  en3lpVD  45271  relopabVD  45327  ax6e2ndVD  45334  ax6e2ndALT  45356  permaxpow  45436  pssnssi  45531  nnf1oxpnn  45625  icof  45648  fnmptif  45694  rn1st  45702  negpilt0  45714  xrgtso  45775  supxrleubrnmptf  45879  xrpnf  45913  rexanuz2nf  45920  ioontr  45941  iccdifioo  45945  iccdifprioo  45946  uzinico2  45991  fsummulc1f  46001  fsumiunss  46005  fnlimfvre2  46105  limsupreuz  46165  limsup10ex  46201  icccncfext  46315  dvcosre  46340  dvsinax  46341  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  dvmptmulf  46365  dvnmul  46371  dvmptfprodlem  46372  dvnprodlem2  46375  stoweidlem1  46429  stoweidlem26  46454  stoweidlem34  46462  stoweidlem44  46472  stoweid  46491  stirlinglem5  46506  dirkercncflem1  46531  fourierdlem44  46579  fourierdlem56  46590  fourierdlem62  46596  fourierdlem89  46623  fourierdlem91  46625  fourierdlem100  46634  fourierdlem102  46636  fourierdlem103  46637  fourierdlem104  46638  fourierdlem108  46642  fourierdlem112  46646  fourierdlem114  46648  fouriersw  46659  rrndistlt  46718  gsumge0cl  46799  sge0tsms  46808  sge0ltfirpmpt2  46854  ovn0  46994  hoidmv1le  47022  hoidmvle  47028  ovnsubadd2lem  47073  ovolval4lem1  47077  vonioolem2  47109  smflimlem3  47201  nsssmfmbf  47207  chnerlem1  47312  nthrucw  47316  goldrasin  47330  goldrapos  47331  sinnpoly  47339  axorbtnotaiffb  47351  axorbciffatcxorb  47353  abnotbtaxb  47363  euabsneu  47476  ceilhalf1  47786  sprval  47939  fmtnoinf  47999  nprmdvdsfacm1lem2  48084  ppivalnnnprmge6  48089  ppivalnn4  48090  ppivalnn  48095  1nevenALTV  48167  nfermltl8rev  48218  nfermltl2rev  48219  nnsum3primes4  48264  tgblthelfgott  48291  tgoldbachlt  48292  cycl3grtri  48423  isubgr3stgrlem3  48444  usgrexmpl1lem  48497  usgrexmpl2lem  48502  usgrexmpl2trifr  48513  gpgprismgr4cycllem7  48577  ldepslinc  48985  ackval42  49172  rrx2plordso  49200  vsn  49287  dmtposss  49351  sepfsepc  49403  basresposfo  49453  rescofuf  49568  oppff1  49623  idfth  49633  idsubc  49635  fuco2eld2  49789  fuco22a  49825  setc1onsubc  50077  alimp-no-surprise  50256  aacllem  50276  amgmwlem  50277  amgmlemALT  50278