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  2236  19.36i  2268  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  3064  nrex  3091  rexlimi  3263  eueqi  3667  euxfr2w  3678  euxfr2  3680  reuxfrd  3706  cdeqri  3724  sseqtri  3979  pssn2lp  4053  equncomi  4107  unssi  4137  ssini  4185  unabs  4211  inabs  4212  dfin4  4224  vn0OLD  4292  inindif  4324  difidALT  4326  ab0orv  4332  ab0orvALT  4333  difin0  4428  pwundif  4582  snid  4623  rabrsn  4685  iinrab2  5028  symdifv  5046  rintn0  5069  breqtri  5130  axsepgfromrep  5247  ax6vsep  5257  notsep  5325  zfpow  5328  dtruALT2  5332  dtruALT  5350  reusv2lem4  5363  dtru  5405  el.OLD  5407  op1stb  5440  copsexgwOLD  5461  uniop  5488  rn0  5908  dmresi  6046  somincom  6126  cnvimassrndm  6141  cnvcnv  6183  elid  6191  rescnvcnv  6198  cnvcnvres  6199  cocnvcnv2  6253  cores2  6254  co01  6256  cnviin  6282  predres  6335  iota4an  6513  fnopab  6669  mpt0  6673  fnmpti  6674  f1cnvcnv  6781  f1ovi  6857  eliman0  6914  fvco4i  6979  cnvimainrn  7058  fmpti  7104  funiunfv  7244  oprabss  7520  relmptopab  7663  zfun  7741  tfinds2  7864  omon  7878  2nd0  7997  f1stres  8014  f2ndres  8015  cnvoprab  8060  relmpoopab  8094  df1st2  8098  df2nd2  8099  fsplit  8117  frpoins3xpg  8141  frpoins3xp3g  8142  poxp2  8144  poseq  8159  reldmtpos  8235  dftpos4  8246  tpostpos  8247  tpos0  8257  frrlem4  8291  smo0  8350  tfrlem14  8383  tfrlem16  8385  rdgsucg  8415  rdglimg  8417  frfnom  8427  tz7.48lem  8434  oawordeulem  8546  uniixp  8933  dfdom2  8989  ssdomg  9011  xpcomf1o  9069  sbthlem5  9094  sdom0  9112  limensuci  9156  1sdom2  9223  fiint  9302  fidomdm  9307  residfi  9311  mptfi  9324  fisn  9403  dffi3  9407  ordtypelem6  9501  ordtypelem7  9502  wemaplem2  9525  harwdom  9569  nelaneqOLD  9581  suc11reg  9604  zfinf  9624  axinf2  9625  noinfep  9645  cantnfvalf  9650  cantnflt  9657  cantnf0  9660  cantnf  9678  ttrclco  9703  tz9.1c  9715  tc2  9725  setinds  9734  r111  9765  r1tr2  9767  r1ordg  9768  r1sssuc  9773  r1val1  9776  tz9.13  9781  r1elssi  9795  pwwf  9797  rankopb  9847  rankeq0b  9857  ranksuc  9863  rankmapu  9876  rankxplim3  9879  rankxpsuc  9880  hfuniOLD  9906  cp  9935  karden  9940  kardenOLD  9941  card0  10020  cardlim  10034  cardom  10048  infxpenlem  10073  alephsuc2  10140  alephgeom  10142  unialeph  10161  dfac4  10182  dfacacn  10201  dju1dif  10232  dju1p1e2  10233  infdju1  10249  ackbij1lem13  10290  ackbij2  10301  cf0  10309  cfsuc  10316  cfom  10323  cfslb2n  10327  ominf4  10371  fin23lem17  10397  fin23lem28  10399  fin23lem30  10401  fin23lem31  10402  fin23lem40  10410  isfin1-3  10445  dfacfin7  10458  fin1a2lem6  10464  itunitc1  10479  axcc3  10497  dcomex  10506  axdc2lem  10507  axcclem  10516  zfac  10519  ac3  10521  ackm  10524  axac2  10525  axac  10526  axaci  10527  cardeqv  10528  numth2  10530  numth  10531  dmct  10583  dmctOLD  10584  brdom3  10588  fin71ac  10593  cardf  10615  aleph1  10637  cfpwsdom  10650  smobeth  10652  zfcndrep  10680  zfcndpow  10682  zfcndac  10685  gch2  10741  wunex3  10807  tskpr  10836  inar1  10841  rankcf  10843  tskcard  10847  tskuni  10849  grothpw  10892  axgroth4  10898  grothprim  10900  inaprc  10902  dmaddpi  10956  dmmulpi  10957  1lt2pi  10971  addpqf  11010  mulpqf  11012  1lt2nq  11039  supsrlem  11177  ssxr  11360  gtso  11372  subf  11540  negne0i  11614  mulnzcnf  11943  infrenegsup  12281  neg1lt0  12289  nnne0  12353  halflt1  12544  nn0ssz  12697  3halfnz  12759  zeo  12766  numlt  12825  numltc  12826  le9lt10  12827  decle  12834  uzf  12949  xaddf  13335  xsubge0  13372  xmulf  13383  ixxf  13467  ixxssxr  13469  iooval2  13490  ioof  13559  unirnioo  13561  dfioo2  13562  fzval2  13623  fzf  13624  0nelfz1  13656  fz10  13658  fz00m1  13659  fzpreddisj  13687  4fvwrd4  13762  fzof  13770  fzo0  13798  fldiv4p1lem1div2  13955  fldiv4lem1div2  13957  om2uzoi  14078  faclbnd4lem1  14417  hashkf  14456  hashgval  14457  hashinf  14459  hashresfn  14464  hashnn0n0nn  14515  hashge3el3dif  14612  hash3tpde  14618  rev0  14893  s2dm  15021  f1oun2prg  15048  trclublem  15128  sqrt2gt1lt2  15421  limsupgord  15619  fclim  15700  fsumrelem  15954  ackbijnn  15977  incexclem  15985  incexc  15986  arisum2  16010  georeclim  16021  geoisumr  16027  0.999...  16030  ege2le3  16236  sin0  16297  ef01bndlem  16332  cos2bnd  16336  cos01gt0  16339  sincos2sgn  16342  sin4lt0  16343  rpnnen2lem3  16364  rpnnen2lem9  16370  rexpen  16376  cnso  16395  dvdslelem  16459  divalglem1  16544  divalglem5  16547  divalglem6  16548  divalglem10  16552  flodddiv4  16565  0bits  16589  sadcf  16603  sadcadd  16608  bitsshft  16625  smupf  16628  gcdf  16664  eucalgf  16738  2prm  16847  dfphi2  16931  pockthi  17065  prmrec  17080  vdwapf  17130  vdwlem6  17144  karatsuba  17241  1259lem5  17293  2503lem3  17297  4001lem4  17302  structcnvcnv  17311  structfn  17314  strleun  17315  imasvscafn  17689  xpsff1o  17719  xrge0base  17759  wunnat  18114  dfinito3  18160  dftermo3  18161  eldmcoa  18220  coapm  18226  catcfuccl  18273  catcxpccl  18361  yonedainv  18435  chnub  18776  smndex1bas  19085  smndex1n0mnd  19091  grpinvfvi  19173  mulgfvi  19263  ressmulgnnd  19268  symgsssg  19661  symgfisg  19662  psgnunilem5  19688  sylow3lem2  19822  oppglsm  19836  efgmf  19907  efgval  19911  efgsf  19923  0frgp  19973  dmdprd  20194  dprdval  20199  invrfval  20599  drngui  20966  rmodislmod  21185  lssintcl  21219  cnfldadd  21664  cnfldmul  21666  cnfldfunALT  21673  cnfld0  21682  cnfld1  21683  cnfldsub  21686  xrsds  21696  pzriprnglem4  21770  pzriprnglem9  21775  pzriprnglem14  21780  psgnghm  21866  zrhpsgnmhm  21870  ocv1  21965  dsmmbas2  22023  mplsubrglem  22291  opsrtoslem2  22345  evl1maprhm  22677  mdetralt  22903  maducoeval2  22935  eltpsi  23242  unitg  23265  fctop  23302  cctop  23304  ppttop  23305  epttop  23307  leordtvallem1  23508  leordtvallem2  23509  iccordt  23512  iscnp2  23537  discmp  23696  conncompcld  23732  1stcrestlem  23750  2ndcdisj  23755  topnlly  23790  disllycmp  23797  dis1stc  23798  txuni2  23864  xkotf  23884  dfac14lem  23916  prdstps  23928  txindis  23933  tx1stc  23949  xkohaus  23952  xkoptsub  23953  cnmpt1st  23967  cnmpt2nd  23968  ptcmpfi  24112  trfil1  24185  fin1aufil  24231  tgpconncompeqg  24411  tgpconncomp  24412  trust  24528  met1stc  24820  dscmet  24871  retopon  25062  cnfldtopon  25081  xrsxmet  25109  xrsmopn  25112  iimulcn  25239  icopnfhmeo  25244  iccpnfhmeo  25246  xrhmeo  25247  cnheiborlem  25255  lebnumii  25267  ishtpy  25273  htpycc  25281  pco1  25316  pcohtpylem  25320  pcopt  25323  pcopt2  25324  pcoass  25325  pcorevlem  25327  rrxcph  25693  rrx0el  25699  ovoliunlem3  25805  ovolicc1  25817  ovolicc2  25823  volf  25830  ioorf  25874  dyadf  25892  dyadmbl  25901  vitalilem5  25913  vitali  25914  mbfimaopnlem  25956  mbflimsup  25967  0plef  25973  i1fima  25979  i1fima2  25980  i1fd  25982  itg1ge0  25987  itg10  25989  i1f1lem  25990  i1fadd  25996  i1fmul  25997  i1fmulc  26004  mbfi1fseqlem5  26020  itg2addlem  26059  reldv  26170  dvbsss  26202  dvef  26280  lhop1lem  26313  deg1fvi  26383  plypf1  26511  coeeulem  26523  coeeu  26524  vieta1lem2  26616  aannenlem3  26639  aalioulem3  26643  dvradcnv  26730  pserulm  26731  pserdvlem2  26737  sinhalfpilem  26774  sincos4thpi  26824  sincos6thpi  26826  pige3ALT  26830  resinf1o  26846  tanord1  26847  tanregt0  26849  efabl  26860  relogrn  26871  dfrelog  26875  logi  26897  logneg  26898  logltb  26910  logcn  26957  logf1o2  26960  dvlog  26961  efopnlem2  26967  efopn  26968  logccv  26973  dvsqrt  27052  dvcnsqrt  27054  cxpcn3  27058  logblog  27102  angpined  27140  1cubr  27152  asinsin  27202  asin1  27204  reasinsin  27206  atan0  27218  atanbnd  27236  atan1  27238  log2cnv  27254  log2ub  27259  log2le1  27260  birthday  27264  amgmlem  27299  emcllem5  27309  emgt0  27316  harmonicbnd3  27317  ftalem3  27384  basellem4  27393  sgmf  27454  ppi1  27473  cht1  27474  vma1  27475  ppiltx  27486  sqff1o  27491  ppiublem1  27511  ppiublem2  27512  ppiub  27513  chtub  27521  dchreq  27567  bposlem7  27599  bposlem8  27600  bposlem9  27601  lgsdir2lem2  27635  lgsdir2lem3  27636  chebbnd1  27781  chto1ub  27785  chpo1ubb  27790  pntibndlem1  27898  nosgnn0  27997  ltssolem1  28014  bdayfo  28016  nolt02o  28034  nogt01o  28035  noetasuplem4  28075  noetainflem4  28079  cutbdaybnd2lim  28165  madeun  28252  cutsfo  28273  addsproplem2  28338  addsproplem7  28343  addsprop  28344  negsprop  28403  subsf  28432  mulsproplem13  28496  mulsproplem14  28497  mulsprop  28498  oniso  28639  n0cut  28702  bdayn0sf1o  28738  twocut  28791  bdaypw2n0bndlem  28831  bdayfinbndlem1  28835  0reno  28864  tgldimor  28947  tglnfn  28992  tgplnfn  29235  axlowdimlem4  29505  axlowdimlem16  29517  axlowdim  29521  upgrfi  29651  lfgrnloop  29685  lfuhgr1v0e  29817  usgrexmplef  29822  usgrres  29871  vdegp1bi  30100  vtxdginducedm1lem2  30103  dfpth2  30296  pthdlem2  30336  wpthswwlks2on  30535  0ewlk  30687  0pth  30698  konigsbergiedgw  30831  konigsberglem1  30835  konigsberglem2  30836  konigsberglem3  30837  konigsberglem4  30838  konigsberglem5  30839  ex-dif  31006  ex-un  31007  ex-in  31008  ex-fl  31030  avril1  31046  9p10ne21fool  31054  n0lplig  31067  cnidOLD  31166  cnnvm  31266  ipasslem8  31421  ipasslem10  31423  hvsubf  31599  normlem1  31694  normlem6  31699  normlem7  31700  norm-ii-i  31721  norm3adifii  31732  hilid  31745  hlimf  31821  hhssabloi  31846  hhssnv  31848  hhshsslem1  31851  shincli  31946  shsval2i  31971  shs0i  32033  chj0i  32039  chm1i  32040  chincli  32044  chdmm1i  32061  shjshsi  32076  chsup0  32132  h1de2bi  32138  spansnpji  32162  cmcmlem  32175  cmcmii  32181  cmcm2ii  32182  cmcm3ii  32183  pjidmi  32257  pjssmii  32265  pj0i  32277  pjocini  32282  mayetes3i  32313  df0op2  32336  hoaddcomi  32356  hoaddassi  32360  hocadddiri  32363  hocsubdiri  32364  hoaddridi  32370  ho0coi  32372  hoid1i  32373  hoid1ri  32374  hodseqi  32378  honegsubi  32380  adj1o  32478  hoddii  32573  lnopunilem1  32594  lnopunilem2  32595  nmcopexi  32611  nmcopex  32613  nmcoplb  32614  nmcfnexi  32635  nmcfnex  32637  nmcfnlb  32638  adjbd1o  32669  adjcoi  32684  nmopcoadji  32685  opsqrlem6  32729  pjsdii  32739  pjddii  32740  pjidmcoi  32761  pjtoi  32763  pjin1i  32776  pjclem1  32779  stji1i  32826  reuxfrdf  33069  iuninc  33137  fnresin  33200  rinvf1o  33206  suppss2f  33214  xppreima  33221  ofoprabco  33240  partfun2  33252  fressupp  33263  supppreima  33266  fsupprnfi  33267  gtiso  33276  df1stres  33279  df2ndres  33280  snct  33287  padct  33292  fsuppcurry1  33298  fsuppcurry2  33299  ffsrn  33302  fpwrelmapffs  33308  fzodif1  33366  nnindf  33393  nn0min  33394  dp2lt  33433  dp2ltsuc  33434  dp2ltc  33435  dplti  33453  dpmul  33461  dpmul4  33462  ressplusf  33506  xrsclat  33554  xrge00  33557  xrnarchi  33727  elrgspnlem2  33786  1fldgenq  33866  xrge0slmod  33891  zringfrac  34068  esplyind  34189  ply1degltdimlem  34236  ccfldsrarelvec  34285  ccfldextdgrr  34286  locfinreflem  34454  locfinref  34455  unicls  34517  sqsscirc1  34522  mhmhmeotmd  34541  raddcn  34543  xrge0iifiso  34549  xrge0iifhmeo  34550  lmxrge0  34566  cnzh  34582  rezh  34583  qqh0  34598  qqh1  34599  qqhre  34634  rrhre  34635  esumnul  34662  esum0  34663  esumsnf  34678  esumpfinvallem  34688  esumpfinvalf  34690  esumpcvgval  34692  esumcvgsum  34702  esumsup  34703  esumcvgre  34705  sigaclfu2  34735  dmsigagen  34759  ddemeas  34851  mbfmvolf  34881  br2base  34884  omssubadd  34915  sibfof  34955  sitg0  34961  eulerpartlemt  34986  eulerpartgbij  34987  0rrv  35066  coinfliplem  35094  coinflipprob  35095  coinfliprv  35098  ballotlem2  35104  ballotlem4  35114  ballotlem5  35115  ballotlemi1  35118  ballotlem7  35151  ballotth  35153  signsplypnf  35162  signsply0  35163  signsw0g  35168  signswch  35173  signsvf0  35192  hashreprin  35232  reprfz1  35236  chtvalz  35241  hgt750lemd  35260  hgt750lem  35263  hgt750lem2  35264  bnj1098  35397  bnj1109  35400  bnj1131  35401  bnj1533  35465  bnj151  35490  bnj580  35526  bnj852  35534  bnj864  35535  bnj865  35536  bnj978  35562  bnj1021  35579  bnj907  35580  bnj1093  35593  bnj1145  35606  bnj1172  35614  bnj1174  35616  bnj1176  35618  bnj1186  35620  nfan1c  35686  xoromon  35697  rankfo  35714  fineqvac  35757  tz9.1regs  35775  axpowg  35787  onvf1odlem4  35858  onvf1od  35859  subfacf  35909  subfacp1lem1  35913  subfacp1lem5  35918  subfacp1lem6  35919  subfacval3  35923  erdszelem2  35926  kur14lem4  35943  ioosconn  35981  iccllysconn  35984  satfn  36089  fmlaomn0  36124  gonan0  36126  goaln0  36127  elnanelprv  36163  msrfo  36280  mthmpps  36316  problem5  36403  quad3  36404  circum  36408  antnestALT  36428  axextprim  36435  axrepprim  36436  axunprim  36437  axinfprim  36440  axacprim  36441  bcneg1  36470  dfon2lem2  36516  dfon2lem4  36518  axextdfeq  36529  fobigcup  36632  snelsingles  36654  fullfunfnv  36680  fullfunfv  36681  rankaltopb  36714  rank0  36901  rankeq1o  36902  in-ax8  36983  fneer  37111  neibastop1  37117  nabi1i  37152  nabi2i  37153  limsucncmpi  37203  tz9.1ctco  37240  ttctr3  37253  ttcpwss  37273  knoppcnlem8  37336  knoppcnlem11  37339  cnndvlem1  37373  bj-consensusALT  37419  bj-sbidmOLD  37732  bj-n0i  37834  bj-snsetex  37846  bj-tagss  37863  bj-2upln0  37906  bj-2upln1upl  37907  bj-nuliota  37940  bj-axseprep  37958  bj-0int  37990  bj-elid5  38058  bj-inftyexpitaufo  38091  bj-pinftyccb  38110  bj-minftyccb  38114  bj-pinftynminfty  38116  bj-isrvec  38183  iccioo01  38218  f1omptsnlem  38227  mptsnunlem  38229  topdifinffinlem  38238  relowlpssretop  38255  1oequni2o  38259  pibt2  38308  imadifss  38491  tan2h  38503  poimirlem3  38509  poimirlem9  38515  poimirlem16  38522  poimirlem17  38523  poimirlem18  38524  poimirlem19  38525  poimirlem20  38526  poimirlem22  38528  poimirlem30  38536  mblfinlem1  38543  mblfinlem2  38544  ovoliunnfl  38548  voliunnfl  38550  itg2addnclem  38557  itg2addnclem2  38558  asindmre  38589  areacirclem1  38594  fdc  38647  cntotbnd  38698  heiborlem6  38718  rrnval  38729  reheibor  38741  rngosn3  38826  brcnvrabga  39242  cnvresrn  39248  moantr  39272  inxp2  39275  dfxrn2  39285  dfsucmap3  39363  dfpre4  39380  cnvcosseq  39427  refrelcosslem  39452  1cosscnvxrn  39465  redundss3  39612  refrelsredund3  39618  refrelredund3  39621  disjimeceqim  39704  eqvrel0  39789  eqvrelid  39792  prter2  39906  renegclALT  39988  mapdunirnN  42675  lcmeprodgcdi  43025  3factsumint2  43040  3factsumint3  43041  3factsumint4  43042  3factsumint  43043  lcmineqlem4  43050  3lexlogpow5ineq1  43072  3lexlogpow2ineq1  43076  dvrelogpow2b  43086  aks4d1p1p4  43089  aks4d1p8  43105  aks6d1c1  43134  aks6d1c2p2  43137  aks6d1c4  43142  2ap1caineq  43163  sticksstones1  43164  sticksstones2  43165  aks6d1c7lem2  43199  aks5lem3a  43207  aks5lem6  43210  unitscyglem2  43214  unitscyglem3  43215  sqdeccom12  43314  readvrec2  43380  readvcot  43383  resubf  43400  sn-0ne2  43425  sn-subf  43448  sn-nnne0  43492  sn-0lt1  43507  reneg1lt0  43512  rntrclfvOAI  43655  diophrw  43723  rabren3dioph  43775  pellexlem6  43794  pellex  43795  frmx  43873  frmy  43874  jm2.23  43956  jm2.27dlem3  43971  axac10  43993  pw2f1ocnv  43997  kelac2lem  44024  lmhmlnmsplit  44047  pwfi2f1o  44056  frlmpwfi  44058  insucid  44363  nla0003  44384  ifpbiidcor  44433  sucomisnotcard  44503  alephiso2  44517  alephiso3  44518  cnvnonrel  44547  rnnonrel  44550  resnonrel  44551  cononrel1  44553  cononrel2  44554  fvnonrel  44556  cnvcnvintabd  44559  cnvintabd  44562  rclexi  44574  rtrclex  44576  clcnvlem  44582  cnvrcl0  44584  dmtrcl  44586  rntrcl  44587  dfrtrcl5  44588  iunrelexp0  44661  dmtrclfvRP  44689  rntrclfv  44691  corcltrcl  44698  cotrclrcl  44701  0heALT  44742  frege54cor1a  44823  uneqsn  44984  clsk3nimkb  44999  int-sqdefd  45140  int-sqgeq0d  45145  rr-groth  45242  rr-grothprim  45243  rr-grothshort  45247  seff  45252  expgrowthi  45276  expgrowth  45278  binomcxplemnotnn0  45299  ee233  45461  ax6e2nd  45500  in1  45513  dfvd2ani  45525  dfvd2i  45527  dfvd3i  45534  dfvd3ani  45537  e0bi  45717  uun2221  45754  uun2221p1  45755  uun2221p2  45756  en3lpVD  45786  relopabVD  45842  ax6e2ndVD  45849  ax6e2ndALT  45871  permaxpow  45951  pssnssi  46059  nnf1oxpnn  46153  icof  46175  fnmptif  46220  rn1st  46228  negpilt0  46240  xrgtso  46301  supxrleubrnmptf  46405  xrpnf  46439  rexanuz2nf  46446  ioontr  46467  iccdifioo  46471  iccdifprioo  46472  uzinico2  46517  fsummulc1f  46527  fsumiunss  46531  fnlimfvre2  46631  limsupreuz  46691  limsup10ex  46727  icccncfext  46841  dvcosre  46866  dvsinax  46867  ioodvbdlimc1lem2  46886  ioodvbdlimc2lem  46888  dvmptmulf  46891  dvnmul  46897  dvmptfprodlem  46898  dvnprodlem2  46901  stoweidlem1  46955  stoweidlem26  46980  stoweidlem34  46988  stoweidlem44  46998  stoweid  47017  stirlinglem5  47032  dirkercncflem1  47057  fourierdlem44  47105  fourierdlem56  47116  fourierdlem62  47122  fourierdlem89  47149  fourierdlem91  47151  fourierdlem100  47160  fourierdlem102  47162  fourierdlem103  47163  fourierdlem104  47164  fourierdlem108  47168  fourierdlem112  47172  fourierdlem114  47174  fouriersw  47185  rrndistlt  47244  gsumge0cl  47325  sge0tsms  47334  sge0ltfirpmpt2  47380  ovn0  47520  hoidmv1le  47548  hoidmvle  47554  ovnsubadd2lem  47599  ovolval4lem1  47603  vonioolem2  47635  smflimlem3  47727  nsssmfmbf  47733  chnerlem1  47836  sqrtnzqaa  47858  numtowerdt  47860  goldrasin  47873  goldrapos  47874  goldratmolem4  47879  goldratval  47880  sqrtnpoly  47887  axorbtnotaiffb  47917  axorbciffatcxorb  47919  abnotbtaxb  47929  euabsneu  48042  ceilhalf1  48352  sprval  48505  fmtnoinf  48565  nprmdvdsfacm1lem2  48650  ppivalnnnprmge6  48655  ppivalnn4  48656  ppivalnn  48661  1nevenALTV  48733  nfermltl8rev  48784  nfermltl2rev  48785  nnsum3primes4  48830  tgblthelfgott  48857  tgoldbachlt  48858  cycl3grtri  48989  isubgr3stgrlem3  49010  usgrexmpl1lem  49063  usgrexmpl2lem  49068  usgrexmpl2trifr  49079  gpgprismgr4cycllem7  49143  ldepslinc  49565  ackval42  49752  rrx2plordso  49780  vsn  49866  dmtposss  49928  sepfsepc  49980  basresposfo  50030  rescofuf  50145  oppff1  50200  idfth  50210  idsubc  50212  fuco2eld2  50366  fuco22a  50402  setc1onsubc  50654  alimp-no-surprise  50821  aacllem  50883  3elfz13  50889  veronesevrowd  50923  veroquadmodzerod  50928  veroquadnolindfd  50929  veroquaddetzerod  50930  amgmwlem  50931  amgmlemALT  50932