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  1641  nic-dfim  1701  nic-dfneg  1702  nic-mp  1703  nic-mpALT  1704  tbw-negdf  1731  rb-imdf  1782  nfri  1821  mpgbi  1830  19.35i  1910  nfim1  2235  19.36i  2267  ax6  2413  sbie  2531  datisi  2704  disamis  2705  dimatis  2712  fresison  2713  bamalip  2716  axi12  2730  eqcomi  2769  eqtri  2783  eleqtri  2858  nfnfc  2934  neii  2957  necomi  3009  neeqtri  3027  neli  3063  nrex  3090  rexlimi  3262  eueqi  3666  euxfr2w  3677  euxfr2  3679  reuxfrd  3705  cdeqri  3723  sseqtri  3956  pssn2lp  4032  ssini  4136  equncomi  4159  unssi  4189  unabs  4210  inabs  4211  dfin4  4223  vn0OLD  4291  inindif  4323  difidALT  4325  ab0orv  4331  ab0orvALT  4332  difin0  4427  pwundif  4582  snid  4619  rabrsn  4681  iinrab2  5027  symdifv  5045  rintn0  5068  breqtri  5129  axsepgfromrep  5246  ax6vsep  5256  notsep  5324  zfpow  5327  dtruALT2  5331  dtruALT  5349  reusv2lem4  5362  dtru  5404  el.OLD  5406  op1stb  5439  copsexgwOLD  5460  uniop  5487  rn0  5907  dmresi  6043  somincom  6127  cnvcnv  6183  elid  6193  cnvimassrndmOLD  6199  rescnvcnv  6205  cnvcnvres  6206  cocnvcnv2  6260  cores2  6261  co01  6263  cnviin  6289  predres  6342  iota4an  6520  fnopab  6677  mpt0  6681  fnmpti  6682  f1cnvcnv  6789  f1ovi  6865  eliman0  6922  fvco4i  6987  cnvimainrn  7066  fmpti  7112  funiunfv  7252  oprabss  7528  relmptopab  7671  zfun  7752  tfinds2  7875  omon  7889  2nd0  8008  f1stres  8025  f2ndres  8026  cnvoprab  8071  relmpoopab  8106  df1st2  8111  df2nd2  8112  fsplit  8130  frpoins3xpg  8159  frpoins3xp3g  8160  poxp2  8162  poseq  8177  reldmtpos  8254  dftpos4  8265  tpostpos  8266  tpos0  8276  frrlem4  8310  smo0  8369  tfrlem14  8402  tfrlem16  8404  rdgsucg  8434  rdglimg  8436  frfnom  8446  tz7.48lem  8453  oawordeulem  8565  uniixp  8952  dfdom2  9008  ssdomg  9030  xpcomf1o  9088  sbthlem5  9113  sdom0  9131  limensuci  9175  1sdom2  9242  fiint  9321  fidomdm  9326  residfi  9330  mptfi  9343  fisn  9422  dffi3  9426  ordtypelem6  9520  ordtypelem7  9521  wemaplem2  9544  harwdom  9588  nelaneqOLD  9600  suc11reg  9623  zfinf  9643  axinf2  9644  noinfep  9664  cantnfvalf  9669  cantnflt  9676  cantnf0  9679  cantnf  9697  ttrclco  9722  tz9.1c  9734  tc2  9744  setinds  9753  r111  9785  r1tr2  9787  r1ordg  9788  r1sssuc  9793  r1val1  9796  tz9.13  9801  r1elssi  9816  pwwf  9818  rankopb  9869  rankeq0b  9879  ranksuc  9885  rankmapu  9898  rankxplim3  9901  rankxpsuc  9902  hfuniOLD  9928  cp  9957  karden  9962  kardenOLD  9963  card0  10042  cardlim  10056  cardom  10070  infxpenlem  10095  alephsuc2  10162  alephgeom  10164  unialeph  10183  dfac4  10204  dfacacn  10223  dju1dif  10254  dju1p1e2  10255  infdju1  10271  ackbij1lem13  10312  ackbij2  10323  cf0  10331  cfsuc  10338  cfom  10345  cfslb2n  10349  ominf4  10393  fin23lem17  10419  fin23lem28  10421  fin23lem30  10423  fin23lem31  10424  fin23lem40  10432  isfin1-3  10467  dfacfin7  10480  fin1a2lem6  10486  itunitc1  10501  axcc3  10519  dcomex  10528  axdc2lem  10529  axcclem  10538  zfac  10541  ac3  10543  ackm  10546  axac2  10547  axac  10548  axaci  10549  cardeqv  10550  numth2  10552  numth  10553  dmct  10605  dmctOLD  10606  brdom3  10610  fin71ac  10615  cardf  10637  aleph1  10659  cfpwsdom  10672  smobeth  10674  zfcndrep  10702  zfcndpow  10704  zfcndac  10707  gch2  10763  wunex3  10829  tskpr  10858  inar1  10863  rankcf  10865  tskcard  10869  tskuni  10871  grothpw  10914  axgroth4  10920  grothprim  10922  inaprc  10924  dmaddpi  10978  dmmulpi  10979  1lt2pi  10993  addpqf  11032  mulpqf  11034  1lt2nq  11061  supsrlem  11199  ssxr  11382  gtso  11394  subf  11562  negne0i  11636  mulnzcnf  11965  infrenegsup  12303  neg1lt0  12311  nnne0  12375  halflt1  12566  nn0ssz  12719  3halfnz  12781  zeo  12788  numlt  12847  numltc  12848  le9lt10  12849  decle  12856  uzf  12971  xaddf  13357  xsubge0  13394  xmulf  13405  ixxf  13489  ixxssxr  13491  iooval2  13512  ioof  13581  unirnioo  13583  dfioo2  13584  fzval2  13645  fzf  13646  0nelfz1  13679  fz10  13681  fz00m1  13682  fzpreddisj  13710  4fvwrd4  13785  fzof  13793  fzo0  13821  fldiv4p1lem1div2  13978  fldiv4lem1div2  13980  om2uzoi  14101  faclbnd4lem1  14440  hashkf  14479  hashgval  14480  hashinf  14482  hashresfn  14487  hashnn0n0nn  14538  hashge3el3dif  14635  hash3tpde  14641  rev0  14917  s2dm  15045  f1oun2prg  15073  trclublem  15153  sqrt2gt1lt2  15446  limsupgord  15644  fclim  15725  fsumrelem  15979  ackbijnn  16002  incexclem  16010  incexc  16011  georeclim  16046  geoisumr  16052  0.999...  16055  ege2le3  16261  sin0  16322  ef01bndlem  16357  cos2bnd  16361  cos01gt0  16364  sincos2sgn  16367  sin4lt0  16368  rpnnen2lem3  16389  rpnnen2lem9  16395  rexpen  16401  cnso  16420  dvdslelem  16484  divalglem1  16569  divalglem5  16572  divalglem6  16573  divalglem10  16577  flodddiv4  16590  0bits  16614  sadcf  16628  sadcadd  16633  bitsshft  16650  smupf  16653  gcdf  16689  eucalgf  16763  2prm  16872  dfphi2  16956  pockthi  17090  prmrec  17105  vdwapf  17155  vdwlem6  17169  karatsuba  17266  1259lem5  17318  2503lem3  17322  4001lem4  17327  structcnvcnv  17336  structfn  17339  strleun  17340  imasvscafn  17714  xpsff1o  17744  xrge0base  17784  wunnat  18139  dfinito3  18185  dftermo3  18186  eldmcoa  18245  coapm  18251  catcfuccl  18298  catcxpccl  18386  yonedainv  18460  chnub  18801  smndex1bas  19110  smndex1n0mnd  19116  grpinvfvi  19198  mulgfvi  19288  ressmulgnnd  19293  symgsssg  19686  symgfisg  19687  psgnunilem5  19713  sylow3lem2  19847  oppglsm  19861  efgmf  19932  efgval  19936  efgsf  19948  0frgp  19998  dmdprd  20219  dprdval  20224  invrfval  20624  drngui  20991  rmodislmod  21210  lssintcl  21244  cnfldadd  21689  cnfldmul  21691  cnfldfunALT  21698  cnfld0  21707  cnfld1  21708  cnfldsub  21711  xrsds  21721  pzriprnglem4  21795  pzriprnglem9  21800  pzriprnglem14  21805  psgnghm  21891  zrhpsgnmhm  21895  ocv1  21990  dsmmbas2  22048  mplsubrglem  22316  opsrtoslem2  22370  evl1maprhm  22702  mdetralt  22928  maducoeval2  22960  eltpsi  23267  unitg  23290  fctop  23327  cctop  23329  ppttop  23330  epttop  23332  leordtvallem1  23533  leordtvallem2  23534  iccordt  23537  iscnp2  23562  discmp  23721  conncompcld  23757  1stcrestlem  23775  2ndcdisj  23780  topnlly  23815  disllycmp  23822  dis1stc  23823  txuni2  23889  xkotf  23909  dfac14lem  23941  prdstps  23953  txindis  23958  tx1stc  23974  xkohaus  23977  xkoptsub  23978  cnmpt1st  23992  cnmpt2nd  23993  ptcmpfi  24137  trfil1  24210  fin1aufil  24256  tgpconncompeqg  24436  tgpconncomp  24437  trust  24553  met1stc  24845  dscmet  24896  retopon  25087  cnfldtopon  25106  xrsxmet  25134  xrsmopn  25137  iimulcn  25264  icopnfhmeo  25269  iccpnfhmeo  25271  xrhmeo  25272  cnheiborlem  25280  lebnumii  25292  ishtpy  25298  htpycc  25306  pco1  25341  pcohtpylem  25345  pcopt  25348  pcopt2  25349  pcoass  25350  pcorevlem  25352  rrxcph  25718  rrx0el  25724  ovoliunlem3  25830  ovolicc1  25842  ovolicc2  25848  volf  25855  ioorf  25899  dyadf  25917  dyadmbl  25926  vitalilem5  25938  vitali  25939  mbfimaopnlem  25981  mbflimsup  25992  0plef  25998  i1fima  26004  i1fima2  26005  i1fd  26007  itg1ge0  26012  itg10  26014  i1f1lem  26015  i1fadd  26021  i1fmul  26022  i1fmulc  26029  mbfi1fseqlem5  26045  itg2addlem  26084  reldv  26195  dvbsss  26227  dvef  26305  lhop1lem  26338  deg1fvi  26408  plypf1  26536  coeeulem  26548  coeeu  26549  vieta1lem2  26639  aannenlem3  26662  aalioulem3  26666  dvradcnv  26753  pserulm  26754  pserdvlem2  26760  sinhalfpilem  26797  sincos4thpi  26847  sincos6thpi  26849  pige3ALT  26853  resinf1o  26869  tanord1  26870  tanregt0  26872  efabl  26883  relogrn  26894  dfrelog  26898  logi  26920  logneg  26921  logltb  26933  logcn  26980  logf1o2  26983  dvlog  26984  efopnlem2  26990  efopn  26991  logccv  26996  dvsqrt  27075  dvcnsqrt  27077  cxpcn3  27081  logblog  27125  angpined  27163  1cubr  27175  asinsin  27225  asin1  27227  reasinsin  27229  atan0  27241  atanbnd  27259  atan1  27261  log2cnv  27277  log2ub  27282  log2le1  27283  birthday  27287  amgmlem  27322  emcllem5  27332  emgt0  27339  harmonicbnd3  27340  ftalem3  27407  basellem4  27416  sgmf  27477  ppi1  27496  cht1  27497  vma1  27498  ppiltx  27509  sqff1o  27514  ppiublem1  27534  ppiublem2  27535  ppiub  27536  chtub  27544  dchreq  27590  bposlem7  27622  bposlem8  27623  bposlem9  27624  lgsdir2lem2  27658  lgsdir2lem3  27659  chebbnd1  27804  chto1ub  27808  chpo1ubb  27813  pntibndlem1  27921  nosgnn0  28020  ltssolem1  28037  bdayfo  28039  nolt02o  28057  nogt01o  28058  noetasuplem4  28098  noetainflem4  28102  cutbdaybnd2lim  28188  madeun  28275  cutsfo  28296  addsproplem2  28361  addsproplem7  28366  addsprop  28367  negsprop  28426  subsf  28455  mulsproplem13  28519  mulsproplem14  28520  mulsprop  28521  oniso  28662  n0cut  28725  bdayn0sf1o  28761  twocut  28814  bdaypw2n0bndlem  28854  bdayfinbndlem1  28858  0reno  28887  tgldimor  28970  tglnfn  29015  tgplnfn  29258  axlowdimlem4  29528  axlowdimlem16  29540  axlowdim  29544  upgrfi  29674  lfgrnloop  29708  lfuhgr1v0e  29840  usgrexmplef  29845  usgrres  29894  vdegp1bi  30123  vtxdginducedm1lem2  30126  dfpth2  30319  pthdlem2  30359  wpthswwlks2on  30558  0ewlk  30710  0pth  30721  konigsbergiedgw  30854  konigsberglem1  30858  konigsberglem2  30859  konigsberglem3  30860  konigsberglem4  30861  konigsberglem5  30862  ex-dif  31029  ex-un  31030  ex-in  31031  ex-fl  31053  avril1  31069  9p10ne21fool  31077  n0lplig  31090  cnidOLD  31189  cnnvm  31289  ipasslem8  31444  ipasslem10  31446  hvsubf  31622  normlem1  31717  normlem6  31722  normlem7  31723  norm-ii-i  31744  norm3adifii  31755  hilid  31768  hlimf  31844  hhssabloi  31869  hhssnv  31871  hhshsslem1  31874  shincli  31969  shsval2i  31994  shs0i  32056  chj0i  32062  chm1i  32063  chincli  32067  chdmm1i  32084  shjshsi  32099  chsup0  32155  h1de2bi  32161  spansnpji  32185  cmcmlem  32198  cmcmii  32204  cmcm2ii  32205  cmcm3ii  32206  pjidmi  32280  pjssmii  32288  pj0i  32300  pjocini  32305  mayetes3i  32336  df0op2  32359  hoaddcomi  32379  hoaddassi  32383  hocadddiri  32386  hocsubdiri  32387  hoaddridi  32393  ho0coi  32395  hoid1i  32396  hoid1ri  32397  hodseqi  32401  honegsubi  32403  adj1o  32501  hoddii  32596  lnopunilem1  32617  lnopunilem2  32618  nmcopexi  32634  nmcopex  32636  nmcoplb  32637  nmcfnexi  32658  nmcfnex  32660  nmcfnlb  32661  adjbd1o  32692  adjcoi  32707  nmopcoadji  32708  opsqrlem6  32752  pjsdii  32762  pjddii  32763  pjidmcoi  32784  pjtoi  32786  pjin1i  32799  pjclem1  32802  stji1i  32849  reuxfrdf  33134  iuninc  33202  fnresin  33265  rinvf1o  33271  suppss2f  33279  xppreima  33286  ofoprabco  33305  partfun2  33317  fressupp  33328  supppreima  33331  fsupprnfi  33332  gtiso  33341  df1stres  33344  df2ndres  33345  snct  33352  padct  33357  fsuppcurry1  33362  fsuppcurry2  33363  ffsrn  33366  fpwrelmapffs  33372  fzodif1  33430  nnindf  33457  nn0min  33458  dp2lt  33497  dp2ltsuc  33498  dp2ltc  33499  dplti  33517  dpmul  33525  dpmul4  33526  ressplusf  33570  xrsclat  33618  xrge00  33621  xrnarchi  33791  elrgspnlem2  33850  1fldgenq  33930  xrge0slmod  33955  zringfrac  34132  esplyind  34253  ply1degltdimlem  34300  ccfldsrarelvec  34349  ccfldextdgrr  34350  locfinreflem  34518  locfinref  34519  unicls  34581  sqsscirc1  34586  mhmhmeotmd  34605  raddcn  34607  xrge0iifiso  34613  xrge0iifhmeo  34614  lmxrge0  34630  cnzh  34646  rezh  34647  qqh0  34662  qqh1  34663  qqhre  34698  rrhre  34699  esumnul  34726  esum0  34727  esumsnf  34742  esumpfinvallem  34752  esumpfinvalf  34754  esumpcvgval  34756  esumcvgsum  34766  esumsup  34767  esumcvgre  34769  sigaclfu2  34799  dmsigagen  34823  ddemeas  34915  mbfmvolf  34944  br2base  34947  sibfof  35018  sitg0  35024  eulerpartlemt  35049  eulerpartgbij  35050  0rrv  35129  coinfliplem  35157  coinflipprob  35158  coinfliprv  35161  ballotlem2  35167  ballotlem4  35177  ballotlem5  35178  ballotlemi1  35181  ballotlem7  35214  ballotth  35216  signsplypnf  35225  signsply0  35226  signsw0g  35231  signswch  35236  signsvf0  35255  hashreprin  35295  reprfz1  35299  chtvalz  35304  hgt750lemd  35323  hgt750lem  35326  hgt750lem2  35327  bnj1098  35460  bnj1109  35463  bnj1131  35464  bnj1533  35528  bnj151  35553  bnj580  35589  bnj852  35597  bnj864  35598  bnj865  35599  bnj978  35625  bnj1021  35642  bnj907  35643  bnj1093  35656  bnj1145  35669  bnj1172  35677  bnj1174  35679  bnj1176  35681  bnj1186  35683  nfan1c  35749  xoromon  35767  rankfo  35787  fineqvac  35840  tz9.1regs  35858  axpowg  35870  j0ltalephlem  35946  onvf1odlem4  35953  onvf1od  35954  srepdflem2  36005  subfacf  36026  subfacp1lem1  36030  subfacp1lem5  36035  subfacp1lem6  36036  subfacval3  36040  erdszelem2  36043  kur14lem4  36060  ioosconn  36098  iccllysconn  36101  satfn  36206  fmlaomn0  36241  gonan0  36243  goaln0  36244  elnanelprv  36280  msrfo  36397  mthmpps  36433  problem5  36520  quad3  36521  circum  36525  antnestALT  36545  axextprim  36558  axrepprim  36559  axunprim  36560  axinfprim  36563  axacprim  36564  bcneg1  36593  dfon2lem2  36638  dfon2lem4  36640  axextdfeq  36651  fobigcup  36754  snelsingles  36776  fullfunfnv  36802  fullfunfv  36803  rankaltopb  36836  rank0  37023  rankeq1o  37024  in-ax8  37105  fneer  37233  neibastop1  37239  nabi1i  37274  nabi2i  37275  limsucncmpi  37325  tz9.1ctco  37362  ttctr3  37375  ttcpwss  37395  knoppcnlem8  37458  knoppcnlem11  37461  cnndvlem1  37495  bj-consensusALT  37541  bj-sbidmOLD  37854  bj-n0i  37956  bj-snsetex  37968  bj-tagss  37985  bj-2upln0  38028  bj-2upln1upl  38029  bj-nuliota  38064  bj-axseprep  38082  bj-0int  38114  bj-elid5  38183  bj-inftyexpitaufo  38216  bj-pinftyccb  38235  bj-minftyccb  38239  bj-pinftynminfty  38241  bj-isrvec  38308  iccioo01  38343  f1omptsnlem  38352  mptsnunlem  38354  topdifinffinlem  38363  relowlpssretop  38380  1oequni2o  38384  imadifss  38616  tan2h  38628  poimirlem3  38634  poimirlem9  38640  poimirlem16  38647  poimirlem17  38648  poimirlem18  38649  poimirlem19  38650  poimirlem20  38651  poimirlem22  38653  poimirlem30  38661  mblfinlem1  38668  mblfinlem2  38669  ovoliunnfl  38673  voliunnfl  38675  itg2addnclem  38682  itg2addnclem2  38683  asindmre  38714  areacirclem1  38719  fdc  38772  cntotbnd  38823  heiborlem6  38843  rrnval  38854  reheibor  38866  rngosn3  38951  brcnvrabga  39367  cnvresrn  39373  moantr  39397  inxp2  39400  dfxrn2  39410  dfsucmap3  39488  dfpre4  39505  cnvcosseq  39552  refrelcosslem  39577  1cosscnvxrn  39590  redundss3  39737  refrelsredund3  39743  refrelredund3  39746  disjimeceqim  39829  eqvrel0  39914  eqvrelid  39917  prter2  40031  renegclALT  40113  mapdunirnN  42800  lcmeprodgcdi  43150  3factsumint2  43165  3factsumint3  43166  3factsumint4  43167  3factsumint  43168  lcmineqlem4  43175  3lexlogpow5ineq1  43197  3lexlogpow2ineq1  43201  dvrelogpow2b  43211  aks4d1p1p4  43214  aks4d1p8  43230  aks6d1c1  43259  aks6d1c2p2  43262  aks6d1c4  43267  2ap1caineq  43288  sticksstones1  43289  sticksstones2  43290  aks6d1c7lem2  43324  aks5lem3a  43332  aks5lem6  43335  unitscyglem2  43339  unitscyglem3  43340  sqdeccom12  43439  readvrec2  43505  readvcot  43508  resubf  43525  sn-0ne2  43550  sn-subf  43573  sn-nnne0  43617  sn-0lt1  43632  reneg1lt0  43637  rntrclfvOAI  43795  diophrw  43863  rabren3dioph  43915  pellexlem6  43934  pellex  43935  frmx  44013  frmy  44014  jm2.23  44096  jm2.27dlem3  44111  axac10  44133  pw2f1ocnv  44137  kelac2lem  44159  lmhmlnmsplit  44182  pwfi2f1o  44191  frlmpwfi  44193  insucid  44498  nla0003  44519  ifpbiidcor  44568  sucomisnotcard  44638  alephiso2  44652  alephiso3  44653  cnvnonrel  44681  rnnonrel  44684  resnonrel  44685  cononrel1  44687  cononrel2  44688  fvnonrel  44690  cnvcnvintabd  44693  cnvintabd  44696  rclexi  44708  rtrclex  44710  clcnvlem  44716  cnvrcl0  44718  dmtrcl  44720  rntrcl  44721  dfrtrcl5  44722  iunrelexp0  44795  dmtrclfvRP  44823  rntrclfv  44825  corcltrcl  44832  cotrclrcl  44835  0heALT  44876  frege54cor1a  44957  uneqsn  45118  clsk3nimkb  45133  int-sqdefd  45274  int-sqgeq0d  45279  rr-groth  45376  rr-grothprim  45377  rr-grothshort  45381  seff  45386  expgrowthi  45410  expgrowth  45412  binomcxplemnotnn0  45433  ee233  45595  ax6e2nd  45634  in1  45647  dfvd2ani  45659  dfvd2i  45661  dfvd3i  45668  dfvd3ani  45671  e0bi  45851  uun2221  45888  uun2221p1  45889  uun2221p2  45890  en3lpVD  45920  relopabVD  45976  ax6e2ndVD  45983  ax6e2ndALT  46005  permaxpow  46092  hfstructhf  46123  hfstructcan  46124  pssnssi  46209  nnf1oxpnn  46303  icof  46325  fnmptif  46370  rn1st  46378  negpilt0  46390  xrgtso  46450  supxrleubrnmptf  46554  xrpnf  46588  rexanuz2nf  46595  ioontr  46616  iccdifioo  46620  iccdifprioo  46621  uzinico2  46666  fsummulc1f  46676  fsumiunss  46680  fnlimfvre2  46780  limsupreuz  46840  limsup10ex  46876  icccncfext  46990  dvcosre  47015  dvsinax  47016  ioodvbdlimc1lem2  47035  ioodvbdlimc2lem  47037  dvmptmulf  47040  dvnmul  47046  dvmptfprodlem  47047  dvnprodlem2  47050  stoweidlem1  47104  stoweidlem26  47129  stoweidlem34  47137  stoweidlem44  47147  stoweid  47166  stirlinglem5  47181  dirkercncflem1  47206  fourierdlem44  47254  fourierdlem56  47265  fourierdlem62  47271  fourierdlem89  47298  fourierdlem91  47300  fourierdlem100  47309  fourierdlem102  47311  fourierdlem103  47312  fourierdlem104  47313  fourierdlem108  47317  fourierdlem112  47321  fourierdlem114  47323  fouriersw  47334  rrndistlt  47393  gsumge0cl  47474  sge0tsms  47483  sge0ltfirpmpt2  47529  ovn0  47669  hoidmv1le  47697  hoidmvle  47703  ovnsubadd2lem  47748  ovolval4lem1  47752  vonioolem2  47784  smflimlem3  47876  nsssmfmbf  47882  chnerlem1  47985  sqrtnzqaa  48007  numtowerdt  48009  goldrasin  48022  goldrapos  48023  goldratmolem4  48028  goldratval  48029  sqrtnpoly  48036  axorbtnotaiffb  48066  axorbciffatcxorb  48068  abnotbtaxb  48078  euabsneu  48191  ceilhalf1  48501  sprval  48654  fmtnoinf  48714  nprmdvdsfacm1lem2  48799  ppivalnnnprmge6  48804  ppivalnn4  48805  ppivalnn  48810  1nevenALTV  48882  nfermltl8rev  48933  nfermltl2rev  48934  nnsum3primes4  48979  tgblthelfgott  49006  tgoldbachlt  49007  cycl3grtri  49138  isubgr3stgrlem3  49159  usgrexmpl1lem  49212  usgrexmpl2lem  49217  usgrexmpl2trifr  49228  gpgprismgr4cycllem7  49292  ldepslinc  49714  ackval42  49901  rrx2plordso  49930  vsn  50016  dmtposss  50082  sepfsepc  50135  basresposfo  50185  rescofuf  50301  oppff1  50357  idfth  50367  idsubc  50369  fuco2eld2  50529  fuco22a  50565  setc1onsubc  50833  par2catid  50860  parswapfunc  50871  alimp-no-surprise  51045  aacllem  51107  3elfz13  51113  veronesevrowd  51147  veroquadmodzerod  51152  veroquadnolindfd  51153  veroquaddetzerod  51154  amgmwlem  51155  amgmlemALT  51156