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  1452  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  1913  nfim1  2239  19.36i  2271  ax6  2416  sbie  2534  datisi  2707  disamis  2708  dimatis  2715  fresison  2716  bamalip  2719  axi12  2733  eqcomi  2772  eqtri  2786  eleqtri  2862  nfnfc  2938  neii  2961  necomi  3013  neeqtri  3031  neli  3067  nrex  3094  rexlimi  3266  eueqi  3670  euxfr2w  3681  euxfr2  3683  reuxfrd  3709  cdeqri  3727  sseqtri  3961  pssn2lp  4035  ssini  4139  equncomi  4162  unssi  4192  unabs  4213  inabs  4214  dfin4  4226  vn0OLD  4295  inindif  4327  difidALT  4329  ab0orv  4335  ab0orvALT  4336  difin0  4431  pwundif  4586  snid  4623  rabrsn  4685  iinrab2  5031  symdifv  5049  rintn0  5072  breqtri  5133  axsepgfromrep  5250  ax6vsep  5260  notsep  5329  zfpow  5332  dtruALT2  5336  dtruALT  5354  reusv2lem4  5367  dtru  5409  el.OLD  5411  op1stb  5444  copsexgwOLD  5465  uniop  5492  rn0  5915  dmresi  6056  somincom  6140  cnvcnv  6196  elid  6206  cnvimassrndmOLD  6212  rescnvcnv  6218  cnvcnvres  6219  cocnvcnv2  6273  cores2  6274  co01  6278  cnviin  6307  predres  6360  iota4an  6539  fnopab  6699  mpt0  6703  fnmpti  6704  f1cnvcnv  6811  f1ovi  6888  eliman0  6945  fvco4i  7010  cnvimainrn  7090  fmpti  7136  funiunfv  7275  oprabss  7551  relmptopab  7695  zfun  7776  tfinds2  7899  omon  7913  2nd0  8032  f1stres  8049  f2ndres  8050  cnvoprab  8096  relmpoopab  8131  df1st2  8136  df2nd2  8137  fsplit  8155  frpoins3xpg  8184  frpoins3xp3g  8185  poxp2  8187  poseq  8202  reldmtpos  8279  dftpos4  8290  tpostpos  8291  tpos0  8301  frrlem4  8335  smo0  8394  tfrlem14  8427  tfrlem16  8429  rdgsucg  8459  rdglimg  8461  frfnom  8471  tz7.48lem  8478  oawordeulem  8590  uniixp  8977  dfdom2  9033  ssdomg  9055  xpcomf1o  9113  sbthlem5  9138  sdom0  9156  limensuci  9200  1sdom2  9267  fiint  9346  fidomdm  9351  residfi  9355  mptfi  9368  fisn  9446  dffi3  9450  ordtypelem6  9544  ordtypelem7  9545  wemaplem2  9568  harwdom  9612  nelaneqOLD  9624  suc11reg  9647  zfinf  9667  axinf2  9668  noinfep  9688  cantnfvalf  9693  cantnflt  9700  cantnf0  9703  cantnf  9721  ttrclco  9746  tz9.1c  9758  tc2  9768  setinds  9777  r111  9809  r1tr2  9811  r1ordg  9812  r1sssuc  9817  r1val1  9820  tz9.13  9825  r1elssi  9840  pwwf  9842  rankopb  9893  rankeq0b  9903  ranksuc  9909  rankmapu  9922  rankxplim3  9925  rankxpsuc  9926  hfuniOLD  9952  cp  9981  karden  9986  kardenOLD  9987  card0  10066  cardlim  10080  cardom  10094  infxpenlem  10119  alephsuc2  10186  alephgeom  10188  unialeph  10207  dfac4  10228  dfacacn  10247  dju1dif  10278  dju1p1e2  10279  infdju1  10295  ackbij1lem13  10336  ackbij2  10347  cf0  10355  cfsuc  10362  cfom  10369  cfslb2n  10373  ominf4  10417  fin23lem17  10443  fin23lem28  10445  fin23lem30  10447  fin23lem31  10448  fin23lem40  10456  isfin1-3  10491  dfacfin7  10504  fin1a2lem6  10510  itunitc1  10525  axcc3  10543  dcomex  10552  axdc2lem  10553  axcclem  10562  zfac  10565  ac3  10567  ackm  10570  axac2  10571  axac  10572  axaci  10573  cardeqv  10574  numth2  10576  numth  10577  dmct  10629  dmctOLD  10630  brdom3  10634  fin71ac  10639  cardf  10661  aleph1  10683  cfpwsdom  10696  smobeth  10698  zfcndrep  10726  zfcndpow  10728  zfcndac  10731  gch2  10787  wunex3  10853  tskpr  10882  inar1  10887  rankcf  10889  tskcard  10893  tskuni  10895  grothpw  10938  axgroth4  10944  grothprim  10946  inaprc  10948  dmaddpi  11002  dmmulpi  11003  1lt2pi  11017  addpqf  11056  mulpqf  11058  1lt2nq  11085  supsrlem  11223  ssxr  11406  gtso  11418  subf  11586  negne0i  11660  mulnzcnf  11989  infrenegsup  12327  neg1lt0  12335  nnne0  12399  halflt1  12590  nn0ssz  12743  3halfnz  12805  zeo  12812  numlt  12871  numltc  12872  le9lt10  12873  decle  12880  uzf  12995  xaddf  13381  xsubge0  13418  xmulf  13429  ixxf  13513  ixxssxr  13515  iooval2  13536  ioof  13605  unirnioo  13607  dfioo2  13608  fzval2  13669  fzf  13670  0nelfz1  13703  fz10  13705  fz00m1  13706  fzpreddisj  13734  4fvwrd4  13809  fzof  13817  fzo0  13845  fldiv4p1lem1div2  14002  fldiv4lem1div2  14004  om2uzoi  14125  faclbnd4lem1  14464  hashkf  14503  hashgval  14504  hashinf  14506  hashresfn  14511  hashnn0n0nn  14562  hashge3el3dif  14659  hash3tpde  14665  rev0  14941  s2dm  15069  f1oun2prg  15097  trclublem  15177  sqrt2gt1lt2  15470  limsupgord  15668  fclim  15749  fsumrelem  16003  ackbijnn  16026  incexclem  16034  incexc  16035  georeclim  16070  geoisumr  16076  0.999...  16079  ege2le3  16285  sin0  16346  ef01bndlem  16381  cos2bnd  16385  cos01gt0  16388  sincos2sgn  16391  sin4lt0  16392  rpnnen2lem3  16413  rpnnen2lem9  16419  rexpen  16425  cnso  16444  dvdslelem  16508  divalglem1  16593  divalglem5  16596  divalglem6  16597  divalglem10  16601  flodddiv4  16614  0bits  16638  sadcf  16652  sadcadd  16657  bitsshft  16674  smupf  16677  gcdf  16713  eucalgf  16787  2prm  16896  dfphi2  16980  pockthi  17114  prmrec  17129  vdwapf  17179  vdwlem6  17193  karatsuba  17290  1259lem5  17342  2503lem3  17346  4001lem4  17351  structcnvcnv  17360  structfn  17363  strleun  17364  imasvscafn  17738  xpsff1o  17768  xrge0base  17808  wunnat  18163  dfinito3  18209  dftermo3  18210  eldmcoa  18269  coapm  18275  catcfuccl  18322  catcxpccl  18410  yonedainv  18484  chnub  18825  smndex1bas  19134  smndex1n0mnd  19140  grpinvfvi  19222  mulgfvi  19312  ressmulgnnd  19317  symgsssg  19711  symgfisg  19712  psgnunilem5  19738  sylow3lem2  19872  oppglsm  19886  efgmf  19957  efgval  19961  efgsf  19973  0frgp  20023  dmdprd  20244  dprdval  20249  invrfval  20649  drngui  21016  rmodislmod  21235  lssintcl  21269  cnfldadd  21714  cnfldmul  21716  cnfldfunALT  21723  cnfld0  21732  cnfld1  21733  cnfldsub  21736  xrsds  21746  pzriprnglem4  21820  pzriprnglem9  21825  pzriprnglem14  21830  psgnghm  21916  zrhpsgnmhm  21920  ocv1  22015  dsmmbas2  22073  mplsubrglem  22341  opsrtoslem2  22395  evl1maprhm  22727  mdetralt  22953  maducoeval2  22985  eltpsi  23292  unitg  23315  fctop  23352  cctop  23354  ppttop  23355  epttop  23357  leordtvallem1  23558  leordtvallem2  23559  iccordt  23562  iscnp2  23587  discmp  23746  conncompcld  23782  1stcrestlem  23800  2ndcdisj  23805  topnlly  23840  disllycmp  23847  dis1stc  23848  txuni2  23914  xkotf  23934  dfac14lem  23966  prdstps  23978  txindis  23983  tx1stc  23999  xkohaus  24002  xkoptsub  24003  cnmpt1st  24017  cnmpt2nd  24018  ptcmpfi  24162  trfil1  24235  fin1aufil  24281  tgpconncompeqg  24461  tgpconncomp  24462  trust  24578  met1stc  24870  dscmet  24921  retopon  25112  cnfldtopon  25131  xrsxmet  25159  xrsmopn  25162  iimulcn  25289  icopnfhmeo  25294  iccpnfhmeo  25296  xrhmeo  25297  cnheiborlem  25305  lebnumii  25317  ishtpy  25323  htpycc  25331  pco1  25366  pcohtpylem  25370  pcopt  25373  pcopt2  25374  pcoass  25375  pcorevlem  25377  rrxcph  25743  rrx0el  25749  ovoliunlem3  25855  ovolicc1  25867  ovolicc2  25873  volf  25880  ioorf  25924  dyadf  25942  dyadmbl  25951  vitalilem5  25963  vitali  25964  mbfimaopnlem  26006  mbflimsup  26017  0plef  26023  i1fima  26029  i1fima2  26030  i1fd  26032  itg1ge0  26037  itg10  26039  i1f1lem  26040  i1fadd  26046  i1fmul  26047  i1fmulc  26054  mbfi1fseqlem5  26070  itg2addlem  26109  reldv  26220  dvbsss  26252  dvef  26330  lhop1lem  26363  deg1fvi  26433  plypf1  26561  coeeulem  26573  coeeu  26574  vieta1lem2  26664  aannenlem3  26687  aalioulem3  26691  dvradcnv  26778  pserulm  26779  pserdvlem2  26785  sinhalfpilem  26822  sincos4thpi  26872  sincos6thpi  26874  pige3ALT  26878  resinf1o  26894  tanord1  26895  tanregt0  26897  efabl  26908  relogrn  26919  dfrelog  26923  logi  26945  logneg  26946  logltb  26958  logcn  27005  logf1o2  27008  dvlog  27009  efopnlem2  27015  efopn  27016  logccv  27021  dvsqrt  27100  dvcnsqrt  27102  cxpcn3  27106  logblog  27150  angpined  27188  1cubr  27200  asinsin  27250  asin1  27252  reasinsin  27254  atan0  27266  atanbnd  27284  atan1  27286  log2cnv  27302  log2ub  27307  log2le1  27308  birthday  27312  amgmlem  27347  emcllem5  27357  emgt0  27364  harmonicbnd3  27365  ftalem3  27432  basellem4  27441  sgmf  27502  ppi1  27521  cht1  27522  vma1  27523  ppiltx  27534  sqff1o  27539  ppiublem1  27559  ppiublem2  27560  ppiub  27561  chtub  27569  dchreq  27615  bposlem7  27647  bposlem8  27648  bposlem9  27649  lgsdir2lem2  27683  lgsdir2lem3  27684  chebbnd1  27829  chto1ub  27833  chpo1ubb  27838  pntibndlem1  27946  nosgnn0  28045  ltssolem1  28062  bdayfo  28064  nolt02o  28082  nogt01o  28083  noetasuplem4  28123  noetainflem4  28127  cutbdaybnd2lim  28213  madeun  28300  cutsfo  28321  addsproplem2  28386  addsproplem7  28391  addsprop  28392  negsprop  28451  subsf  28480  mulsproplem13  28544  mulsproplem14  28545  mulsprop  28546  oniso  28687  n0cut  28750  bdayn0sf1o  28786  twocut  28839  bdaypw2n0bndlem  28879  bdayfinbndlem1  28883  0reno  28912  tgldimor  28995  tglnfn  29040  tgplnfn  29283  axlowdimlem4  29553  axlowdimlem16  29565  axlowdim  29569  upgrfi  29699  lfgrnloop  29733  lfuhgr1v0e  29865  usgrexmplef  29870  usgrres  29919  vdegp1bi  30148  vtxdginducedm1lem2  30151  dfpth2  30344  pthdlem2  30384  wpthswwlks2on  30583  0ewlk  30735  0pth  30746  konigsbergiedgw  30879  konigsberglem1  30883  konigsberglem2  30884  konigsberglem3  30885  konigsberglem4  30886  konigsberglem5  30887  ex-dif  31054  ex-un  31055  ex-in  31056  ex-fl  31078  avril1  31094  9p10ne21fool  31102  n0lplig  31115  cnidOLD  31214  cnnvm  31314  ipasslem8  31469  ipasslem10  31471  hvsubf  31647  normlem1  31742  normlem6  31747  normlem7  31748  norm-ii-i  31769  norm3adifii  31780  hilid  31793  hlimf  31869  hhssabloi  31894  hhssnv  31896  hhshsslem1  31899  shincli  31994  shsval2i  32019  shs0i  32081  chj0i  32087  chm1i  32088  chincli  32092  chdmm1i  32109  shjshsi  32124  chsup0  32180  h1de2bi  32186  spansnpji  32210  cmcmlem  32223  cmcmii  32229  cmcm2ii  32230  cmcm3ii  32231  pjidmi  32305  pjssmii  32313  pj0i  32325  pjocini  32330  mayetes3i  32361  df0op2  32384  hoaddcomi  32404  hoaddassi  32408  hocadddiri  32411  hocsubdiri  32412  hoaddridi  32418  ho0coi  32420  hoid1i  32421  hoid1ri  32422  hodseqi  32426  honegsubi  32428  adj1o  32526  hoddii  32621  lnopunilem1  32642  lnopunilem2  32643  nmcopexi  32659  nmcopex  32661  nmcoplb  32662  nmcfnexi  32683  nmcfnex  32685  nmcfnlb  32686  adjbd1o  32717  adjcoi  32732  nmopcoadji  32733  opsqrlem6  32777  pjsdii  32787  pjddii  32788  pjidmcoi  32809  pjtoi  32811  pjin1i  32824  pjclem1  32827  stji1i  32874  reuxfrdf  33159  iuninc  33227  fnresin  33290  rinvf1o  33296  suppss2f  33304  xppreima  33311  ofoprabco  33330  partfun2  33341  fressupp  33352  supppreima  33355  fsupprnfi  33356  gtiso  33365  df1stres  33368  df2ndres  33369  snct  33376  padct  33381  fsuppcurry1  33386  fsuppcurry2  33387  ffsrn  33390  fpwrelmapffs  33396  fzodif1  33454  nnindf  33481  nn0min  33482  dp2lt  33521  dp2ltsuc  33522  dp2ltc  33523  dplti  33541  dpmul  33549  dpmul4  33550  ressplusf  33594  xrsclat  33642  xrge00  33645  xrnarchi  33815  elrgspnlem2  33874  1fldgenq  33954  xrge0slmod  33979  zringfrac  34156  esplyind  34277  ply1degltdimlem  34324  ccfldsrarelvec  34373  ccfldextdgrr  34374  locfinreflem  34542  locfinref  34543  unicls  34605  sqsscirc1  34610  mhmhmeotmd  34629  raddcn  34631  xrge0iifiso  34637  xrge0iifhmeo  34638  lmxrge0  34654  cnzh  34670  rezh  34671  qqh0  34686  qqh1  34687  qqhre  34722  rrhre  34723  esumnul  34750  esum0  34751  esumsnf  34766  esumpfinvallem  34776  esumpfinvalf  34778  esumpcvgval  34780  esumcvgsum  34790  esumsup  34791  esumcvgre  34793  sigaclfu2  34823  dmsigagen  34847  ddemeas  34939  mbfmvolf  34968  br2base  34971  sibfof  35042  sitg0  35048  eulerpartlemt  35073  eulerpartgbij  35074  0rrv  35153  coinfliplem  35181  coinflipprob  35182  coinfliprv  35185  ballotlem2  35191  ballotlem4  35201  ballotlem5  35202  ballotlemi1  35205  ballotlem7  35238  ballotth  35240  signsplypnf  35249  signsply0  35250  signsw0g  35255  signswch  35260  signsvf0  35279  hashreprin  35319  reprfz1  35323  chtvalz  35328  hgt750lemd  35347  hgt750lem  35350  hgt750lem2  35351  bnj1098  35484  bnj1109  35487  bnj1131  35488  bnj1533  35552  bnj151  35577  bnj580  35613  bnj852  35621  bnj864  35622  bnj865  35623  bnj978  35649  bnj1021  35666  bnj907  35667  bnj1093  35680  bnj1145  35693  bnj1172  35701  bnj1174  35703  bnj1176  35705  bnj1186  35707  nfan1c  35773  xoromon  35794  rankfo  35817  0elscott  35837  fineqvac  35884  tz9.1regs  35902  axpowg  35914  gdlopcfvlem  35971  j0ltalephlem  36007  onvf1odlem4  36034  onvf1od  36035  srepdflem2  36086  subfacf  36107  subfacp1lem1  36111  subfacp1lem5  36116  subfacp1lem6  36117  subfacval3  36121  erdszelem2  36124  kur14lem4  36141  ioosconn  36179  iccllysconn  36182  satfn  36287  fmlaomn0  36322  gonan0  36324  goaln0  36325  elnanelprv  36361  msrfo  36478  mthmpps  36514  problem5  36601  quad3  36602  circum  36606  antnestALT  36626  axextprim  36644  axrepprim  36645  axunprim  36646  axinfprim  36649  axacprim  36650  bcneg1  36679  dfon2lem2  36724  dfon2lem4  36726  axextdfeq  36737  fobigcup  36840  snelsingles  36862  fullfunfnv  36888  fullfunfv  36889  rankaltopb  36922  rank0  37109  rankeq1o  37110  in-ax8  37191  fneer  37319  neibastop1  37325  nabi1i  37360  nabi2i  37361  limsucncmpi  37411  tz9.1ctco  37448  ttctr3  37461  ttcpwss  37481  knoppcnlem8  37544  knoppcnlem11  37547  cnndvlem1  37581  bj-consensusALT  37627  bj-sbidmOLD  37940  bj-n0i  38042  bj-snsetex  38054  bj-tagss  38071  bj-2upln0  38114  bj-2upln1upl  38115  bj-nuliota  38163  bj-axseprep  38181  bj-0int  38213  bj-elid5  38282  bj-inftyexpitaufo  38315  bj-pinftyccb  38334  bj-minftyccb  38338  bj-pinftynminfty  38340  bj-isrvec  38407  iccioo01  38442  f1omptsnlem  38451  mptsnunlem  38453  topdifinffinlem  38462  relowlpssretop  38479  1oequni2o  38483  imadifss  38715  tan2h  38727  poimirlem3  38733  poimirlem9  38739  poimirlem16  38746  poimirlem17  38747  poimirlem18  38748  poimirlem19  38749  poimirlem20  38750  poimirlem22  38752  poimirlem30  38760  mblfinlem1  38767  mblfinlem2  38768  ovoliunnfl  38772  voliunnfl  38774  itg2addnclem  38781  itg2addnclem2  38782  asindmre  38813  areacirclem1  38818  fdc  38871  cntotbnd  38922  heiborlem6  38942  rrnval  38953  reheibor  38965  rngosn3  39050  brcnvrabga  39466  cnvresrn  39472  moantr  39496  inxp2  39499  dfxrn2  39509  dfsucmap3  39587  dfpre4  39604  cnvcosseq  39651  refrelcosslem  39676  1cosscnvxrn  39689  redundss3  39836  refrelsredund3  39842  refrelredund3  39845  disjimeceqim  39928  eqvrel0  40013  eqvrelid  40016  prter2  40130  renegclALT  40212  mapdunirnN  42899  lcmeprodgcdi  43249  3factsumint2  43264  3factsumint3  43265  3factsumint4  43266  3factsumint  43267  lcmineqlem4  43274  3lexlogpow5ineq1  43296  3lexlogpow2ineq1  43300  dvrelogpow2b  43310  aks4d1p1p4  43313  aks4d1p8  43329  aks6d1c1  43358  aks6d1c2p2  43361  aks6d1c4  43366  2ap1caineq  43387  sticksstones1  43388  sticksstones2  43389  aks6d1c7lem2  43423  aks5lem3a  43431  aks5lem6  43434  unitscyglem2  43438  unitscyglem3  43439  sqdeccom12  43539  readvrec2  43605  readvcot  43608  resubf  43625  sn-0ne2  43650  sn-subf  43673  sn-nnne0  43717  sn-0lt1  43732  reneg1lt0  43737  rntrclfvOAI  43895  diophrw  43963  rabren3dioph  44015  pellexlem6  44034  pellex  44035  frmx  44113  frmy  44114  jm2.23  44196  jm2.27dlem3  44211  axac10  44233  pw2f1ocnv  44237  kelac2lem  44259  lmhmlnmsplit  44282  pwfi2f1o  44291  frlmpwfi  44293  insucid  44597  nla0003  44618  ifpbiidcor  44667  sucomisnotcard  44737  alephiso2  44751  alephiso3  44752  cnvnonrel  44780  rnnonrel  44783  resnonrel  44784  cononrel1  44786  cononrel2  44787  fvnonrel  44789  cnvcnvintabd  44792  cnvintabd  44795  rclexi  44807  rtrclex  44809  clcnvlem  44815  cnvrcl0  44817  dmtrcl  44819  rntrcl  44820  dfrtrcl5  44821  iunrelexp0  44894  dmtrclfvRP  44922  rntrclfv  44924  corcltrcl  44931  cotrclrcl  44934  0heALT  44975  frege54cor1a  45056  uneqsn  45217  clsk3nimkb  45232  int-sqdefd  45373  int-sqgeq0d  45378  rr-groth  45475  rr-grothprim  45476  rr-grothshort  45480  seff  45485  expgrowthi  45509  expgrowth  45511  binomcxplemnotnn0  45532  ee233  45693  ax6e2nd  45732  in1  45745  dfvd2ani  45757  dfvd2i  45759  dfvd3i  45766  dfvd3ani  45769  e0bi  45949  uun2221  45986  uun2221p1  45987  uun2221p2  45988  en3lpVD  46018  relopabVD  46074  ax6e2ndVD  46081  ax6e2ndALT  46103  permaxpow  46194  hfstructhf  46228  hfstructcan  46229  pssnssi  46321  nnf1oxpnn  46415  icof  46437  fnmptif  46482  rn1st  46490  negpilt0  46502  xrgtso  46562  supxrleubrnmptf  46666  xrpnf  46700  rexanuz2nf  46707  ioontr  46728  iccdifioo  46732  iccdifprioo  46733  uzinico2  46778  fsummulc1f  46788  fsumiunss  46792  fnlimfvre2  46892  limsupreuz  46952  limsup10ex  46988  icccncfext  47102  dvcosre  47127  dvsinax  47128  ioodvbdlimc1lem2  47147  ioodvbdlimc2lem  47149  dvmptmulf  47152  dvnmul  47158  dvmptfprodlem  47159  dvnprodlem2  47162  stoweidlem1  47216  stoweidlem26  47241  stoweidlem34  47249  stoweidlem44  47259  stoweid  47278  stirlinglem5  47293  dirkercncflem1  47318  fourierdlem44  47366  fourierdlem56  47377  fourierdlem62  47383  fourierdlem89  47410  fourierdlem91  47412  fourierdlem100  47421  fourierdlem102  47423  fourierdlem103  47424  fourierdlem104  47425  fourierdlem108  47429  fourierdlem112  47433  fourierdlem114  47435  fouriersw  47446  rrndistlt  47505  gsumge0cl  47586  sge0tsms  47595  sge0ltfirpmpt2  47641  ovn0  47781  hoidmv1le  47809  hoidmvle  47815  ovnsubadd2lem  47860  ovolval4lem1  47864  vonioolem2  47896  smflimlem3  47988  nsssmfmbf  47994  chnerlem1  48097  sqrtnzqaa  48119  numtowerdt  48121  goldrasin  48134  goldrapos  48135  goldratmolem4  48140  goldratval  48141  sqrtnpoly  48148  axorbtnotaiffb  48178  axorbciffatcxorb  48180  abnotbtaxb  48190  euabsneu  48303  ceilhalf1  48613  sprval  48766  fmtnoinf  48826  nprmdvdsfacm1lem2  48911  ppivalnnnprmge6  48916  ppivalnn4  48917  ppivalnn  48922  1nevenALTV  48994  nfermltl8rev  49045  nfermltl2rev  49046  nnsum3primes4  49091  tgblthelfgott  49118  tgoldbachlt  49119  cycl3grtri  49250  isubgr3stgrlem3  49271  usgrexmpl1lem  49324  usgrexmpl2lem  49329  usgrexmpl2trifr  49340  gpgprismgr4cycllem7  49404  ldepslinc  49826  ackval42  50013  rrx2plordso  50042  vsn  50128  dmtposss  50194  sepfsepc  50247  basresposfo  50297  rescofuf  50413  oppff1  50469  idfth  50479  idsubc  50481  fuco2eld2  50641  fuco22a  50677  setc1onsubc  50945  par2catid  50972  parswapfunc  50983  alimp-no-surprise  51157  aacllem  51219  3elfz13  51225  veronesevrowd  51259  veroquadmodzerod  51264  veroquadnolindfd  51265  veroquaddetzerod  51266  amgmwlem  51267  amgmlemALT  51268