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 ⊢ 𝜓

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  pm5.74i  274  notbii  323  biluk  389  pm5.19  390  pm3.24  407  dfbi  480  pm4.71i  568  pm5.32i  584  biadani  831  biadanii  833  imori  867  ori  874  pm5.16  1031  dn1  1073  3ori  1451  cadan  1639  nic-dfim  1699  nic-dfneg  1700  nic-mp  1701  nic-mpALT  1702  tbw-negdf  1729  rb-imdf  1780  nfri  1819  mpgbi  1828  19.35i  1908  nfim1  2235  19.36i  2267  ax6  2416  sbie  2534  datisi  2707  disamis  2708  dimatis  2715  fresison  2716  bamalip  2719  axi12  2733  eqcomi  2772  eqtri  2786  eleqtri  2861  nfnfc  2937  neii  2960  necomi  3012  neeqtri  3030  neli  3066  nrex  3093  rexlimi  3265  eueqi  3673  euxfr2w  3684  euxfr2  3686  reuxfrd  3712  cdeqri  3730  sseqtri  3986  pssn2lp  4060  equncomi  4115  unssi  4145  ssini  4193  unabs  4219  inabs  4220  dfin4  4232  vn0OLD  4300  inindif  4332  difidALT  4334  ab0orv  4340  ab0orvALT  4341  difin0  4436  pwundif  4588  snid  4629  rabrsn  4691  iinrab2  5035  symdifv  5053  rintn0  5076  breqtri  5137  axsepgfromrep  5256  bm1.3iiOLD  5266  ax6vsep  5267  notsep  5336  zfpow  5339  dtruALT2  5343  dtruALT  5361  reusv2lem4  5374  dtru  5420  elOLD  5422  op1stb  5455  copsexgw  5474  copsexgwOLD  5475  copsexg  5476  uniop  5500  rn0  5918  dmresi  6056  somincom  6136  cnvimassrndm  6151  cnvcnv  6192  elid  6200  rescnvcnv  6207  cnvcnvres  6208  cocnvcnv2  6262  cores2  6263  co01  6265  cnviin  6289  predres  6342  iota4an  6520  fnopab  6675  mpt0  6679  fnmpti  6680  f1cnvcnv  6787  f1ovi  6863  eliman0  6920  fvco4i  6985  cnvimainrn  7064  fmpti  7109  funiunfv  7248  oprabss  7520  relmptopab  7662  zfun  7735  tfinds2  7861  omon  7875  2nd0  7994  f1stres  8011  f2ndres  8012  cnvoprab  8058  relmpoopab  8090  df1st2  8094  df2nd2  8095  fsplit  8113  frpoins3xpg  8137  frpoins3xp3g  8138  poxp2  8140  poseq  8155  reldmtpos  8231  dftpos4  8242  tpostpos  8243  tpos0  8253  frrlem4  8287  smo0  8346  tfrlem14  8379  tfrlem16  8381  rdgsucg  8411  rdglimg  8413  frfnom  8423  oawordeulem  8540  uniixp  8920  dfdom2  8976  ssdomg  8998  xpcomf1o  9055  sbthlem5  9080  sdom0  9098  limensuci  9142  1sdom2  9209  fiint  9287  fidomdm  9292  residfi  9296  mptfi  9309  fisn  9388  dffi3  9392  ordtypelem6  9486  ordtypelem7  9487  wemaplem2  9510  harwdom  9554  nelaneqOLD  9566  suc11reg  9589  zfinf  9609  axinf2  9610  noinfep  9630  cantnfvalf  9635  cantnflt  9642  cantnf0  9645  cantnf  9663  ttrclco  9688  tz9.1c  9700  tc2  9710  setinds  9719  r111  9748  r1tr2  9750  r1ordg  9751  r1sssuc  9756  r1val1  9759  tz9.13  9764  r1elssi  9778  pwwf  9780  rankopb  9825  rankeq0b  9833  ranksuc  9838  rankmapu  9851  rankxplim3  9854  rankxpsuc  9855  cp  9878  karden  9882  card0  9945  cardlim  9959  cardom  9973  infxpenlem  9998  alephsuc2  10065  alephgeom  10067  unialeph  10086  dfac4  10107  dfacacn  10126  dju1dif  10157  dju1p1e2  10158  infdju1  10174  ackbij1lem13  10215  ackbij2  10226  cf0  10235  cfsuc  10242  cfom  10249  cfslb2n  10253  ominf4  10297  fin23lem17  10323  fin23lem28  10325  fin23lem30  10327  fin23lem31  10328  fin23lem40  10336  isfin1-3  10371  dfacfin7  10384  fin1a2lem6  10390  itunitc1  10405  axcc3  10423  dcomex  10432  axdc2lem  10433  axcclem  10442  zfac  10445  ac3  10447  ackm  10450  axac2  10451  axac  10452  axaci  10453  cardeqv  10454  numth2  10456  numth  10457  dmct  10509  brdom3  10513  fin71ac  10518  cardf  10535  aleph1  10557  cfpwsdom  10570  smobeth  10572  zfcndrep  10600  zfcndpow  10602  zfcndac  10605  gch2  10661  wunex3  10727  tskpr  10756  inar1  10761  rankcf  10763  tskcard  10767  tskuni  10769  grothpw  10812  axgroth4  10818  grothprim  10820  inaprc  10822  dmaddpi  10876  dmmulpi  10877  1lt2pi  10891  addpqf  10930  mulpqf  10932  1lt2nq  10959  supsrlem  11097  ssxr  11280  gtso  11292  subf  11460  negne0i  11534  mulnzcnf  11861  infrenegsup  12199  neg1lt0  12207  nnne0  12271  halflt1  12462  nn0ssz  12615  3halfnz  12676  zeo  12683  numlt  12742  numltc  12743  le9lt10  12744  decle  12751  uzf  12866  xaddf  13251  xsubge0  13288  xmulf  13299  ixxf  13383  ixxssxr  13385  iooval2  13406  ioof  13475  unirnioo  13477  dfioo2  13478  fzval2  13539  fzf  13540  0nelfz1  13572  fz10  13574  fz00m1  13575  fzpreddisj  13603  4fvwrd4  13678  fzof  13686  fzo0  13714  fldiv4p1lem1div2  13870  fldiv4lem1div2  13872  om2uzoi  13993  faclbnd4lem1  14331  hashkf  14370  hashgval  14371  hashinf  14373  hashresfn  14378  hashnn0n0nn  14429  hashge3el3dif  14526  hash3tpde  14532  rev0  14803  s2dm  14929  f1oun2prg  14956  trclublem  15034  sqrt2gt1lt2  15327  limsupgord  15525  fclim  15606  fsumrelem  15861  ackbijnn  15884  incexclem  15892  incexc  15893  arisum2  15917  georeclim  15928  geoisumr  15934  0.999...  15937  ege2le3  16145  sin0  16206  ef01bndlem  16241  cos2bnd  16245  cos01gt0  16248  sincos2sgn  16251  sin4lt0  16252  rpnnen2lem3  16273  rpnnen2lem9  16279  rexpen  16285  cnso  16304  dvdslelem  16368  divalglem1  16453  divalglem5  16456  divalglem6  16457  divalglem10  16461  flodddiv4  16474  0bits  16498  sadcf  16512  sadcadd  16517  bitsshft  16534  smupf  16537  gcdf  16571  eucalgf  16642  2prm  16751  dfphi2  16834  pockthi  16968  prmrec  16983  vdwapf  17033  vdwlem6  17047  karatsuba  17144  1259lem5  17196  2503lem3  17200  4001lem4  17205  structcnvcnv  17214  structfn  17217  strleun  17218  imasvscafn  17592  xpsff1o  17622  xrge0base  17662  wunnat  18017  dfinito3  18063  dftermo3  18064  eldmcoa  18123  coapm  18129  catcfuccl  18176  catcxpccl  18264  yonedainv  18338  chnub  18679  smndex1bas  18969  smndex1n0mnd  18975  grpinvfvi  19050  mulgfvi  19140  ressmulgnnd  19145  symgsssg  19538  symgfisg  19539  psgnunilem5  19565  sylow3lem2  19699  oppglsm  19713  efgmf  19784  efgval  19788  efgsf  19800  0frgp  19850  dmdprd  20071  dprdval  20076  invrfval  20472  drngui  20820  rmodislmod  21032  lssintcl  21066  cnfldadd  21509  cnfldmul  21511  cnfldfunALT  21518  cnfld0  21527  cnfld1  21528  cnfldsub  21531  xrsds  21541  pzriprnglem4  21615  pzriprnglem9  21620  pzriprnglem14  21625  psgnghm  21711  zrhpsgnmhm  21715  ocv1  21810  dsmmbas2  21868  mplsubrglem  22134  opsrtoslem2  22188  evl1maprhm  22520  mdetralt  22746  maducoeval2  22778  eltpsi  23082  unitg  23105  fctop  23142  cctop  23144  ppttop  23145  epttop  23147  leordtvallem1  23348  leordtvallem2  23349  iccordt  23352  iscnp2  23377  discmp  23536  conncompcld  23572  1stcrestlem  23590  2ndcdisj  23594  topnlly  23629  disllycmp  23636  dis1stc  23637  txuni2  23703  xkotf  23723  dfac14lem  23755  prdstps  23767  txindis  23772  tx1stc  23788  xkohaus  23791  xkoptsub  23792  cnmpt1st  23806  cnmpt2nd  23807  ptcmpfi  23951  trfil1  24024  fin1aufil  24070  tgpconncompeqg  24250  tgpconncomp  24251  trust  24367  met1stc  24659  dscmet  24710  retopon  24901  cnfldtopon  24920  xrsxmet  24948  xrsmopn  24951  iimulcn  25078  icopnfhmeo  25083  iccpnfhmeo  25085  xrhmeo  25086  cnheiborlem  25094  lebnumii  25106  ishtpy  25112  htpycc  25120  pco1  25155  pcohtpylem  25159  pcopt  25162  pcopt2  25163  pcoass  25164  pcorevlem  25166  rrxcph  25532  rrx0el  25538  ovoliunlem3  25644  ovolicc1  25656  ovolicc2  25662  volf  25669  ioorf  25713  dyadf  25731  dyadmbl  25740  vitalilem5  25752  vitali  25753  mbfimaopnlem  25795  mbflimsup  25806  0plef  25812  i1fima  25818  i1fima2  25819  i1fd  25821  itg1ge0  25826  itg10  25828  i1f1lem  25829  i1fadd  25835  i1fmul  25836  i1fmulc  25843  mbfi1fseqlem5  25859  itg2addlem  25898  reldv  26010  dvbsss  26042  dvef  26120  lhop1lem  26153  deg1fvi  26223  plypf1  26350  coeeulem  26362  coeeu  26363  vieta1lem2  26453  aannenlem3  26472  aalioulem3  26476  dvradcnv  26562  pserulm  26563  pserdvlem2  26569  sinhalfpilem  26606  sincos4thpi  26656  tan4thpiOLD  26658  sincos6thpi  26659  pige3ALT  26663  resinf1o  26679  tanord1  26680  tanregt0  26682  efabl  26693  relogrn  26704  dfrelog  26708  logi  26730  logneg  26731  logltb  26743  logcn  26790  logf1o2  26793  dvlog  26794  efopnlem2  26800  efopn  26801  logccv  26806  dvsqrt  26885  dvcnsqrt  26887  cxpcn3  26891  logblog  26935  angpined  26973  1cubr  26985  asinsin  27035  asin1  27037  reasinsin  27039  atan0  27051  atanbnd  27069  atan1  27071  log2cnv  27087  log2ub  27092  log2le1  27093  birthday  27097  amgmlem  27132  emcllem5  27142  emgt0  27149  harmonicbnd3  27150  ftalem3  27217  basellem4  27226  sgmf  27287  ppi1  27306  cht1  27307  vma1  27308  ppiltx  27319  sqff1o  27324  ppiublem1  27344  ppiublem2  27345  ppiub  27346  chtub  27354  dchreq  27400  bposlem7  27432  bposlem8  27433  bposlem9  27434  lgsdir2lem2  27468  lgsdir2lem3  27469  chebbnd1  27614  chto1ub  27618  chpo1ubb  27623  pntibndlem1  27731  nosgnn0  27800  ltssolem1  27817  bdayfo  27819  nolt02o  27837  nogt01o  27838  noetasuplem4  27878  noetainflem4  27882  cutbdaybnd2lim  27968  madeun  28055  cutsfo  28076  addsproplem2  28141  addsproplem7  28146  addsprop  28147  negsprop  28206  subsf  28235  mulsproplem13  28299  mulsproplem14  28300  mulsprop  28301  oniso  28442  n0cut  28505  bdayn0sf1o  28541  twocut  28594  bdaypw2n0bndlem  28634  bdayfinbndlem1  28638  0reno  28667  tgldimor  28749  tglnfn  28794  tgplnfn  29035  axlowdimlem4  29273  axlowdimlem16  29285  axlowdim  29289  upgrfi  29419  lfgrnloop  29453  lfuhgr1v0e  29582  usgrexmplef  29587  usgrres  29636  vdegp1bi  29865  vtxdginducedm1lem2  29868  dfpth2  30056  pthdlem2  30095  wpthswwlks2on  30291  0ewlk  30443  0pth  30454  konigsbergiedgw  30577  konigsberglem1  30581  konigsberglem2  30582  konigsberglem3  30583  konigsberglem4  30584  konigsberglem5  30585  ex-dif  30752  ex-un  30753  ex-in  30754  ex-fl  30776  avril1  30792  9p10ne21fool  30800  n0lplig  30813  cnidOLD  30912  cnnvm  31012  ipasslem8  31167  ipasslem10  31169  hvsubf  31345  normlem1  31440  normlem6  31445  normlem7  31446  norm-ii-i  31467  norm3adifii  31478  hilid  31491  hlimf  31567  hhssabloi  31592  hhssnv  31594  hhshsslem1  31597  shincli  31692  shsval2i  31717  shs0i  31779  chj0i  31785  chm1i  31786  chincli  31790  chdmm1i  31807  shjshsi  31822  chsup0  31878  h1de2bi  31884  spansnpji  31908  cmcmlem  31921  cmcmii  31927  cmcm2ii  31928  cmcm3ii  31929  pjidmi  32003  pjssmii  32011  pj0i  32023  pjocini  32028  mayetes3i  32059  df0op2  32082  hoaddcomi  32102  hoaddassi  32106  hocadddiri  32109  hocsubdiri  32110  hoaddridi  32116  ho0coi  32118  hoid1i  32119  hoid1ri  32120  hodseqi  32124  honegsubi  32126  adj1o  32224  hoddii  32319  lnopunilem1  32340  lnopunilem2  32341  nmcopexi  32357  nmcopex  32359  nmcoplb  32360  nmcfnexi  32381  nmcfnex  32383  nmcfnlb  32384  adjbd1o  32415  adjcoi  32430  nmopcoadji  32431  opsqrlem6  32475  pjsdii  32485  pjddii  32486  pjidmcoi  32507  pjtoi  32509  pjin1i  32522  pjclem1  32525  stji1i  32572  reuxfrdf  32815  iuninc  32883  fnresin  32947  rinvf1o  32953  suppss2f  32961  xppreima  32968  ofoprabco  32987  partfun2  32999  fressupp  33011  supppreima  33014  fsupprnfi  33015  gtiso  33024  df1stres  33027  df2ndres  33028  snct  33035  padct  33041  fsuppcurry1  33047  fsuppcurry2  33048  ffsrn  33051  fpwrelmapffs  33057  fzodif1  33115  nnindf  33142  nn0min  33143  dp2lt  33182  dp2ltsuc  33183  dp2ltc  33184  dplti  33202  dpmul  33210  dpmul4  33211  ressplusf  33261  xrsclat  33309  xrge00  33312  xrnarchi  33482  elrgspnlem2  33541  1fldgenq  33621  xrge0slmod  33646  zringfrac  33822  esplyind  33943  ply1degltdimlem  33990  ccfldsrarelvec  34039  ccfldextdgrr  34040  locfinreflem  34208  locfinref  34209  unicls  34271  sqsscirc1  34276  mhmhmeotmd  34295  raddcn  34297  xrge0iifiso  34303  xrge0iifhmeo  34304  lmxrge0  34320  cnzh  34336  rezh  34337  qqh0  34352  qqh1  34353  qqhre  34388  rrhre  34389  esumnul  34416  esum0  34417  esumsnf  34432  esumpfinvallem  34442  esumpfinvalf  34444  esumpcvgval  34446  esumcvgsum  34456  esumsup  34457  esumcvgre  34459  sigaclfu2  34489  dmsigagen  34512  ddemeas  34604  mbfmvolf  34634  br2base  34637  omssubadd  34668  sibfof  34708  sitg0  34714  eulerpartlemt  34739  eulerpartgbij  34740  0rrv  34819  coinfliplem  34847  coinflipprob  34848  coinfliprv  34851  ballotlem2  34857  ballotlem4  34867  ballotlem5  34868  ballotlemi1  34871  ballotlem7  34904  ballotth  34906  signsplypnf  34915  signsply0  34916  signsw0g  34921  signswch  34926  signsvf0  34945  hashreprin  34985  reprfz1  34989  chtvalz  34994  hgt750lemd  35013  hgt750lem  35016  hgt750lem2  35017  bnj1098  35150  bnj1109  35153  bnj1131  35154  bnj1533  35218  bnj151  35243  bnj580  35279  bnj852  35287  bnj864  35288  bnj865  35289  bnj978  35315  bnj1021  35332  bnj907  35333  bnj1093  35346  bnj1145  35359  bnj1172  35367  bnj1174  35369  bnj1176  35371  bnj1186  35373  nfan1c  35439  xoromon  35457  rankfo  35483  fineqvac  35507  tz9.1regs  35525  axpowg  35537  onvf1odlem4  35568  onvf1od  35569  subfacf  35645  subfacp1lem1  35649  subfacp1lem5  35654  subfacp1lem6  35655  subfacval3  35659  erdszelem2  35662  kur14lem4  35679  ioosconn  35717  iccllysconn  35720  satfn  35825  fmlaomn0  35860  gonan0  35862  goaln0  35863  elnanelprv  35899  msrfo  36016  mthmpps  36052  problem5  36139  quad3  36140  circum  36144  antnestALT  36164  axextprim  36171  axrepprim  36172  axunprim  36173  axinfprim  36176  axacprim  36177  bcneg1  36206  dfon2lem2  36252  dfon2lem4  36254  axextdfeq  36265  fobigcup  36368  snelsingles  36390  fullfunfnv  36416  fullfunfv  36417  rankaltopb  36449  rank0  36640  rankeq1o  36641  hfuni  36654  in-ax8  36714  fneer  36842  neibastop1  36848  nabi1i  36883  nabi2i  36884  limsucncmpi  36934  tz9.1ctco  36971  ttctr3  36984  ttcpwss  37004  knoppcnlem8  37067  knoppcnlem11  37070  cnndvlem1  37104  bj-consensusALT  37150  bj-sbidmOLD  37463  bj-n0i  37565  bj-snsetex  37577  bj-tagss  37594  bj-2upln0  37637  bj-2upln1upl  37638  bj-nuliota  37671  bj-axseprep  37689  bj-0int  37721  bj-elid5  37791  bj-inftyexpitaufo  37824  bj-pinftyccb  37843  bj-minftyccb  37847  bj-pinftynminfty  37849  bj-isrvec  37916  iccioo01  37951  f1omptsnlem  37960  mptsnunlem  37962  topdifinffinlem  37971  relowlpssretop  37988  1oequni2o  37992  pibt2  38041  imadifss  38224  tan2h  38241  poimirlem3  38252  poimirlem9  38258  poimirlem16  38265  poimirlem17  38266  poimirlem18  38267  poimirlem19  38268  poimirlem20  38269  poimirlem22  38271  poimirlem30  38279  mblfinlem1  38286  mblfinlem2  38287  ovoliunnfl  38291  voliunnfl  38293  itg2addnclem  38300  itg2addnclem2  38301  asindmre  38332  areacirclem1  38337  fdc  38374  cntotbnd  38425  heiborlem6  38445  rrnval  38456  reheibor  38468  rngosn3  38553  brcnvrabga  38969  cnvresrn  38975  moantr  38999  inxp2  39002  dfxrn2  39012  dfsucmap3  39090  dfpre4  39107  cnvcosseq  39154  refrelcosslem  39179  1cosscnvxrn  39192  redundss3  39339  refrelsredund3  39345  refrelredund3  39348  disjimeceqim  39431  eqvrel0  39516  eqvrelid  39519  prter2  39633  renegclALT  39715  mapdunirnN  42402  lcmeprodgcdi  42752  3factsumint2  42767  3factsumint3  42768  3factsumint4  42769  3factsumint  42770  lcmineqlem4  42777  3lexlogpow5ineq1  42799  3lexlogpow2ineq1  42803  dvrelogpow2b  42813  aks4d1p1p4  42816  aks4d1p8  42832  aks6d1c1  42861  aks6d1c2p2  42864  aks6d1c4  42869  2ap1caineq  42890  sticksstones1  42891  sticksstones2  42892  aks6d1c7lem2  42926  aks5lem3a  42934  aks5lem6  42937  unitscyglem2  42941  unitscyglem3  42942  sqdeccom12  43028  readvrec2  43100  readvcot  43103  resubf  43120  sn-0ne2  43145  sn-subf  43168  sn-nnne0  43212  sn-0lt1  43227  reneg1lt0  43232  rntrclfvOAI  43402  diophrw  43470  rabren3dioph  43522  pellexlem6  43541  pellex  43542  frmx  43620  frmy  43621  jm2.23  43703  jm2.27dlem3  43718  axac10  43740  pw2f1ocnv  43744  kelac2lem  43771  lmhmlnmsplit  43794  pwfi2f1o  43803  frlmpwfi  43805  insucid  44110  nla0003  44131  ifpbiidcor  44180  sucomisnotcard  44250  alephiso2  44264  alephiso3  44265  cnvnonrel  44294  rnnonrel  44297  resnonrel  44298  cononrel1  44300  cononrel2  44301  fvnonrel  44303  cnvcnvintabd  44306  cnvintabd  44309  rclexi  44321  rtrclex  44323  clcnvlem  44329  cnvrcl0  44331  dmtrcl  44333  rntrcl  44334  dfrtrcl5  44335  iunrelexp0  44408  dmtrclfvRP  44436  rntrclfv  44438  corcltrcl  44445  cotrclrcl  44448  0heALT  44489  frege54cor1a  44570  uneqsn  44731  clsk3nimkb  44746  int-sqdefd  44887  int-sqgeq0d  44892  rr-groth  44989  rr-grothprim  44990  rr-grothshort  44994  seff  44999  expgrowthi  45023  expgrowth  45025  binomcxplemnotnn0  45046  ee233  45208  ax6e2nd  45247  in1  45260  dfvd2ani  45272  dfvd2i  45274  dfvd3i  45281  dfvd3ani  45284  e0bi  45464  uun2221  45501  uun2221p1  45502  uun2221p2  45503  en3lpVD  45533  relopabVD  45589  ax6e2ndVD  45596  ax6e2ndALT  45618  permaxpow  45698  pssnssi  45799  nnf1oxpnn  45893  icof  45915  fnmptif  45960  rn1st  45968  negpilt0  45980  xrgtso  46041  supxrleubrnmptf  46145  xrpnf  46179  rexanuz2nf  46186  ioontr  46207  iccdifioo  46211  iccdifprioo  46212  uzinico2  46257  fsummulc1f  46267  fsumiunss  46271  fnlimfvre2  46371  limsupreuz  46431  limsup10ex  46467  icccncfext  46581  dvcosre  46606  dvsinax  46607  ioodvbdlimc1lem2  46626  ioodvbdlimc2lem  46628  dvmptmulf  46631  dvnmul  46637  dvmptfprodlem  46638  dvnprodlem2  46641  stoweidlem1  46695  stoweidlem26  46720  stoweidlem34  46728  stoweidlem44  46738  stoweid  46757  stirlinglem5  46772  dirkercncflem1  46797  fourierdlem44  46845  fourierdlem56  46856  fourierdlem62  46862  fourierdlem89  46889  fourierdlem91  46891  fourierdlem100  46900  fourierdlem102  46902  fourierdlem103  46903  fourierdlem104  46904  fourierdlem108  46908  fourierdlem112  46912  fourierdlem114  46914  fouriersw  46925  rrndistlt  46984  gsumge0cl  47065  sge0tsms  47074  sge0ltfirpmpt2  47120  ovn0  47260  hoidmv1le  47288  hoidmvle  47294  ovnsubadd2lem  47339  ovolval4lem1  47343  vonioolem2  47375  smflimlem3  47467  nsssmfmbf  47473  chnerlem1  47578  nthrucw  47582  goldrasin  47596  goldrapos  47597  sinnpoly  47605  axorbtnotaiffb  47617  axorbciffatcxorb  47619  abnotbtaxb  47629  euabsneu  47742  ceilhalf1  48052  sprval  48205  fmtnoinf  48265  nprmdvdsfacm1lem2  48350  ppivalnnnprmge6  48355  ppivalnn4  48356  ppivalnn  48361  1nevenALTV  48433  nfermltl8rev  48484  nfermltl2rev  48485  nnsum3primes4  48530  tgblthelfgott  48557  tgoldbachlt  48558  cycl3grtri  48689  isubgr3stgrlem3  48710  usgrexmpl1lem  48763  usgrexmpl2lem  48768  usgrexmpl2trifr  48779  gpgprismgr4cycllem7  48843  ldepslinc  49266  ackval42  49453  rrx2plordso  49481  vsn  49567  dmtposss  49631  sepfsepc  49683  basresposfo  49733  rescofuf  49848  oppff1  49903  idfth  49913  idsubc  49915  fuco2eld2  50069  fuco22a  50105  setc1onsubc  50357  alimp-no-surprise  50536  aacllem  50578  amgmwlem  50579  amgmlemALT  50580