Theorem mpbi 231

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

Syntax hints:   ↔ wb 207

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 208

This theorem is referenced by:  pm5.74i  272  notbii  321  biluk  386  pm5.19  387  pm3.24  403  dfbi  476  pm4.71i  564  pm5.32i  579  biadani  825  biadanii  827  imori  860  ori  867  pm5.16  1021  dn1  1063  3ori  1432  cadan  1616  nic-dfim  1676  nic-dfneg  1677  nic-mp  1678  nic-mpALT  1679  tbw-negdf  1706  rb-imdf  1757  nfri  1796  mpgbi  1805  19.35i  1885  nfim1  2211  19.36i  2243  ax6  2392  sbie  2510  datisi  2684  disamis  2685  dimatis  2692  fresison  2693  bamalip  2696  axi12  2710  eqcomi  2749  eqtri  2763  eleqtri  2838  nfnfc  2914  neii  2937  necomi  2989  neeqtri  3007  neli  3041  nrex  3068  rexlimi  3240  eueqi  3657  euxfr2w  3668  euxfr2  3670  reuxfrd  3696  cdeqri  3714  sseqtri  3970  pssn2lp  4042  equncomi  4097  unssi  4127  ssini  4175  unabs  4200  inabs  4201  dfin4  4213  vn0  4280  inindif  4310  difidALT  4312  ab0orv  4318  ab0orvALT  4319  disjdif  4407  difin0  4409  pwundif  4560  snid  4601  rabrsn  4663  iinrab2  5006  symdifv  5022  rintn0  5045  breqtri  5104  axsepgfromrep  5223  bm1.3iiOLD  5231  ax6vsep  5232  notzfaus  5299  zfpow  5302  dtruALT2  5306  dtruALT  5324  reusv2lem4  5337  dtru  5383  elOLD  5385  op1stb  5418  copsexgw  5437  copsexgwOLD  5438  copsexg  5439  uniop  5463  rn0  5875  dmresi  6011  somincom  6091  cnvimassrndm  6110  cnvcnv  6150  elid  6157  rescnvcnv  6162  cnvcnvres  6163  cocnvcnv2  6217  cores2  6218  co01  6220  cnviin  6244  predres  6297  iota4an  6474  fnopab  6630  mpt0  6634  fnmpti  6635  f1cnvcnv  6739  f1ovi  6814  eliman0  6871  fvco4i  6936  cnvimainrn  7015  fmpti  7060  funiunfv  7199  oprabss  7471  relmptopab  7613  zfun  7686  tfinds2  7811  omon  7825  2nd0  7945  f1stres  7962  f2ndres  7963  cnvoprab  8009  relmpoopab  8040  df1st2  8044  df2nd2  8045  fsplit  8063  frpoins3xpg  8087  frpoins3xp3g  8088  poxp2  8090  poseq  8105  reldmtpos  8181  dftpos4  8192  tpostpos  8193  tpos0  8203  frrlem4  8236  smo0  8295  tfrlem14  8327  tfrlem16  8329  rdgsucg  8359  rdglimg  8361  frfnom  8371  oawordeulem  8486  uniixp  8866  dfdom2  8922  ssdomg  8944  xpcomf1o  9001  sbthlem5  9026  sdom0  9044  limensuci  9088  1sdom2  9155  fiint  9234  fidomdm  9241  residfi  9245  mptfi  9258  fisn  9337  dffi3  9341  ordtypelem6  9435  ordtypelem7  9436  wemaplem2  9459  harwdom  9503  nelaneqOLD  9515  suc11reg  9538  zfinf  9558  axinf2  9559  noinfep  9579  cantnfvalf  9584  cantnflt  9591  cantnf0  9594  cantnf  9612  ttrclco  9637  tz9.1c  9649  tc2  9659  setinds  9668  r111  9697  r1tr2  9699  r1ordg  9700  r1sssuc  9705  r1val1  9708  tz9.13  9713  r1elssi  9727  pwwf  9729  rankopb  9774  rankeq0b  9782  ranksuc  9787  rankmapu  9800  rankxplim3  9803  rankxpsuc  9804  cp  9813  karden  9817  card0  9880  cardlim  9894  cardom  9908  infxpenlem  9933  alephsuc2  10000  alephgeom  10002  unialeph  10021  dfac4  10042  dfacacn  10062  dju1dif  10093  dju1p1e2  10094  infdju1  10110  ackbij1lem13  10151  ackbij2  10162  cf0  10171  cfsuc  10177  cfom  10184  cfslb2n  10188  ominf4  10232  fin23lem17  10258  fin23lem28  10260  fin23lem30  10262  fin23lem31  10263  fin23lem40  10271  isfin1-3  10306  dfacfin7  10319  fin1a2lem6  10325  itunitc1  10340  axcc3  10358  dcomex  10367  axdc2lem  10368  axcclem  10377  zfac  10380  ac3  10382  ackm  10385  axac2  10386  axac  10387  axaci  10388  cardeqv  10389  numth2  10391  numth  10392  dmct  10444  brdom3  10448  fin71ac  10453  cardf  10470  aleph1  10492  cfpwsdom  10505  smobeth  10507  zfcndrep  10535  zfcndpow  10537  zfcndac  10540  gch2  10596  wunex3  10662  tskpr  10691  inar1  10696  rankcf  10698  tskcard  10702  tskuni  10704  grothpw  10747  axgroth4  10753  grothprim  10755  inaprc  10757  dmaddpi  10811  dmmulpi  10812  1lt2pi  10826  addpqf  10865  mulpqf  10867  1lt2nq  10894  supsrlem  11032  ssxr  11213  gtso  11225  subf  11393  negne0i  11467  mulnzcnf  11794  infrenegsup  12137  neg1lt0  12145  nnne0  12209  halflt1  12392  nn0ssz  12545  3halfnz  12606  zeo  12613  numlt  12667  numltc  12668  le9lt10  12669  decle  12676  uzf  12789  xaddf  13174  xsubge0  13211  xmulf  13222  ixxf  13306  ixxssxr  13308  iooval2  13329  ioof  13398  unirnioo  13400  dfioo2  13401  fzval2  13462  fzf  13463  0nelfz1  13495  fz10  13497  fzpreddisj  13525  4fvwrd4  13600  fzof  13608  fzo0  13636  fldiv4p1lem1div2  13792  fldiv4lem1div2  13794  om2uzoi  13915  faclbnd4lem1  14253  hashkf  14292  hashgval  14293  hashinf  14295  hashresfn  14300  hashnn0n0nn  14351  hashge3el3dif  14447  hash3tpde  14453  rev0  14724  s2dm  14850  f1oun2prg  14877  trclublem  14955  sqrt2gt1lt2  15234  limsupgord  15432  fclim  15513  fsumrelem  15768  ackbijnn  15791  incexclem  15799  incexc  15800  arisum2  15824  georeclim  15835  geoisumr  15841  0.999...  15844  risefall0lem  15989  ege2le3  16053  sin0  16114  ef01bndlem  16149  cos2bnd  16153  cos01gt0  16156  sincos2sgn  16159  sin4lt0  16160  rpnnen2lem3  16181  rpnnen2lem9  16187  rexpen  16193  cnso  16212  dvdslelem  16276  divalglem1  16361  divalglem5  16364  divalglem6  16365  divalglem10  16369  flodddiv4  16382  0bits  16406  sadcf  16420  sadcadd  16425  bitsshft  16442  smupf  16445  gcdf  16479  eucalgf  16550  2prm  16659  dfphi2  16742  pockthi  16876  prmrec  16891  vdwapf  16941  vdwlem6  16955  karatsuba  17052  1259lem5  17103  2503lem3  17107  4001lem4  17112  structcnvcnv  17121  structfn  17124  strleun  17125  imasvscafn  17499  xpsff1o  17529  xrge0base  17569  wunnat  17924  dfinito3  17970  dftermo3  17971  eldmcoa  18030  coapm  18036  catcfuccl  18083  catcxpccl  18171  yonedainv  18245  chnub  18586  smndex1bas  18875  smndex1n0mnd  18881  grpinvfvi  18956  mulgfvi  19047  ressmulgnnd  19052  symgsssg  19440  symgfisg  19441  psgnunilem5  19467  sylow3lem2  19601  oppglsm  19615  efgmf  19686  efgval  19690  efgsf  19702  0frgp  19752  dmdprd  19973  dprdval  19978  invrfval  20367  drngui  20714  rmodislmod  20927  lssintcl  20961  cnfldadd  21360  cnfldmul  21362  cnfldfunALT  21369  cnfld0  21378  cnfld1  21379  cnfldsub  21382  xrsds  21392  pzriprnglem4  21466  pzriprnglem9  21471  pzriprnglem14  21476  psgnghm  21562  zrhpsgnmhm  21566  ocv1  21661  dsmmbas2  21719  mplsubrglem  21985  opsrtoslem2  22039  evl1maprhm  22372  mdetralt  22598  maducoeval2  22630  eltpsi  22934  unitg  22957  fctop  22994  cctop  22996  ppttop  22997  epttop  22999  leordtvallem1  23200  leordtvallem2  23201  iccordt  23204  iscnp2  23229  discmp  23388  conncompcld  23424  1stcrestlem  23442  2ndcdisj  23446  topnlly  23481  disllycmp  23488  dis1stc  23489  txuni2  23555  xkotf  23575  dfac14lem  23607  prdstps  23619  txindis  23624  tx1stc  23640  xkohaus  23643  xkoptsub  23644  cnmpt1st  23658  cnmpt2nd  23659  ptcmpfi  23803  trfil1  23876  fin1aufil  23922  tgpconncompeqg  24102  tgpconncomp  24103  trust  24219  met1stc  24511  dscmet  24562  retopon  24753  cnfldtopon  24772  xrsxmet  24800  xrsmopn  24803  iimulcn  24930  icopnfhmeo  24935  iccpnfhmeo  24937  xrhmeo  24938  cnheiborlem  24946  lebnumii  24958  ishtpy  24964  htpycc  24972  pco1  25007  pcohtpylem  25011  pcopt  25014  pcopt2  25015  pcoass  25016  pcorevlem  25018  rrxcph  25384  rrx0el  25390  ovoliunlem3  25496  ovolicc1  25508  ovolicc2  25514  volf  25521  ioorf  25565  dyadf  25583  dyadmbl  25592  vitalilem5  25604  vitali  25605  mbfimaopnlem  25647  mbflimsup  25658  0plef  25664  i1fima  25670  i1fima2  25671  i1fd  25673  itg1ge0  25678  itg10  25680  i1f1lem  25681  i1fadd  25687  i1fmul  25688  i1fmulc  25695  mbfi1fseqlem5  25711  itg2addlem  25750  reldv  25862  dvbsss  25894  dvef  25972  lhop1lem  26005  deg1fvi  26075  plypf1  26202  coeeulem  26214  coeeu  26215  vieta1lem2  26302  aannenlem3  26321  aalioulem3  26325  dvradcnv  26411  pserulm  26412  pserdvlem2  26418  sinhalfpilem  26452  sincos4thpi  26502  tan4thpiOLD  26504  sincos6thpi  26505  pige3ALT  26509  resinf1o  26525  tanord1  26526  tanregt0  26528  efabl  26539  relogrn  26550  dfrelog  26554  logi  26576  logneg  26577  logltb  26589  logcn  26636  logf1o2  26639  dvlog  26640  efopnlem2  26646  efopn  26647  logccv  26652  dvsqrt  26731  dvcnsqrt  26733  cxpcn3  26737  logblog  26781  angpined  26819  1cubr  26831  asinsin  26881  asin1  26883  reasinsin  26885  atan0  26897  atanbnd  26915  atan1  26917  log2cnv  26933  log2ub  26938  log2le1  26939  birthday  26943  amgmlem  26978  emcllem5  26988  emgt0  26995  harmonicbnd3  26996  ftalem3  27063  basellem4  27072  sgmf  27133  ppi1  27152  cht1  27153  vma1  27154  ppiltx  27165  sqff1o  27170  ppiublem1  27190  ppiublem2  27191  ppiub  27192  chtub  27200  dchreq  27246  bposlem7  27278  bposlem8  27279  bposlem9  27280  lgsdir2lem2  27314  lgsdir2lem3  27315  chebbnd1  27460  chto1ub  27464  chpo1ubb  27469  pntibndlem1  27577  nosgnn0  27647  ltssolem1  27664  bdayfo  27666  nolt02o  27684  nogt01o  27685  noetasuplem4  27725  noetainflem4  27729  cutbdaybnd2lim  27814  madeun  27901  cutsfo  27922  addsproplem2  27987  addsproplem7  27992  addsprop  27993  negsprop  28052  subsf  28081  mulsproplem13  28145  mulsproplem14  28146  mulsprop  28147  oniso  28288  n0cut  28351  bdayn0sf1o  28387  twocut  28440  bdaypw2n0bndlem  28480  bdayfinbndlem1  28484  0reno  28513  tgldimor  28595  tglnfn  28640  axlowdimlem4  29039  axlowdimlem16  29051  axlowdim  29055  upgrfi  29185  lfgrnloop  29219  lfuhgr1v0e  29348  usgrexmplef  29353  usgrres  29402  vdegp1bi  29631  vtxdginducedm1lem2  29634  dfpth2  29822  pthdlem2  29861  wpthswwlks2on  30057  0ewlk  30209  0pth  30220  konigsbergiedgw  30343  konigsberglem1  30347  konigsberglem2  30348  konigsberglem3  30349  konigsberglem4  30350  konigsberglem5  30351  ex-dif  30518  ex-un  30519  ex-in  30520  ex-fl  30542  avril1  30558  9p10ne21fool  30566  n0lplig  30579  cnidOLD  30678  cnnvm  30778  ipasslem8  30933  ipasslem10  30935  hvsubf  31111  normlem1  31206  normlem6  31211  normlem7  31212  norm-ii-i  31233  norm3adifii  31244  hilid  31257  hlimf  31333  hhssabloi  31358  hhssnv  31360  hhshsslem1  31363  shincli  31458  shsval2i  31483  shs0i  31545  chj0i  31551  chm1i  31552  chincli  31556  chdmm1i  31573  shjshsi  31588  chsup0  31644  h1de2bi  31650  spansnpji  31674  cmcmlem  31687  cmcmii  31693  cmcm2ii  31694  cmcm3ii  31695  pjidmi  31769  pjssmii  31777  pj0i  31789  pjocini  31794  mayetes3i  31825  df0op2  31848  hoaddcomi  31868  hoaddassi  31872  hocadddiri  31875  hocsubdiri  31876  hoaddridi  31882  ho0coi  31884  hoid1i  31885  hoid1ri  31886  hodseqi  31890  honegsubi  31892  adj1o  31990  hoddii  32085  lnopunilem1  32106  lnopunilem2  32107  nmcopexi  32123  nmcopex  32125  nmcoplb  32126  nmcfnexi  32147  nmcfnex  32149  nmcfnlb  32150  adjbd1o  32181  adjcoi  32196  nmopcoadji  32197  opsqrlem6  32241  pjsdii  32251  pjddii  32252  pjidmcoi  32273  pjtoi  32275  pjin1i  32288  pjclem1  32291  stji1i  32338  reuxfrdf  32585  iuninc  32656  fnresin  32723  rinvf1o  32729  suppss2f  32737  xppreima  32744  ofoprabco  32763  partfun2  32775  fressupp  32787  supppreima  32790  fsupprnfi  32791  gtiso  32800  df1stres  32803  df2ndres  32804  snct  32811  padct  32817  fsuppcurry1  32823  fsuppcurry2  32824  ffsrn  32827  fpwrelmapffs  32833  fzodif1  32891  nnindf  32919  nn0min  32920  dp2lt  32970  dp2ltsuc  32971  dp2ltc  32972  dplti  32990  dpmul  32998  dpmul4  32999  ressplusf  33049  xrsclat  33097  xrge00  33100  xrnarchi  33272  elrgspnlem2  33331  1fldgenq  33413  xrge0slmod  33438  zringfrac  33644  esplyind  33766  ply1degltdimlem  33813  ccfldsrarelvec  33862  ccfldextdgrr  33863  locfinreflem  34031  locfinref  34032  unicls  34094  sqsscirc1  34099  mhmhmeotmd  34118  raddcn  34120  xrge0iifiso  34126  xrge0iifhmeo  34127  lmxrge0  34143  cnzh  34159  rezh  34160  qqh0  34175  qqh1  34176  qqhre  34211  rrhre  34212  esumnul  34239  esum0  34240  esumsnf  34255  esumpfinvallem  34265  esumpfinvalf  34267  esumpcvgval  34269  esumcvgsum  34279  esumsup  34280  esumcvgre  34282  sigaclfu2  34312  dmsigagen  34335  ddemeas  34427  mbfmvolf  34457  br2base  34460  omssubadd  34491  sibfof  34531  sitg0  34537  eulerpartlemt  34562  eulerpartgbij  34563  0rrv  34642  coinfliplem  34670  coinflipprob  34671  coinfliprv  34674  ballotlem2  34680  ballotlem4  34690  ballotlem5  34691  ballotlemi1  34694  ballotlem7  34727  ballotth  34729  signsplypnf  34741  signsply0  34742  signsw0g  34747  signswch  34752  signsvf0  34771  hashreprin  34811  reprfz1  34815  chtvalz  34820  hgt750lemd  34839  hgt750lem  34842  hgt750lem2  34843  bnj1098  34973  bnj1109  34976  bnj1131  34977  bnj1533  35041  bnj151  35066  bnj580  35102  bnj852  35110  bnj864  35111  bnj865  35112  bnj978  35138  bnj1021  35155  bnj907  35156  bnj1093  35169  bnj1145  35182  bnj1172  35190  bnj1174  35192  bnj1176  35194  bnj1186  35196  nfan1c  35262  xoromon  35277  fineqvac  35304  tz9.1regs  35322  axpowg  35334  onvf1odlem4  35341  onvf1od  35342  subfacf  35410  subfacp1lem1  35414  subfacp1lem5  35419  subfacp1lem6  35420  subfacval3  35424  erdszelem2  35427  kur14lem4  35444  ioosconn  35482  iccllysconn  35485  satfn  35590  fmlaomn0  35625  gonan0  35627  goaln0  35628  elnanelprv  35664  msrfo  35781  mthmpps  35817  problem5  35904  quad3  35905  circum  35909  antnestALT  35929  axextprim  35936  axrepprim  35937  axunprim  35938  axinfprim  35941  axacprim  35942  bcneg1  35971  dfon2lem2  36017  dfon2lem4  36019  axextdfeq  36030  fobigcup  36133  snelsingles  36155  fullfunfnv  36181  fullfunfv  36182  rankaltopb  36214  rank0  36405  rankeq1o  36406  hfuni  36419  in-ax8  36459  fneer  36588  neibastop1  36594  nabi1i  36629  nabi2i  36630  limsucncmpi  36680  tz9.1ctco  36717  ttctr3  36730  ttcpwss  36750  knoppcnlem8  36813  knoppcnlem11  36816  cnndvlem1  36850  bj-consensusALT  36897  bj-sbidmOLD  37210  bj-n0i  37311  bj-snsetex  37323  bj-tagss  37340  bj-2upln0  37383  bj-2upln1upl  37384  bj-nuliota  37417  bj-axseprep  37434  bj-0int  37466  bj-elid5  37536  bj-inftyexpitaufo  37569  bj-pinftyccb  37588  bj-minftyccb  37592  bj-pinftynminfty  37594  bj-isrvec  37661  iccioo01  37696  f1omptsnlem  37705  mptsnunlem  37707  topdifinffinlem  37716  relowlpssretop  37733  1oequni2o  37737  pibt2  37786  imadifss  37969  tan2h  37986  poimirlem3  37997  poimirlem9  38003  poimirlem16  38010  poimirlem17  38011  poimirlem18  38012  poimirlem19  38013  poimirlem20  38014  poimirlem22  38016  poimirlem30  38024  mblfinlem1  38031  mblfinlem2  38032  ovoliunnfl  38036  voliunnfl  38038  itg2addnclem  38045  itg2addnclem2  38046  asindmre  38077  areacirclem1  38082  fdc  38119  cntotbnd  38170  heiborlem6  38190  rrnval  38201  reheibor  38213  rngosn3  38298  brcnvrabga  38716  cnvresrn  38722  moantr  38746  inxp2  38749  dfxrn2  38759  dfsucmap3  38837  dfpre4  38854  cnvcosseq  38901  refrelcosslem  38926  1cosscnvxrn  38939  redundss3  39086  refrelsredund3  39092  refrelredund3  39095  disjimeceqim  39178  eqvrel0  39263  eqvrelid  39266  prter2  39380  renegclALT  39462  mapdunirnN  42149  lcmeprodgcdi  42499  3factsumint2  42514  3factsumint3  42515  3factsumint4  42516  3factsumint  42517  lcmineqlem4  42524  3lexlogpow5ineq1  42546  3lexlogpow2ineq1  42550  dvrelogpow2b  42560  aks4d1p1p4  42563  aks4d1p8  42579  aks6d1c1  42608  aks6d1c2p2  42611  aks6d1c4  42616  2ap1caineq  42637  sticksstones1  42638  sticksstones2  42639  aks6d1c7lem2  42673  aks5lem3a  42681  aks5lem6  42684  unitscyglem2  42688  unitscyglem3  42689  sqdeccom12  42773  readvrec2  42845  readvcot  42848  resubf  42865  sn-0ne2  42890  sn-subf  42913  sn-nnne0  42957  sn-0lt1  42972  reneg1lt0  42977  rntrclfvOAI  43147  diophrw  43215  rabren3dioph  43267  pellexlem6  43286  pellex  43287  frmx  43365  frmy  43366  jm2.23  43448  jm2.27dlem3  43463  axac10  43485  pw2f1ocnv  43489  kelac2lem  43516  lmhmlnmsplit  43539  pwfi2f1o  43548  frlmpwfi  43550  insucid  43855  nla0003  43876  ifpbiidcor  43925  sucomisnotcard  43995  alephiso2  44009  alephiso3  44010  cnvnonrel  44039  rnnonrel  44042  resnonrel  44043  cononrel1  44045  cononrel2  44046  fvnonrel  44048  cnvcnvintabd  44051  cnvintabd  44054  rclexi  44066  rtrclex  44068  clcnvlem  44074  cnvrcl0  44076  dmtrcl  44078  rntrcl  44079  dfrtrcl5  44080  iunrelexp0  44153  dmtrclfvRP  44181  rntrclfv  44183  corcltrcl  44190  cotrclrcl  44193  0heALT  44234  frege54cor1a  44315  uneqsn  44476  clsk3nimkb  44491  int-sqdefd  44632  int-sqgeq0d  44637  rr-groth  44750  rr-grothprim  44751  rr-grothshort  44755  seff  44760  expgrowthi  44784  expgrowth  44786  binomcxplemnotnn0  44807  ee233  44970  ax6e2nd  45009  in1  45022  dfvd2ani  45034  dfvd2i  45036  dfvd3i  45043  dfvd3ani  45046  e0bi  45226  uun2221  45263  uun2221p1  45264  uun2221p2  45265  en3lpVD  45295  relopabVD  45351  ax6e2ndVD  45358  ax6e2ndALT  45380  permaxpow  45460  pssnssi  45555  nnf1oxpnn  45649  icof  45671  fnmptif  45716  rn1st  45724  negpilt0  45736  xrgtso  45797  supxrleubrnmptf  45901  xrpnf  45935  rexanuz2nf  45942  ioontr  45963  iccdifioo  45967  iccdifprioo  45968  uzinico2  46013  fsummulc1f  46023  fsumiunss  46027  fnlimfvre2  46127  limsupreuz  46187  limsup10ex  46223  icccncfext  46337  dvcosre  46362  dvsinax  46363  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  dvmptmulf  46387  dvnmul  46393  dvmptfprodlem  46394  dvnprodlem2  46397  stoweidlem1  46451  stoweidlem26  46476  stoweidlem34  46484  stoweidlem44  46494  stoweid  46513  stirlinglem5  46528  dirkercncflem1  46553  fourierdlem44  46601  fourierdlem56  46612  fourierdlem62  46618  fourierdlem89  46645  fourierdlem91  46647  fourierdlem100  46656  fourierdlem102  46658  fourierdlem103  46659  fourierdlem104  46660  fourierdlem108  46664  fourierdlem112  46668  fourierdlem114  46670  fouriersw  46681  rrndistlt  46740  gsumge0cl  46821  sge0tsms  46830  sge0ltfirpmpt2  46876  ovn0  47016  hoidmv1le  47044  hoidmvle  47050  ovnsubadd2lem  47095  ovolval4lem1  47099  vonioolem2  47131  smflimlem3  47223  nsssmfmbf  47229  chnerlem1  47334  nthrucw  47338  goldrasin  47352  goldrapos  47353  sinnpoly  47361  axorbtnotaiffb  47373  axorbciffatcxorb  47375  abnotbtaxb  47385  euabsneu  47498  ceilhalf1  47808  sprval  47961  fmtnoinf  48021  nprmdvdsfacm1lem2  48106  ppivalnnnprmge6  48111  ppivalnn4  48112  ppivalnn  48117  1nevenALTV  48189  nfermltl8rev  48240  nfermltl2rev  48241  nnsum3primes4  48286  tgblthelfgott  48313  tgoldbachlt  48314  cycl3grtri  48445  isubgr3stgrlem3  48466  usgrexmpl1lem  48519  usgrexmpl2lem  48524  usgrexmpl2trifr  48535  gpgprismgr4cycllem7  48599  ldepslinc  49007  ackval42  49194  rrx2plordso  49222  vsn  49309  dmtposss  49373  sepfsepc  49425  basresposfo  49475  rescofuf  49590  oppff1  49645  idfth  49655  idsubc  49657  fuco2eld2  49811  fuco22a  49847  setc1onsubc  50099  alimp-no-surprise  50278  aacllem  50298  amgmwlem  50299  amgmlemALT  50300