Theorem mpbi 233

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

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  pm5.74i  274  notbii  323  biluk  390  pm5.19  391  pm3.24  408  dfbi  481  pm4.71i  569  pm5.32i  585  biadani  832  biadanii  834  imori  868  ori  875  pm5.16  1031  dn1  1073  3ori  1451  cadan  1642  nic-dfim  1702  nic-dfneg  1703  nic-mp  1704  nic-mpALT  1705  tbw-negdf  1732  rb-imdf  1783  nfri  1822  mpgbi  1831  19.35i  1911  nfim1  2238  19.36i  2270  ax6  2419  sbie  2537  datisi  2710  disamis  2711  dimatis  2718  fresison  2719  bamalip  2722  axi12  2736  eqcomi  2775  eqtri  2789  eleqtri  2864  nfnfc  2940  neii  2963  necomi  3015  neeqtri  3033  neli  3069  nrex  3096  rexlimi  3268  eueqi  3675  euxfr2w  3686  euxfr2  3688  reuxfrd  3714  cdeqri  3732  sseqtri  3988  pssn2lp  4062  equncomi  4117  unssi  4147  ssini  4195  unabs  4221  inabs  4222  dfin4  4234  vn0OLD  4302  inindif  4334  difidALT  4336  ab0orv  4342  ab0orvALT  4343  difin0  4438  pwundif  4592  snid  4633  rabrsn  4695  iinrab2  5039  symdifv  5057  rintn0  5080  breqtri  5141  axsepgfromrep  5260  bm1.3iiOLD  5270  ax6vsep  5271  notsep  5339  zfpow  5342  dtruALT2  5346  dtruALT  5364  reusv2lem4  5377  dtru  5423  el.OLD  5425  op1stb  5458  copsexgw  5477  copsexgwOLD  5478  copsexg  5479  uniop  5503  rn0  5921  dmresi  6059  somincom  6139  cnvimassrndm  6154  cnvcnv  6195  elid  6203  rescnvcnv  6210  cnvcnvres  6211  cocnvcnv2  6265  cores2  6266  co01  6268  cnviin  6294  predres  6347  iota4an  6525  fnopab  6680  mpt0  6684  fnmpti  6685  f1cnvcnv  6792  f1ovi  6868  eliman0  6925  fvco4i  6990  cnvimainrn  7069  fmpti  7114  funiunfv  7253  oprabss  7531  relmptopab  7673  zfun  7746  tfinds2  7869  omon  7883  2nd0  8002  f1stres  8019  f2ndres  8020  cnvoprab  8066  relmpoopab  8098  df1st2  8102  df2nd2  8103  fsplit  8121  frpoins3xpg  8145  frpoins3xp3g  8146  poxp2  8148  poseq  8163  reldmtpos  8239  dftpos4  8250  tpostpos  8251  tpos0  8261  frrlem4  8295  smo0  8354  tfrlem14  8387  tfrlem16  8389  rdgsucg  8419  rdglimg  8421  frfnom  8431  oawordeulem  8548  uniixp  8928  dfdom2  8984  ssdomg  9006  xpcomf1o  9064  sbthlem5  9089  sdom0  9107  limensuci  9151  1sdom2  9218  fiint  9296  fidomdm  9301  residfi  9305  mptfi  9318  fisn  9397  dffi3  9401  ordtypelem6  9495  ordtypelem7  9496  wemaplem2  9519  harwdom  9563  nelaneqOLD  9575  suc11reg  9598  zfinf  9618  axinf2  9619  noinfep  9639  cantnfvalf  9644  cantnflt  9651  cantnf0  9654  cantnf  9672  ttrclco  9697  tz9.1c  9709  tc2  9719  setinds  9728  r111  9757  r1tr2  9759  r1ordg  9760  r1sssuc  9765  r1val1  9768  tz9.13  9773  r1elssi  9787  pwwf  9789  rankopb  9834  rankeq0b  9842  ranksuc  9847  rankmapu  9860  rankxplim3  9863  rankxpsuc  9864  cp  9893  karden  9898  kardenOLD  9899  card0  9963  cardlim  9977  cardom  9991  infxpenlem  10016  alephsuc2  10083  alephgeom  10085  unialeph  10104  dfac4  10125  dfacacn  10144  dju1dif  10175  dju1p1e2  10176  infdju1  10192  ackbij1lem13  10233  ackbij2  10244  cf0  10252  cfsuc  10259  cfom  10266  cfslb2n  10270  ominf4  10314  fin23lem17  10340  fin23lem28  10342  fin23lem30  10344  fin23lem31  10345  fin23lem40  10353  isfin1-3  10388  dfacfin7  10401  fin1a2lem6  10407  itunitc1  10422  axcc3  10440  dcomex  10449  axdc2lem  10450  axcclem  10459  zfac  10462  ac3  10464  ackm  10467  axac2  10468  axac  10469  axaci  10470  cardeqv  10471  numth2  10473  numth  10474  dmct  10526  brdom3  10530  fin71ac  10535  cardf  10552  aleph1  10574  cfpwsdom  10587  smobeth  10589  zfcndrep  10617  zfcndpow  10619  zfcndac  10622  gch2  10678  wunex3  10744  tskpr  10773  inar1  10778  rankcf  10780  tskcard  10784  tskuni  10786  grothpw  10829  axgroth4  10835  grothprim  10837  inaprc  10839  dmaddpi  10893  dmmulpi  10894  1lt2pi  10908  addpqf  10947  mulpqf  10949  1lt2nq  10976  supsrlem  11114  ssxr  11297  gtso  11309  subf  11477  negne0i  11551  mulnzcnf  11878  infrenegsup  12216  neg1lt0  12224  nnne0  12288  halflt1  12479  nn0ssz  12632  3halfnz  12693  zeo  12700  numlt  12759  numltc  12760  le9lt10  12761  decle  12768  uzf  12883  xaddf  13268  xsubge0  13305  xmulf  13316  ixxf  13400  ixxssxr  13402  iooval2  13423  ioof  13492  unirnioo  13494  dfioo2  13495  fzval2  13556  fzf  13557  0nelfz1  13589  fz10  13591  fz00m1  13592  fzpreddisj  13620  4fvwrd4  13695  fzof  13703  fzo0  13731  fldiv4p1lem1div2  13888  fldiv4lem1div2  13890  om2uzoi  14011  faclbnd4lem1  14349  hashkf  14388  hashgval  14389  hashinf  14391  hashresfn  14396  hashnn0n0nn  14447  hashge3el3dif  14544  hash3tpde  14550  rev0  14825  s2dm  14953  f1oun2prg  14980  trclublem  15058  sqrt2gt1lt2  15351  limsupgord  15549  fclim  15630  fsumrelem  15885  ackbijnn  15908  incexclem  15916  incexc  15917  arisum2  15941  georeclim  15952  geoisumr  15958  0.999...  15961  ege2le3  16169  sin0  16230  ef01bndlem  16265  cos2bnd  16269  cos01gt0  16272  sincos2sgn  16275  sin4lt0  16276  rpnnen2lem3  16297  rpnnen2lem9  16303  rexpen  16309  cnso  16328  dvdslelem  16392  divalglem1  16477  divalglem5  16480  divalglem6  16481  divalglem10  16485  flodddiv4  16498  0bits  16522  sadcf  16536  sadcadd  16541  bitsshft  16558  smupf  16561  gcdf  16595  eucalgf  16666  2prm  16775  dfphi2  16858  pockthi  16992  prmrec  17007  vdwapf  17057  vdwlem6  17071  karatsuba  17168  1259lem5  17220  2503lem3  17224  4001lem4  17229  structcnvcnv  17238  structfn  17241  strleun  17242  imasvscafn  17616  xpsff1o  17646  xrge0base  17686  wunnat  18041  dfinito3  18087  dftermo3  18088  eldmcoa  18147  coapm  18153  catcfuccl  18200  catcxpccl  18288  yonedainv  18362  chnub  18703  smndex1bas  18999  smndex1n0mnd  19005  grpinvfvi  19080  mulgfvi  19170  ressmulgnnd  19175  symgsssg  19568  symgfisg  19569  psgnunilem5  19595  sylow3lem2  19729  oppglsm  19743  efgmf  19814  efgval  19818  efgsf  19830  0frgp  19880  dmdprd  20101  dprdval  20106  invrfval  20504  drngui  20870  rmodislmod  21088  lssintcl  21122  cnfldadd  21565  cnfldmul  21567  cnfldfunALT  21574  cnfld0  21583  cnfld1  21584  cnfldsub  21587  xrsds  21597  pzriprnglem4  21671  pzriprnglem9  21676  pzriprnglem14  21681  psgnghm  21767  zrhpsgnmhm  21771  ocv1  21866  dsmmbas2  21924  mplsubrglem  22190  opsrtoslem2  22244  evl1maprhm  22576  mdetralt  22802  maducoeval2  22834  eltpsi  23138  unitg  23161  fctop  23198  cctop  23200  ppttop  23201  epttop  23203  leordtvallem1  23404  leordtvallem2  23405  iccordt  23408  iscnp2  23433  discmp  23592  conncompcld  23628  1stcrestlem  23646  2ndcdisj  23650  topnlly  23685  disllycmp  23692  dis1stc  23693  txuni2  23759  xkotf  23779  dfac14lem  23811  prdstps  23823  txindis  23828  tx1stc  23844  xkohaus  23847  xkoptsub  23848  cnmpt1st  23862  cnmpt2nd  23863  ptcmpfi  24007  trfil1  24080  fin1aufil  24126  tgpconncompeqg  24306  tgpconncomp  24307  trust  24423  met1stc  24715  dscmet  24766  retopon  24957  cnfldtopon  24976  xrsxmet  25004  xrsmopn  25007  iimulcn  25134  icopnfhmeo  25139  iccpnfhmeo  25141  xrhmeo  25142  cnheiborlem  25150  lebnumii  25162  ishtpy  25168  htpycc  25176  pco1  25211  pcohtpylem  25215  pcopt  25218  pcopt2  25219  pcoass  25220  pcorevlem  25222  rrxcph  25588  rrx0el  25594  ovoliunlem3  25700  ovolicc1  25712  ovolicc2  25718  volf  25725  ioorf  25769  dyadf  25787  dyadmbl  25796  vitalilem5  25808  vitali  25809  mbfimaopnlem  25851  mbflimsup  25862  0plef  25868  i1fima  25874  i1fima2  25875  i1fd  25877  itg1ge0  25882  itg10  25884  i1f1lem  25885  i1fadd  25891  i1fmul  25892  i1fmulc  25899  mbfi1fseqlem5  25915  itg2addlem  25954  reldv  26066  dvbsss  26098  dvef  26176  lhop1lem  26209  deg1fvi  26279  plypf1  26406  coeeulem  26418  coeeu  26419  vieta1lem2  26509  aannenlem3  26530  aalioulem3  26534  dvradcnv  26621  pserulm  26622  pserdvlem2  26628  sinhalfpilem  26665  sincos4thpi  26715  tan4thpiOLD  26717  sincos6thpi  26718  pige3ALT  26722  resinf1o  26738  tanord1  26739  tanregt0  26741  efabl  26752  relogrn  26763  dfrelog  26767  logi  26789  logneg  26790  logltb  26802  logcn  26849  logf1o2  26852  dvlog  26853  efopnlem2  26859  efopn  26860  logccv  26865  dvsqrt  26944  dvcnsqrt  26946  cxpcn3  26950  logblog  26994  angpined  27032  1cubr  27044  asinsin  27094  asin1  27096  reasinsin  27098  atan0  27110  atanbnd  27128  atan1  27130  log2cnv  27146  log2ub  27151  log2le1  27152  birthday  27156  amgmlem  27191  emcllem5  27201  emgt0  27208  harmonicbnd3  27209  ftalem3  27276  basellem4  27285  sgmf  27346  ppi1  27365  cht1  27366  vma1  27367  ppiltx  27378  sqff1o  27383  ppiublem1  27403  ppiublem2  27404  ppiub  27405  chtub  27413  dchreq  27459  bposlem7  27491  bposlem8  27492  bposlem9  27493  lgsdir2lem2  27527  lgsdir2lem3  27528  chebbnd1  27673  chto1ub  27677  chpo1ubb  27682  pntibndlem1  27790  nosgnn0  27859  ltssolem1  27876  bdayfo  27878  nolt02o  27896  nogt01o  27897  noetasuplem4  27937  noetainflem4  27941  cutbdaybnd2lim  28027  madeun  28114  cutsfo  28135  addsproplem2  28200  addsproplem7  28205  addsprop  28206  negsprop  28265  subsf  28294  mulsproplem13  28358  mulsproplem14  28359  mulsprop  28360  oniso  28501  n0cut  28564  bdayn0sf1o  28600  twocut  28653  bdaypw2n0bndlem  28693  bdayfinbndlem1  28697  0reno  28726  tgldimor  28808  tglnfn  28853  tgplnfn  29094  axlowdimlem4  29332  axlowdimlem16  29344  axlowdim  29348  upgrfi  29478  lfgrnloop  29512  lfuhgr1v0e  29641  usgrexmplef  29646  usgrres  29695  vdegp1bi  29924  vtxdginducedm1lem2  29927  dfpth2  30115  pthdlem2  30154  wpthswwlks2on  30350  0ewlk  30502  0pth  30513  konigsbergiedgw  30636  konigsberglem1  30640  konigsberglem2  30641  konigsberglem3  30642  konigsberglem4  30643  konigsberglem5  30644  ex-dif  30811  ex-un  30812  ex-in  30813  ex-fl  30835  avril1  30851  9p10ne21fool  30859  n0lplig  30872  cnidOLD  30971  cnnvm  31071  ipasslem8  31226  ipasslem10  31228  hvsubf  31404  normlem1  31499  normlem6  31504  normlem7  31505  norm-ii-i  31526  norm3adifii  31537  hilid  31550  hlimf  31626  hhssabloi  31651  hhssnv  31653  hhshsslem1  31656  shincli  31751  shsval2i  31776  shs0i  31838  chj0i  31844  chm1i  31845  chincli  31849  chdmm1i  31866  shjshsi  31881  chsup0  31937  h1de2bi  31943  spansnpji  31967  cmcmlem  31980  cmcmii  31986  cmcm2ii  31987  cmcm3ii  31988  pjidmi  32062  pjssmii  32070  pj0i  32082  pjocini  32087  mayetes3i  32118  df0op2  32141  hoaddcomi  32161  hoaddassi  32165  hocadddiri  32168  hocsubdiri  32169  hoaddridi  32175  ho0coi  32177  hoid1i  32178  hoid1ri  32179  hodseqi  32183  honegsubi  32185  adj1o  32283  hoddii  32378  lnopunilem1  32399  lnopunilem2  32400  nmcopexi  32416  nmcopex  32418  nmcoplb  32419  nmcfnexi  32440  nmcfnex  32442  nmcfnlb  32443  adjbd1o  32474  adjcoi  32489  nmopcoadji  32490  opsqrlem6  32534  pjsdii  32544  pjddii  32545  pjidmcoi  32566  pjtoi  32568  pjin1i  32581  pjclem1  32584  stji1i  32631  reuxfrdf  32874  iuninc  32942  fnresin  33006  rinvf1o  33012  suppss2f  33020  xppreima  33027  ofoprabco  33046  partfun2  33058  fressupp  33070  supppreima  33073  fsupprnfi  33074  gtiso  33083  df1stres  33086  df2ndres  33087  snct  33094  padct  33100  fsuppcurry1  33106  fsuppcurry2  33107  ffsrn  33110  fpwrelmapffs  33116  fzodif1  33174  nnindf  33201  nn0min  33202  dp2lt  33241  dp2ltsuc  33242  dp2ltc  33243  dplti  33261  dpmul  33269  dpmul4  33270  ressplusf  33314  xrsclat  33362  xrge00  33365  xrnarchi  33535  elrgspnlem2  33594  1fldgenq  33674  xrge0slmod  33699  zringfrac  33875  esplyind  33996  ply1degltdimlem  34043  ccfldsrarelvec  34092  ccfldextdgrr  34093  locfinreflem  34261  locfinref  34262  unicls  34324  sqsscirc1  34329  mhmhmeotmd  34348  raddcn  34350  xrge0iifiso  34356  xrge0iifhmeo  34357  lmxrge0  34373  cnzh  34389  rezh  34390  qqh0  34405  qqh1  34406  qqhre  34441  rrhre  34442  esumnul  34469  esum0  34470  esumsnf  34485  esumpfinvallem  34495  esumpfinvalf  34497  esumpcvgval  34499  esumcvgsum  34509  esumsup  34510  esumcvgre  34512  sigaclfu2  34542  dmsigagen  34565  ddemeas  34657  mbfmvolf  34687  br2base  34690  omssubadd  34721  sibfof  34761  sitg0  34767  eulerpartlemt  34792  eulerpartgbij  34793  0rrv  34872  coinfliplem  34900  coinflipprob  34901  coinfliprv  34904  ballotlem2  34910  ballotlem4  34920  ballotlem5  34921  ballotlemi1  34924  ballotlem7  34957  ballotth  34959  signsplypnf  34968  signsply0  34969  signsw0g  34974  signswch  34979  signsvf0  34998  hashreprin  35038  reprfz1  35042  chtvalz  35047  hgt750lemd  35066  hgt750lem  35069  hgt750lem2  35070  bnj1098  35203  bnj1109  35206  bnj1131  35207  bnj1533  35271  bnj151  35296  bnj580  35332  bnj852  35340  bnj864  35341  bnj865  35342  bnj978  35368  bnj1021  35385  bnj907  35386  bnj1093  35399  bnj1145  35412  bnj1172  35420  bnj1174  35422  bnj1176  35424  bnj1186  35426  nfan1c  35492  xoromon  35503  rankfo  35529  fineqvac  35552  tz9.1regs  35570  axpowg  35582  onvf1odlem4  35613  onvf1od  35614  subfacf  35687  subfacp1lem1  35691  subfacp1lem5  35696  subfacp1lem6  35697  subfacval3  35701  erdszelem2  35704  kur14lem4  35721  ioosconn  35759  iccllysconn  35762  satfn  35867  fmlaomn0  35902  gonan0  35904  goaln0  35905  elnanelprv  35941  msrfo  36058  mthmpps  36094  problem5  36181  quad3  36182  circum  36186  antnestALT  36206  axextprim  36213  axrepprim  36214  axunprim  36215  axinfprim  36218  axacprim  36219  bcneg1  36248  dfon2lem2  36294  dfon2lem4  36296  axextdfeq  36307  fobigcup  36410  snelsingles  36432  fullfunfnv  36458  fullfunfv  36459  rankaltopb  36491  rank0  36682  rankeq1o  36683  hfuni  36696  in-ax8  36776  fneer  36904  neibastop1  36910  nabi1i  36945  nabi2i  36946  limsucncmpi  36996  tz9.1ctco  37033  ttctr3  37046  ttcpwss  37066  knoppcnlem8  37129  knoppcnlem11  37132  cnndvlem1  37166  bj-consensusALT  37212  bj-sbidmOLD  37525  bj-n0i  37627  bj-snsetex  37639  bj-tagss  37656  bj-2upln0  37699  bj-2upln1upl  37700  bj-nuliota  37733  bj-axseprep  37751  bj-0int  37783  bj-elid5  37853  bj-inftyexpitaufo  37886  bj-pinftyccb  37905  bj-minftyccb  37909  bj-pinftynminfty  37911  bj-isrvec  37978  iccioo01  38013  f1omptsnlem  38022  mptsnunlem  38024  topdifinffinlem  38033  relowlpssretop  38050  1oequni2o  38054  pibt2  38103  imadifss  38286  tan2h  38303  poimirlem3  38314  poimirlem9  38320  poimirlem16  38327  poimirlem17  38328  poimirlem18  38329  poimirlem19  38330  poimirlem20  38331  poimirlem22  38333  poimirlem30  38341  mblfinlem1  38348  mblfinlem2  38349  ovoliunnfl  38353  voliunnfl  38355  itg2addnclem  38362  itg2addnclem2  38363  asindmre  38394  areacirclem1  38399  fdc  38436  cntotbnd  38487  heiborlem6  38507  rrnval  38518  reheibor  38530  rngosn3  38615  brcnvrabga  39031  cnvresrn  39037  moantr  39061  inxp2  39064  dfxrn2  39074  dfsucmap3  39152  dfpre4  39169  cnvcosseq  39216  refrelcosslem  39241  1cosscnvxrn  39254  redundss3  39401  refrelsredund3  39407  refrelredund3  39410  disjimeceqim  39493  eqvrel0  39578  eqvrelid  39581  prter2  39695  renegclALT  39777  mapdunirnN  42464  lcmeprodgcdi  42814  3factsumint2  42829  3factsumint3  42830  3factsumint4  42831  3factsumint  42832  lcmineqlem4  42839  3lexlogpow5ineq1  42861  3lexlogpow2ineq1  42865  dvrelogpow2b  42875  aks4d1p1p4  42878  aks4d1p8  42894  aks6d1c1  42923  aks6d1c2p2  42926  aks6d1c4  42931  2ap1caineq  42952  sticksstones1  42953  sticksstones2  42954  aks6d1c7lem2  42988  aks5lem3a  42996  aks5lem6  42999  unitscyglem2  43003  unitscyglem3  43004  sqdeccom12  43090  readvrec2  43162  readvcot  43165  resubf  43182  sn-0ne2  43207  sn-subf  43230  sn-nnne0  43274  sn-0lt1  43289  reneg1lt0  43294  rntrclfvOAI  43462  diophrw  43530  rabren3dioph  43582  pellexlem6  43601  pellex  43602  frmx  43680  frmy  43681  jm2.23  43763  jm2.27dlem3  43778  axac10  43800  pw2f1ocnv  43804  kelac2lem  43831  lmhmlnmsplit  43854  pwfi2f1o  43863  frlmpwfi  43865  insucid  44170  nla0003  44191  ifpbiidcor  44240  sucomisnotcard  44310  alephiso2  44324  alephiso3  44325  cnvnonrel  44354  rnnonrel  44357  resnonrel  44358  cononrel1  44360  cononrel2  44361  fvnonrel  44363  cnvcnvintabd  44366  cnvintabd  44369  rclexi  44381  rtrclex  44383  clcnvlem  44389  cnvrcl0  44391  dmtrcl  44393  rntrcl  44394  dfrtrcl5  44395  iunrelexp0  44468  dmtrclfvRP  44496  rntrclfv  44498  corcltrcl  44505  cotrclrcl  44508  0heALT  44549  frege54cor1a  44630  uneqsn  44791  clsk3nimkb  44806  int-sqdefd  44947  int-sqgeq0d  44952  rr-groth  45049  rr-grothprim  45050  rr-grothshort  45054  seff  45059  expgrowthi  45083  expgrowth  45085  binomcxplemnotnn0  45106  ee233  45268  ax6e2nd  45307  in1  45320  dfvd2ani  45332  dfvd2i  45334  dfvd3i  45341  dfvd3ani  45344  e0bi  45524  uun2221  45561  uun2221p1  45562  uun2221p2  45563  en3lpVD  45593  relopabVD  45649  ax6e2ndVD  45656  ax6e2ndALT  45678  permaxpow  45758  pssnssi  45859  nnf1oxpnn  45953  icof  45975  fnmptif  46020  rn1st  46028  negpilt0  46040  xrgtso  46101  supxrleubrnmptf  46205  xrpnf  46239  rexanuz2nf  46246  ioontr  46267  iccdifioo  46271  iccdifprioo  46272  uzinico2  46317  fsummulc1f  46327  fsumiunss  46331  fnlimfvre2  46431  limsupreuz  46491  limsup10ex  46527  icccncfext  46641  dvcosre  46666  dvsinax  46667  ioodvbdlimc1lem2  46686  ioodvbdlimc2lem  46688  dvmptmulf  46691  dvnmul  46697  dvmptfprodlem  46698  dvnprodlem2  46701  stoweidlem1  46755  stoweidlem26  46780  stoweidlem34  46788  stoweidlem44  46798  stoweid  46817  stirlinglem5  46832  dirkercncflem1  46857  fourierdlem44  46905  fourierdlem56  46916  fourierdlem62  46922  fourierdlem89  46949  fourierdlem91  46951  fourierdlem100  46960  fourierdlem102  46962  fourierdlem103  46963  fourierdlem104  46964  fourierdlem108  46968  fourierdlem112  46972  fourierdlem114  46974  fouriersw  46985  rrndistlt  47044  gsumge0cl  47125  sge0tsms  47134  sge0ltfirpmpt2  47180  ovn0  47320  hoidmv1le  47348  hoidmvle  47354  ovnsubadd2lem  47399  ovolval4lem1  47403  vonioolem2  47435  smflimlem3  47527  nsssmfmbf  47533  chnerlem1  47638  sqrtnzqaa  47645  nthrucw  47647  goldrasin  47659  goldrapos  47660  sinnpoly  47668  axorbtnotaiffb  47680  axorbciffatcxorb  47682  abnotbtaxb  47692  euabsneu  47805  ceilhalf1  48115  sprval  48268  fmtnoinf  48328  nprmdvdsfacm1lem2  48413  ppivalnnnprmge6  48418  ppivalnn4  48419  ppivalnn  48424  1nevenALTV  48496  nfermltl8rev  48547  nfermltl2rev  48548  nnsum3primes4  48593  tgblthelfgott  48620  tgoldbachlt  48621  cycl3grtri  48752  isubgr3stgrlem3  48773  usgrexmpl1lem  48826  usgrexmpl2lem  48831  usgrexmpl2trifr  48842  gpgprismgr4cycllem7  48906  ldepslinc  49329  ackval42  49516  rrx2plordso  49544  vsn  49630  dmtposss  49694  sepfsepc  49746  basresposfo  49796  rescofuf  49911  oppff1  49966  idfth  49976  idsubc  49978  fuco2eld2  50132  fuco22a  50168  setc1onsubc  50420  alimp-no-surprise  50599  aacllem  50661  3elfz13  50667  amgmwlem  50690  amgmlemALT  50691