Theorem mpbi 232

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

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  pm5.74i  273  notbii  322  biluk  388  pm5.19  389  pm3.24  406  dfbi  479  pm4.71i  567  pm5.32i  582  biadani  829  biadanii  831  imori  865  ori  872  pm5.16  1026  dn1  1068  3ori  1442  cadan  1628  nic-dfim  1688  nic-dfneg  1689  nic-mp  1690  nic-mpALT  1691  tbw-negdf  1718  rb-imdf  1769  nfri  1808  mpgbi  1817  19.35i  1897  nfim1  2233  19.36i  2265  ax6  2414  sbie  2532  datisi  2705  disamis  2706  dimatis  2713  fresison  2714  bamalip  2717  axi12  2731  eqcomi  2770  eqtri  2784  eleqtri  2859  nfnfc  2935  neii  2958  necomi  3010  neeqtri  3028  neli  3062  nrex  3089  rexlimi  3261  eueqi  3671  euxfr2w  3682  euxfr2  3684  reuxfrd  3710  cdeqri  3728  sseqtri  3984  pssn2lp  4058  equncomi  4113  unssi  4143  ssini  4191  unabs  4217  inabs  4218  dfin4  4230  vn0  4297  inindif  4327  difidALT  4329  ab0orv  4335  ab0orvALT  4336  disjdif  4425  difin0  4427  pwundif  4579  snid  4620  rabrsn  4682  iinrab2  5026  symdifv  5042  rintn0  5065  breqtri  5124  axsepgfromrep  5243  bm1.3iiOLD  5251  ax6vsep  5252  notzfaus  5319  zfpow  5322  dtruALT2  5326  dtruALT  5344  reusv2lem4  5357  dtru  5403  elOLD  5405  op1stb  5438  copsexgw  5457  copsexgwOLD  5458  copsexg  5459  uniop  5483  rn0  5900  dmresi  6038  somincom  6118  cnvimassrndm  6134  cnvcnv  6174  elid  6182  rescnvcnv  6187  cnvcnvres  6188  cocnvcnv2  6242  cores2  6243  co01  6245  cnviin  6269  predres  6322  iota4an  6499  fnopab  6655  mpt0  6659  fnmpti  6660  f1cnvcnv  6767  f1ovi  6843  eliman0  6900  fvco4i  6965  cnvimainrn  7044  fmpti  7089  funiunfv  7228  oprabss  7500  relmptopab  7642  zfun  7715  tfinds2  7840  omon  7854  2nd0  7973  f1stres  7990  f2ndres  7991  cnvoprab  8037  relmpoopab  8068  df1st2  8072  df2nd2  8073  fsplit  8091  frpoins3xpg  8115  frpoins3xp3g  8116  poxp2  8118  poseq  8133  reldmtpos  8209  dftpos4  8220  tpostpos  8221  tpos0  8231  frrlem4  8265  smo0  8324  tfrlem14  8357  tfrlem16  8359  rdgsucg  8389  rdglimg  8391  frfnom  8401  oawordeulem  8518  uniixp  8899  dfdom2  8955  ssdomg  8977  xpcomf1o  9034  sbthlem5  9059  sdom0  9077  limensuci  9121  1sdom2  9188  fiint  9267  fidomdm  9274  residfi  9278  mptfi  9291  fisn  9370  dffi3  9374  ordtypelem6  9468  ordtypelem7  9469  wemaplem2  9492  harwdom  9536  nelaneqOLD  9548  suc11reg  9571  zfinf  9591  axinf2  9592  noinfep  9612  cantnfvalf  9617  cantnflt  9624  cantnf0  9627  cantnf  9645  ttrclco  9670  tz9.1c  9682  tc2  9692  setinds  9701  r111  9730  r1tr2  9732  r1ordg  9733  r1sssuc  9738  r1val1  9741  tz9.13  9746  r1elssi  9760  pwwf  9762  rankopb  9807  rankeq0b  9815  ranksuc  9820  rankmapu  9833  rankxplim3  9836  rankxpsuc  9837  cp  9846  karden  9850  card0  9913  cardlim  9927  cardom  9941  infxpenlem  9966  alephsuc2  10033  alephgeom  10035  unialeph  10054  dfac4  10075  dfacacn  10095  dju1dif  10126  dju1p1e2  10127  infdju1  10143  ackbij1lem13  10184  ackbij2  10195  cf0  10204  cfsuc  10211  cfom  10218  cfslb2n  10222  ominf4  10266  fin23lem17  10292  fin23lem28  10294  fin23lem30  10296  fin23lem31  10297  fin23lem40  10305  isfin1-3  10340  dfacfin7  10353  fin1a2lem6  10359  itunitc1  10374  axcc3  10392  dcomex  10401  axdc2lem  10402  axcclem  10411  zfac  10414  ac3  10416  ackm  10419  axac2  10420  axac  10421  axaci  10422  cardeqv  10423  numth2  10425  numth  10426  dmct  10478  brdom3  10482  fin71ac  10487  cardf  10504  aleph1  10526  cfpwsdom  10539  smobeth  10541  zfcndrep  10569  zfcndpow  10571  zfcndac  10574  gch2  10630  wunex3  10696  tskpr  10725  inar1  10730  rankcf  10732  tskcard  10736  tskuni  10738  grothpw  10781  axgroth4  10787  grothprim  10789  inaprc  10791  dmaddpi  10845  dmmulpi  10846  1lt2pi  10860  addpqf  10899  mulpqf  10901  1lt2nq  10928  supsrlem  11066  ssxr  11249  gtso  11261  subf  11429  negne0i  11503  mulnzcnf  11830  infrenegsup  12172  neg1lt0  12180  nnne0  12244  halflt1  12435  nn0ssz  12588  3halfnz  12649  zeo  12656  numlt  12715  numltc  12716  le9lt10  12717  decle  12724  uzf  12839  xaddf  13224  xsubge0  13261  xmulf  13272  ixxf  13356  ixxssxr  13358  iooval2  13379  ioof  13448  unirnioo  13450  dfioo2  13451  fzval2  13512  fzf  13513  0nelfz1  13545  fz10  13547  fzpreddisj  13575  4fvwrd4  13650  fzof  13658  fzo0  13686  fldiv4p1lem1div2  13842  fldiv4lem1div2  13844  om2uzoi  13965  faclbnd4lem1  14303  hashkf  14342  hashgval  14343  hashinf  14345  hashresfn  14350  hashnn0n0nn  14401  hashge3el3dif  14497  hash3tpde  14503  rev0  14774  s2dm  14900  f1oun2prg  14927  trclublem  15005  sqrt2gt1lt2  15284  limsupgord  15482  fclim  15563  fsumrelem  15818  ackbijnn  15841  incexclem  15849  incexc  15850  arisum2  15874  georeclim  15885  geoisumr  15891  0.999...  15894  risefall0lem  16039  ege2le3  16103  sin0  16164  ef01bndlem  16199  cos2bnd  16203  cos01gt0  16206  sincos2sgn  16209  sin4lt0  16210  rpnnen2lem3  16231  rpnnen2lem9  16237  rexpen  16243  cnso  16262  dvdslelem  16326  divalglem1  16411  divalglem5  16414  divalglem6  16415  divalglem10  16419  flodddiv4  16432  0bits  16456  sadcf  16470  sadcadd  16475  bitsshft  16492  smupf  16495  gcdf  16529  eucalgf  16600  2prm  16709  dfphi2  16792  pockthi  16926  prmrec  16941  vdwapf  16991  vdwlem6  17005  karatsuba  17102  1259lem5  17154  2503lem3  17158  4001lem4  17163  structcnvcnv  17172  structfn  17175  strleun  17176  imasvscafn  17550  xpsff1o  17580  xrge0base  17620  wunnat  17975  dfinito3  18021  dftermo3  18022  eldmcoa  18081  coapm  18087  catcfuccl  18134  catcxpccl  18222  yonedainv  18296  chnub  18637  smndex1bas  18926  smndex1n0mnd  18932  grpinvfvi  19007  mulgfvi  19098  ressmulgnnd  19103  symgsssg  19490  symgfisg  19491  psgnunilem5  19517  sylow3lem2  19651  oppglsm  19665  efgmf  19736  efgval  19740  efgsf  19752  0frgp  19802  dmdprd  20023  dprdval  20028  invrfval  20417  drngui  20764  rmodislmod  20977  lssintcl  21011  cnfldadd  21410  cnfldmul  21412  cnfldfunALT  21419  cnfld0  21428  cnfld1  21429  cnfldsub  21432  xrsds  21442  pzriprnglem4  21516  pzriprnglem9  21521  pzriprnglem14  21526  psgnghm  21612  zrhpsgnmhm  21616  ocv1  21711  dsmmbas2  21769  mplsubrglem  22035  opsrtoslem2  22089  evl1maprhm  22422  mdetralt  22648  maducoeval2  22680  eltpsi  22984  unitg  23007  fctop  23044  cctop  23046  ppttop  23047  epttop  23049  leordtvallem1  23250  leordtvallem2  23251  iccordt  23254  iscnp2  23279  discmp  23438  conncompcld  23474  1stcrestlem  23492  2ndcdisj  23496  topnlly  23531  disllycmp  23538  dis1stc  23539  txuni2  23605  xkotf  23625  dfac14lem  23657  prdstps  23669  txindis  23674  tx1stc  23690  xkohaus  23693  xkoptsub  23694  cnmpt1st  23708  cnmpt2nd  23709  ptcmpfi  23853  trfil1  23926  fin1aufil  23972  tgpconncompeqg  24152  tgpconncomp  24153  trust  24269  met1stc  24561  dscmet  24612  retopon  24803  cnfldtopon  24822  xrsxmet  24850  xrsmopn  24853  iimulcn  24980  icopnfhmeo  24985  iccpnfhmeo  24987  xrhmeo  24988  cnheiborlem  24996  lebnumii  25008  ishtpy  25014  htpycc  25022  pco1  25057  pcohtpylem  25061  pcopt  25064  pcopt2  25065  pcoass  25066  pcorevlem  25068  rrxcph  25434  rrx0el  25440  ovoliunlem3  25546  ovolicc1  25558  ovolicc2  25564  volf  25571  ioorf  25615  dyadf  25633  dyadmbl  25642  vitalilem5  25654  vitali  25655  mbfimaopnlem  25697  mbflimsup  25708  0plef  25714  i1fima  25720  i1fima2  25721  i1fd  25723  itg1ge0  25728  itg10  25730  i1f1lem  25731  i1fadd  25737  i1fmul  25738  i1fmulc  25745  mbfi1fseqlem5  25761  itg2addlem  25800  reldv  25912  dvbsss  25944  dvef  26022  lhop1lem  26055  deg1fvi  26125  plypf1  26252  coeeulem  26264  coeeu  26265  vieta1lem2  26352  aannenlem3  26371  aalioulem3  26375  dvradcnv  26461  pserulm  26462  pserdvlem2  26468  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  26790  logblog  26834  angpined  26872  1cubr  26884  asinsin  26934  asin1  26936  reasinsin  26938  atan0  26950  atanbnd  26968  atan1  26970  log2cnv  26986  log2ub  26991  log2le1  26992  birthday  26996  amgmlem  27031  emcllem5  27041  emgt0  27048  harmonicbnd3  27049  ftalem3  27116  basellem4  27125  sgmf  27186  ppi1  27205  cht1  27206  vma1  27207  ppiltx  27218  sqff1o  27223  ppiublem1  27243  ppiublem2  27244  ppiub  27245  chtub  27253  dchreq  27299  bposlem7  27331  bposlem8  27332  bposlem9  27333  lgsdir2lem2  27367  lgsdir2lem3  27368  chebbnd1  27513  chto1ub  27517  chpo1ubb  27522  pntibndlem1  27630  nosgnn0  27699  ltssolem1  27716  bdayfo  27718  nolt02o  27736  nogt01o  27737  noetasuplem4  27777  noetainflem4  27781  cutbdaybnd2lim  27867  madeun  27954  cutsfo  27975  addsproplem2  28040  addsproplem7  28045  addsprop  28046  negsprop  28105  subsf  28134  mulsproplem13  28198  mulsproplem14  28199  mulsprop  28200  oniso  28341  n0cut  28404  bdayn0sf1o  28440  twocut  28493  bdaypw2n0bndlem  28533  bdayfinbndlem1  28537  0reno  28566  tgldimor  28648  tglnfn  28693  axlowdimlem4  29092  axlowdimlem16  29104  axlowdim  29108  upgrfi  29238  lfgrnloop  29272  lfuhgr1v0e  29401  usgrexmplef  29406  usgrres  29455  vdegp1bi  29684  vtxdginducedm1lem2  29687  dfpth2  29875  pthdlem2  29914  wpthswwlks2on  30110  0ewlk  30262  0pth  30273  konigsbergiedgw  30396  konigsberglem1  30400  konigsberglem2  30401  konigsberglem3  30402  konigsberglem4  30403  konigsberglem5  30404  ex-dif  30571  ex-un  30572  ex-in  30573  ex-fl  30595  avril1  30611  9p10ne21fool  30619  n0lplig  30632  cnidOLD  30731  cnnvm  30831  ipasslem8  30986  ipasslem10  30988  hvsubf  31164  normlem1  31259  normlem6  31264  normlem7  31265  norm-ii-i  31286  norm3adifii  31297  hilid  31310  hlimf  31386  hhssabloi  31411  hhssnv  31413  hhshsslem1  31416  shincli  31511  shsval2i  31536  shs0i  31598  chj0i  31604  chm1i  31605  chincli  31609  chdmm1i  31626  shjshsi  31641  chsup0  31697  h1de2bi  31703  spansnpji  31727  cmcmlem  31740  cmcmii  31746  cmcm2ii  31747  cmcm3ii  31748  pjidmi  31822  pjssmii  31830  pj0i  31842  pjocini  31847  mayetes3i  31878  df0op2  31901  hoaddcomi  31921  hoaddassi  31925  hocadddiri  31928  hocsubdiri  31929  hoaddridi  31935  ho0coi  31937  hoid1i  31938  hoid1ri  31939  hodseqi  31943  honegsubi  31945  adj1o  32043  hoddii  32138  lnopunilem1  32159  lnopunilem2  32160  nmcopexi  32176  nmcopex  32178  nmcoplb  32179  nmcfnexi  32200  nmcfnex  32202  nmcfnlb  32203  adjbd1o  32234  adjcoi  32249  nmopcoadji  32250  opsqrlem6  32294  pjsdii  32304  pjddii  32305  pjidmcoi  32326  pjtoi  32328  pjin1i  32341  pjclem1  32344  stji1i  32391  reuxfrdf  32638  iuninc  32709  fnresin  32776  rinvf1o  32782  suppss2f  32790  xppreima  32797  ofoprabco  32816  partfun2  32828  fressupp  32840  supppreima  32843  fsupprnfi  32844  gtiso  32853  df1stres  32856  df2ndres  32857  snct  32864  padct  32870  fsuppcurry1  32876  fsuppcurry2  32877  ffsrn  32880  fpwrelmapffs  32886  fzodif1  32944  nnindf  32972  nn0min  32973  dp2lt  33023  dp2ltsuc  33024  dp2ltc  33025  dplti  33043  dpmul  33051  dpmul4  33052  ressplusf  33102  xrsclat  33150  xrge00  33153  xrnarchi  33325  elrgspnlem2  33385  1fldgenq  33470  xrge0slmod  33495  zringfrac  33711  esplyind  33833  ply1degltdimlem  33880  ccfldsrarelvec  33929  ccfldextdgrr  33930  locfinreflem  34098  locfinref  34099  unicls  34161  sqsscirc1  34166  mhmhmeotmd  34185  raddcn  34187  xrge0iifiso  34193  xrge0iifhmeo  34194  lmxrge0  34210  cnzh  34226  rezh  34227  qqh0  34242  qqh1  34243  qqhre  34278  rrhre  34279  esumnul  34306  esum0  34307  esumsnf  34322  esumpfinvallem  34332  esumpfinvalf  34334  esumpcvgval  34336  esumcvgsum  34346  esumsup  34347  esumcvgre  34349  sigaclfu2  34379  dmsigagen  34402  ddemeas  34494  mbfmvolf  34524  br2base  34527  omssubadd  34558  sibfof  34598  sitg0  34604  eulerpartlemt  34629  eulerpartgbij  34630  0rrv  34709  coinfliplem  34737  coinflipprob  34738  coinfliprv  34741  ballotlem2  34747  ballotlem4  34757  ballotlem5  34758  ballotlemi1  34761  ballotlem7  34794  ballotth  34796  signsplypnf  34808  signsply0  34809  signsw0g  34814  signswch  34819  signsvf0  34838  hashreprin  34878  reprfz1  34882  chtvalz  34887  hgt750lemd  34906  hgt750lem  34909  hgt750lem2  34910  bnj1098  35043  bnj1109  35046  bnj1131  35047  bnj1533  35111  bnj151  35136  bnj580  35172  bnj852  35180  bnj864  35181  bnj865  35182  bnj978  35208  bnj1021  35225  bnj907  35226  bnj1093  35239  bnj1145  35252  bnj1172  35260  bnj1174  35262  bnj1176  35264  bnj1186  35266  nfan1c  35332  xoromon  35348  fineqvac  35376  tz9.1regs  35394  axpowg  35406  onvf1odlem4  35413  onvf1od  35414  subfacf  35489  subfacp1lem1  35493  subfacp1lem5  35498  subfacp1lem6  35499  subfacval3  35503  erdszelem2  35506  kur14lem4  35523  ioosconn  35561  iccllysconn  35564  satfn  35669  fmlaomn0  35704  gonan0  35706  goaln0  35707  elnanelprv  35743  msrfo  35860  mthmpps  35896  problem5  35983  quad3  35984  circum  35988  antnestALT  36008  axextprim  36015  axrepprim  36016  axunprim  36017  axinfprim  36020  axacprim  36021  bcneg1  36050  dfon2lem2  36096  dfon2lem4  36098  axextdfeq  36109  fobigcup  36212  snelsingles  36234  fullfunfnv  36260  fullfunfv  36261  rankaltopb  36293  rank0  36484  rankeq1o  36485  hfuni  36498  in-ax8  36548  fneer  36677  neibastop1  36683  nabi1i  36718  nabi2i  36719  limsucncmpi  36769  tz9.1ctco  36806  ttctr3  36819  ttcpwss  36839  knoppcnlem8  36902  knoppcnlem11  36905  cnndvlem1  36939  bj-consensusALT  36986  bj-sbidmOLD  37299  bj-n0i  37400  bj-snsetex  37412  bj-tagss  37429  bj-2upln0  37472  bj-2upln1upl  37473  bj-nuliota  37506  bj-axseprep  37523  bj-0int  37555  bj-elid5  37625  bj-inftyexpitaufo  37658  bj-pinftyccb  37677  bj-minftyccb  37681  bj-pinftynminfty  37683  bj-isrvec  37750  iccioo01  37785  f1omptsnlem  37794  mptsnunlem  37796  topdifinffinlem  37805  relowlpssretop  37822  1oequni2o  37826  pibt2  37875  imadifss  38058  tan2h  38075  poimirlem3  38086  poimirlem9  38092  poimirlem16  38099  poimirlem17  38100  poimirlem18  38101  poimirlem19  38102  poimirlem20  38103  poimirlem22  38105  poimirlem30  38113  mblfinlem1  38120  mblfinlem2  38121  ovoliunnfl  38125  voliunnfl  38127  itg2addnclem  38134  itg2addnclem2  38135  asindmre  38166  areacirclem1  38171  fdc  38208  cntotbnd  38259  heiborlem6  38279  rrnval  38290  reheibor  38302  rngosn3  38387  brcnvrabga  38805  cnvresrn  38811  moantr  38835  inxp2  38838  dfxrn2  38848  dfsucmap3  38926  dfpre4  38943  cnvcosseq  38990  refrelcosslem  39015  1cosscnvxrn  39028  redundss3  39175  refrelsredund3  39181  refrelredund3  39184  disjimeceqim  39267  eqvrel0  39352  eqvrelid  39355  prter2  39469  renegclALT  39551  mapdunirnN  42238  lcmeprodgcdi  42588  3factsumint2  42603  3factsumint3  42604  3factsumint4  42605  3factsumint  42606  lcmineqlem4  42613  3lexlogpow5ineq1  42635  3lexlogpow2ineq1  42639  dvrelogpow2b  42649  aks4d1p1p4  42652  aks4d1p8  42668  aks6d1c1  42697  aks6d1c2p2  42700  aks6d1c4  42705  2ap1caineq  42726  sticksstones1  42727  sticksstones2  42728  aks6d1c7lem2  42762  aks5lem3a  42770  aks5lem6  42773  unitscyglem2  42777  unitscyglem3  42778  sqdeccom12  42862  readvrec2  42934  readvcot  42937  resubf  42954  sn-0ne2  42979  sn-subf  43002  sn-nnne0  43046  sn-0lt1  43061  reneg1lt0  43066  rntrclfvOAI  43236  diophrw  43304  rabren3dioph  43356  pellexlem6  43375  pellex  43376  frmx  43454  frmy  43455  jm2.23  43537  jm2.27dlem3  43552  axac10  43574  pw2f1ocnv  43578  kelac2lem  43605  lmhmlnmsplit  43628  pwfi2f1o  43637  frlmpwfi  43639  insucid  43944  nla0003  43965  ifpbiidcor  44014  sucomisnotcard  44084  alephiso2  44098  alephiso3  44099  cnvnonrel  44128  rnnonrel  44131  resnonrel  44132  cononrel1  44134  cononrel2  44135  fvnonrel  44137  cnvcnvintabd  44140  cnvintabd  44143  rclexi  44155  rtrclex  44157  clcnvlem  44163  cnvrcl0  44165  dmtrcl  44167  rntrcl  44168  dfrtrcl5  44169  iunrelexp0  44242  dmtrclfvRP  44270  rntrclfv  44272  corcltrcl  44279  cotrclrcl  44282  0heALT  44323  frege54cor1a  44404  uneqsn  44565  clsk3nimkb  44580  int-sqdefd  44721  int-sqgeq0d  44726  rr-groth  44839  rr-grothprim  44840  rr-grothshort  44844  seff  44849  expgrowthi  44873  expgrowth  44875  binomcxplemnotnn0  44896  ee233  45059  ax6e2nd  45098  in1  45111  dfvd2ani  45123  dfvd2i  45125  dfvd3i  45132  dfvd3ani  45135  e0bi  45315  uun2221  45352  uun2221p1  45353  uun2221p2  45354  en3lpVD  45384  relopabVD  45440  ax6e2ndVD  45447  ax6e2ndALT  45469  permaxpow  45549  pssnssi  45643  nnf1oxpnn  45737  icof  45759  fnmptif  45804  rn1st  45812  negpilt0  45824  xrgtso  45885  supxrleubrnmptf  45989  xrpnf  46023  rexanuz2nf  46030  ioontr  46051  iccdifioo  46055  iccdifprioo  46056  uzinico2  46101  fsummulc1f  46111  fsumiunss  46115  fnlimfvre2  46215  limsupreuz  46275  limsup10ex  46311  icccncfext  46425  dvcosre  46450  dvsinax  46451  ioodvbdlimc1lem2  46470  ioodvbdlimc2lem  46472  dvmptmulf  46475  dvnmul  46481  dvmptfprodlem  46482  dvnprodlem2  46485  stoweidlem1  46539  stoweidlem26  46564  stoweidlem34  46572  stoweidlem44  46582  stoweid  46601  stirlinglem5  46616  dirkercncflem1  46641  fourierdlem44  46689  fourierdlem56  46700  fourierdlem62  46706  fourierdlem89  46733  fourierdlem91  46735  fourierdlem100  46744  fourierdlem102  46746  fourierdlem103  46747  fourierdlem104  46748  fourierdlem108  46752  fourierdlem112  46756  fourierdlem114  46758  fouriersw  46769  rrndistlt  46828  gsumge0cl  46909  sge0tsms  46918  sge0ltfirpmpt2  46964  ovn0  47104  hoidmv1le  47132  hoidmvle  47138  ovnsubadd2lem  47183  ovolval4lem1  47187  vonioolem2  47219  smflimlem3  47311  nsssmfmbf  47317  chnerlem1  47422  nthrucw  47426  goldrasin  47440  goldrapos  47441  sinnpoly  47449  axorbtnotaiffb  47461  axorbciffatcxorb  47463  abnotbtaxb  47473  euabsneu  47586  ceilhalf1  47896  sprval  48049  fmtnoinf  48109  nprmdvdsfacm1lem2  48194  ppivalnnnprmge6  48199  ppivalnn4  48200  ppivalnn  48205  1nevenALTV  48277  nfermltl8rev  48328  nfermltl2rev  48329  nnsum3primes4  48374  tgblthelfgott  48401  tgoldbachlt  48402  cycl3grtri  48533  isubgr3stgrlem3  48554  usgrexmpl1lem  48607  usgrexmpl2lem  48612  usgrexmpl2trifr  48623  gpgprismgr4cycllem7  48687  ldepslinc  49095  ackval42  49282  rrx2plordso  49310  vsn  49397  dmtposss  49461  sepfsepc  49513  basresposfo  49563  rescofuf  49678  oppff1  49733  idfth  49743  idsubc  49745  fuco2eld2  49899  fuco22a  49935  setc1onsubc  50187  alimp-no-surprise  50366  aacllem  50386  amgmwlem  50387  amgmlemALT  50388