Theorem mpbi 230

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

Syntax hints:   ↔ wb 206

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 207

This theorem is referenced by:  pm5.74i  271  notbii  320  biluk  385  pm5.19  386  pm3.24  402  dfbi  475  pm4.71i  559  pm5.32i  574  biadani  820  biadanii  822  imori  855  ori  862  pm5.16  1016  dn1  1058  3ori  1427  cadan  1611  nic-dfim  1671  nic-dfneg  1672  nic-mp  1673  nic-mpALT  1674  tbw-negdf  1701  rb-imdf  1752  nfri  1791  mpgbi  1800  19.35i  1880  nfim1  2207  19.36i  2239  ax6  2389  sbie  2507  datisi  2681  disamis  2682  dimatis  2689  fresison  2690  bamalip  2693  axi12  2707  eqcomi  2746  eqtri  2760  eleqtri  2835  nfnfc  2912  neii  2935  necomi  2987  neeqtri  3005  neli  3039  nrex  3066  rexlimi  3238  eueqi  3656  euxfr2w  3667  euxfr2  3669  reuxfrd  3695  cdeqri  3713  sseqtri  3971  pssn2lp  4045  equncomi  4101  unssi  4132  ssini  4181  unabs  4206  inabs  4207  dfin4  4219  vn0  4286  inindif  4316  difidALT  4318  ab0orv  4324  ab0orvALT  4325  disjdif  4413  difin0  4415  pwundif  4566  snid  4607  rabrsn  4669  iinrab2  5013  symdifv  5029  rintn0  5052  breqtri  5111  axsepgfromrep  5229  bm1.3iiOLD  5237  ax6vsep  5238  notzfaus  5298  zfpow  5301  dtruALT2  5305  dtruALT  5323  reusv2lem4  5336  dtru  5382  elOLD  5384  op1stb  5417  copsexgw  5436  copsexg  5437  uniop  5461  rn0  5873  dmresi  6009  somincom  6089  cnvimassrndm  6108  cnvcnv  6148  elid  6155  rescnvcnv  6160  cnvcnvres  6161  cocnvcnv2  6215  cores2  6216  co01  6218  cnviin  6242  predres  6295  iota4an  6472  fnopab  6628  mpt0  6632  fnmpti  6633  f1cnvcnv  6737  f1ovi  6812  eliman0  6869  fvco4i  6933  cnvimainrn  7011  fmpti  7056  funiunfv  7194  oprabss  7466  relmptopab  7608  zfun  7681  tfinds2  7806  omon  7820  2nd0  7940  f1stres  7957  f2ndres  7958  cnvoprab  8004  relmpoopab  8035  df1st2  8039  df2nd2  8040  fsplit  8058  frpoins3xpg  8081  frpoins3xp3g  8082  poxp2  8084  poseq  8099  reldmtpos  8175  dftpos4  8186  tpostpos  8187  tpos0  8197  frrlem4  8230  smo0  8289  tfrlem14  8321  tfrlem16  8323  rdgsucg  8353  rdglimg  8355  frfnom  8365  oawordeulem  8480  uniixp  8860  dfdom2  8916  ssdomg  8938  xpcomf1o  8995  sbthlem5  9020  sdom0  9038  limensuci  9082  1sdom2  9149  fiint  9228  fidomdm  9235  residfi  9239  mptfi  9252  fisn  9331  dffi3  9335  ordtypelem6  9429  ordtypelem7  9430  wemaplem2  9453  harwdom  9497  nelaneq  9507  suc11reg  9529  zfinf  9549  axinf2  9550  noinfep  9570  cantnfvalf  9575  cantnflt  9582  cantnf0  9585  cantnf  9603  ttrclco  9628  tz9.1c  9640  tc2  9650  setinds  9659  r111  9688  r1tr2  9690  r1ordg  9691  r1sssuc  9696  r1val1  9699  tz9.13  9704  r1elssi  9718  pwwf  9720  rankopb  9765  rankeq0b  9773  ranksuc  9778  rankmapu  9791  rankxplim3  9794  rankxpsuc  9795  cp  9804  karden  9808  card0  9871  cardlim  9885  cardom  9899  infxpenlem  9924  alephsuc2  9991  alephgeom  9993  unialeph  10012  dfac4  10033  dfacacn  10053  dju1dif  10084  dju1p1e2  10085  infdju1  10101  ackbij1lem13  10142  ackbij2  10153  cf0  10162  cfsuc  10168  cfom  10175  cfslb2n  10179  ominf4  10223  fin23lem17  10249  fin23lem28  10251  fin23lem30  10253  fin23lem31  10254  fin23lem40  10262  isfin1-3  10297  dfacfin7  10310  fin1a2lem6  10316  itunitc1  10331  axcc3  10349  dcomex  10358  axdc2lem  10359  axcclem  10368  zfac  10371  ac3  10373  ackm  10376  axac2  10377  axac  10378  axaci  10379  cardeqv  10380  numth2  10382  numth  10383  dmct  10435  brdom3  10439  fin71ac  10444  cardf  10461  aleph1  10483  cfpwsdom  10496  smobeth  10498  zfcndrep  10526  zfcndpow  10528  zfcndac  10531  gch2  10587  wunex3  10653  tskpr  10682  inar1  10687  rankcf  10689  tskcard  10693  tskuni  10695  grothpw  10738  axgroth4  10744  grothprim  10746  inaprc  10748  dmaddpi  10802  dmmulpi  10803  1lt2pi  10817  addpqf  10856  mulpqf  10858  1lt2nq  10885  supsrlem  11023  ssxr  11203  gtso  11215  subf  11383  negne0i  11457  mulnzcnf  11784  infrenegsup  12126  neg1lt0  12134  nnne0  12180  halflt1  12359  nn0ssz  12512  3halfnz  12572  zeo  12579  numlt  12633  numltc  12634  le9lt10  12635  decle  12642  uzf  12755  xaddf  13140  xsubge0  13177  xmulf  13188  ixxf  13272  ixxssxr  13274  iooval2  13295  ioof  13364  unirnioo  13366  dfioo2  13367  fzval2  13427  fzf  13428  0nelfz1  13460  fz10  13462  fzpreddisj  13490  4fvwrd4  13565  fzof  13573  fzo0  13600  fldiv4p1lem1div2  13756  fldiv4lem1div2  13758  om2uzoi  13879  faclbnd4lem1  14217  hashkf  14256  hashgval  14257  hashinf  14259  hashresfn  14264  hashnn0n0nn  14315  hashge3el3dif  14411  hash3tpde  14417  rev0  14688  s2dm  14814  f1oun2prg  14841  trclublem  14919  sqrt2gt1lt2  15198  limsupgord  15396  fclim  15477  fsumrelem  15731  ackbijnn  15752  incexclem  15760  incexc  15761  arisum2  15785  georeclim  15796  geoisumr  15802  0.999...  15805  risefall0lem  15950  ege2le3  16014  sin0  16075  ef01bndlem  16110  cos2bnd  16114  cos01gt0  16117  sincos2sgn  16120  sin4lt0  16121  rpnnen2lem3  16142  rpnnen2lem9  16148  rexpen  16154  cnso  16173  dvdslelem  16237  divalglem1  16322  divalglem5  16325  divalglem6  16326  divalglem10  16330  flodddiv4  16343  0bits  16367  sadcf  16381  sadcadd  16386  bitsshft  16403  smupf  16406  gcdf  16440  eucalgf  16511  2prm  16620  dfphi2  16702  pockthi  16836  prmrec  16851  vdwapf  16901  vdwlem6  16915  karatsuba  17012  1259lem5  17063  2503lem3  17067  4001lem4  17072  structcnvcnv  17081  structfn  17084  strleun  17085  imasvscafn  17459  xpsff1o  17489  xrge0base  17529  wunnat  17884  dfinito3  17930  dftermo3  17931  eldmcoa  17990  coapm  17996  catcfuccl  18043  catcxpccl  18131  yonedainv  18205  chnub  18546  smndex1bas  18835  smndex1n0mnd  18841  grpinvfvi  18916  mulgfvi  19007  ressmulgnnd  19012  symgsssg  19400  symgfisg  19401  psgnunilem5  19427  sylow3lem2  19561  oppglsm  19575  efgmf  19646  efgval  19650  efgsf  19662  0frgp  19712  dmdprd  19933  dprdval  19938  invrfval  20327  drngui  20670  rmodislmod  20883  lssintcl  20917  cnfldadd  21317  cnfldmul  21319  cnfldfunALT  21326  dfcnfldOLD  21327  cnfldfunALTOLD  21339  cnfld0  21349  cnfld1  21350  cnfld1OLD  21351  cnfldsub  21354  xrsds  21366  pzriprnglem4  21441  pzriprnglem9  21446  pzriprnglem14  21451  psgnghm  21537  zrhpsgnmhm  21541  ocv1  21636  dsmmbas2  21694  mplsubrglem  21960  opsrtoslem2  22012  evl1maprhm  22322  mdetralt  22551  maducoeval2  22583  eltpsi  22887  unitg  22910  fctop  22947  cctop  22949  ppttop  22950  epttop  22952  leordtvallem1  23153  leordtvallem2  23154  iccordt  23157  iscnp2  23182  discmp  23341  conncompcld  23377  1stcrestlem  23395  2ndcdisj  23399  topnlly  23434  disllycmp  23441  dis1stc  23442  txuni2  23508  xkotf  23528  dfac14lem  23560  prdstps  23572  txindis  23577  tx1stc  23593  xkohaus  23596  xkoptsub  23597  cnmpt1st  23611  cnmpt2nd  23612  ptcmpfi  23756  trfil1  23829  fin1aufil  23875  tgpconncompeqg  24055  tgpconncomp  24056  trust  24172  met1stc  24464  dscmet  24515  retopon  24706  cnfldtopon  24725  xrsxmet  24753  xrsmopn  24756  iimulcn  24883  icopnfhmeo  24888  iccpnfhmeo  24890  xrhmeo  24891  cnheiborlem  24899  lebnumii  24911  ishtpy  24917  htpycc  24925  pco1  24960  pcohtpylem  24964  pcopt  24967  pcopt2  24968  pcoass  24969  pcorevlem  24971  rrxcph  25337  rrx0el  25343  ovoliunlem3  25449  ovolicc1  25461  ovolicc2  25467  volf  25474  ioorf  25518  dyadf  25536  dyadmbl  25545  vitalilem5  25557  vitali  25558  mbfimaopnlem  25600  mbflimsup  25611  0plef  25617  i1fima  25623  i1fima2  25624  i1fd  25626  itg1ge0  25631  itg10  25633  i1f1lem  25634  i1fadd  25640  i1fmul  25641  i1fmulc  25648  mbfi1fseqlem5  25664  itg2addlem  25703  reldv  25815  dvbsss  25847  dvef  25925  lhop1lem  25959  deg1fvi  26031  plypf1  26158  coeeulem  26170  coeeu  26171  vieta1lem2  26259  aannenlem3  26278  aalioulem3  26282  dvradcnv  26370  pserulm  26371  pserdvlem2  26378  sinhalfpilem  26412  sincos4thpi  26462  tan4thpiOLD  26464  sincos6thpi  26465  pige3ALT  26469  resinf1o  26485  tanord1  26486  tanregt0  26488  efabl  26499  relogrn  26510  dfrelog  26514  logi  26536  logneg  26537  logltb  26549  logcn  26596  logf1o2  26599  dvlog  26600  efopnlem2  26606  efopn  26607  logccv  26612  dvsqrt  26691  dvcnsqrt  26693  cxpcn3  26698  logblog  26742  angpined  26780  1cubr  26792  asinsin  26842  asin1  26844  reasinsin  26846  atan0  26858  atanbnd  26876  atan1  26878  log2cnv  26894  log2ub  26899  log2le1  26900  birthday  26904  amgmlem  26940  emcllem5  26950  emgt0  26957  harmonicbnd3  26958  ftalem3  27025  basellem4  27034  sgmf  27095  ppi1  27114  cht1  27115  vma1  27116  ppiltx  27127  sqff1o  27132  ppiublem1  27153  ppiublem2  27154  ppiub  27155  chtub  27163  dchreq  27209  bposlem7  27241  bposlem8  27242  bposlem9  27243  lgsdir2lem2  27277  lgsdir2lem3  27278  chebbnd1  27423  chto1ub  27427  chpo1ubb  27432  pntibndlem1  27540  nosgnn0  27610  ltssolem1  27627  bdayfo  27629  nolt02o  27647  nogt01o  27648  noetasuplem4  27688  noetainflem4  27692  cutbdaybnd2lim  27777  madeun  27864  cutsfo  27885  addsproplem2  27950  addsproplem7  27955  addsprop  27956  negsprop  28015  subsf  28044  mulsproplem13  28108  mulsproplem14  28109  mulsprop  28110  oniso  28251  n0cut  28314  bdayn0sf1o  28350  twocut  28403  bdaypw2n0bndlem  28443  bdayfinbndlem1  28447  0reno  28476  tgldimor  28558  tglnfn  28603  axlowdimlem4  29002  axlowdimlem16  29014  axlowdim  29018  upgrfi  29148  lfgrnloop  29182  lfuhgr1v0e  29311  usgrexmplef  29316  usgrres  29365  vdegp1bi  29595  vtxdginducedm1lem2  29598  dfpth2  29786  pthdlem2  29825  wpthswwlks2on  30021  0ewlk  30173  0pth  30184  konigsbergiedgw  30307  konigsberglem1  30311  konigsberglem2  30312  konigsberglem3  30313  konigsberglem4  30314  konigsberglem5  30315  ex-dif  30482  ex-un  30483  ex-in  30484  ex-fl  30506  avril1  30522  9p10ne21fool  30530  n0lplig  30543  cnidOLD  30642  cnnvm  30742  ipasslem8  30897  ipasslem10  30899  hvsubf  31075  normlem1  31170  normlem6  31175  normlem7  31176  norm-ii-i  31197  norm3adifii  31208  hilid  31221  hlimf  31297  hhssabloi  31322  hhssnv  31324  hhshsslem1  31327  shincli  31422  shsval2i  31447  shs0i  31509  chj0i  31515  chm1i  31516  chincli  31520  chdmm1i  31537  shjshsi  31552  chsup0  31608  h1de2bi  31614  spansnpji  31638  cmcmlem  31651  cmcmii  31657  cmcm2ii  31658  cmcm3ii  31659  pjidmi  31733  pjssmii  31741  pj0i  31753  pjocini  31758  mayetes3i  31789  df0op2  31812  hoaddcomi  31832  hoaddassi  31836  hocadddiri  31839  hocsubdiri  31840  hoaddridi  31846  ho0coi  31848  hoid1i  31849  hoid1ri  31850  hodseqi  31854  honegsubi  31856  adj1o  31954  hoddii  32049  lnopunilem1  32070  lnopunilem2  32071  nmcopexi  32087  nmcopex  32089  nmcoplb  32090  nmcfnexi  32111  nmcfnex  32113  nmcfnlb  32114  adjbd1o  32145  adjcoi  32160  nmopcoadji  32161  opsqrlem6  32205  pjsdii  32215  pjddii  32216  pjidmcoi  32237  pjtoi  32239  pjin1i  32252  pjclem1  32255  stji1i  32302  reuxfrdf  32549  iuninc  32619  fnresin  32686  rinvf1o  32692  suppss2f  32700  xppreima  32707  ofoprabco  32726  partfun2  32738  fressupp  32750  supppreima  32753  fsupprnfi  32754  gtiso  32763  df1stres  32766  df2ndres  32767  snct  32774  padct  32780  fsuppcurry1  32786  fsuppcurry2  32787  ffsrn  32790  fpwrelmapffs  32796  fzodif1  32855  nnindf  32883  nn0min  32884  dp2lt  32949  dp2ltsuc  32950  dp2ltc  32951  dplti  32969  dpmul  32977  dpmul4  32978  ressplusf  33028  xrsclat  33076  xrge00  33079  xrnarchi  33250  elrgspnlem2  33309  1fldgenq  33388  xrge0slmod  33413  zringfrac  33619  esplyind  33724  ply1degltdimlem  33772  ccfldsrarelvec  33821  ccfldextdgrr  33822  locfinreflem  33990  locfinref  33991  unicls  34053  sqsscirc1  34058  mhmhmeotmd  34077  raddcn  34079  xrge0iifiso  34085  xrge0iifhmeo  34086  lmxrge0  34102  cnzh  34118  rezh  34119  qqh0  34134  qqh1  34135  qqhre  34170  rrhre  34171  esumnul  34198  esum0  34199  esumsnf  34214  esumpfinvallem  34224  esumpfinvalf  34226  esumpcvgval  34228  esumcvgsum  34238  esumsup  34239  esumcvgre  34241  sigaclfu2  34271  dmsigagen  34294  ddemeas  34386  mbfmvolf  34416  br2base  34419  omssubadd  34450  sibfof  34490  sitg0  34496  eulerpartlemt  34521  eulerpartgbij  34522  0rrv  34601  coinfliplem  34629  coinflipprob  34630  coinfliprv  34633  ballotlem2  34639  ballotlem4  34649  ballotlem5  34650  ballotlemi1  34653  ballotlem7  34686  ballotth  34688  signsplypnf  34700  signsply0  34701  signsw0g  34706  signswch  34711  signsvf0  34730  hashreprin  34770  reprfz1  34774  chtvalz  34779  hgt750lemd  34798  hgt750lem  34801  hgt750lem2  34802  bnj1098  34932  bnj1109  34935  bnj1131  34936  bnj1533  35000  bnj151  35025  bnj580  35061  bnj852  35069  bnj864  35070  bnj865  35071  bnj978  35097  bnj1021  35114  bnj907  35115  bnj1093  35128  bnj1145  35141  bnj1172  35149  bnj1174  35151  bnj1176  35153  bnj1186  35155  nfan1c  35221  xoromon  35238  fineqvac  35266  tz9.1regs  35284  onvf1odlem4  35294  onvf1od  35295  subfacf  35363  subfacp1lem1  35367  subfacp1lem5  35372  subfacp1lem6  35373  subfacval3  35377  erdszelem2  35380  kur14lem4  35397  ioosconn  35435  iccllysconn  35438  satfn  35543  fmlaomn0  35578  gonan0  35580  goaln0  35581  elnanelprv  35617  msrfo  35734  mthmpps  35770  problem5  35857  quad3  35858  circum  35862  antnestALT  35882  axextprim  35889  axrepprim  35890  axunprim  35891  axinfprim  35894  axacprim  35895  bcneg1  35924  dfon2lem2  35970  dfon2lem4  35972  axextdfeq  35983  fobigcup  36086  snelsingles  36108  fullfunfnv  36134  fullfunfv  36135  rankaltopb  36167  rank0  36358  rankeq1o  36359  hfuni  36372  in-ax8  36412  fneer  36541  neibastop1  36547  nabi1i  36582  nabi2i  36583  limsucncmpi  36633  tz9.1ctco  36670  ttctr3  36683  ttcpwss  36703  knoppcnlem8  36758  knoppcnlem11  36761  cnndvlem1  36795  bj-consensusALT  36842  bj-sbidmOLD  37155  bj-n0i  37256  bj-snsetex  37268  bj-tagss  37285  bj-2upln0  37328  bj-2upln1upl  37329  bj-nuliota  37362  bj-axseprep  37379  bj-0int  37411  bj-elid5  37481  bj-inftyexpitaufo  37514  bj-pinftyccb  37533  bj-minftyccb  37537  bj-pinftynminfty  37539  bj-isrvec  37606  iccioo01  37639  f1omptsnlem  37648  mptsnunlem  37650  topdifinffinlem  37659  relowlpssretop  37676  1oequni2o  37680  pibt2  37729  imadifss  37907  tan2h  37924  poimirlem3  37935  poimirlem9  37941  poimirlem16  37948  poimirlem17  37949  poimirlem18  37950  poimirlem19  37951  poimirlem20  37952  poimirlem22  37954  poimirlem30  37962  mblfinlem1  37969  mblfinlem2  37970  ovoliunnfl  37974  voliunnfl  37976  itg2addnclem  37983  itg2addnclem2  37984  asindmre  38015  areacirclem1  38020  fdc  38057  cntotbnd  38108  heiborlem6  38128  rrnval  38139  reheibor  38151  rngosn3  38236  brcnvrabga  38654  cnvresrn  38660  moantr  38684  inxp2  38687  dfxrn2  38697  dfsucmap3  38775  dfpre4  38792  cnvcosseq  38839  refrelcosslem  38864  1cosscnvxrn  38877  redundss3  39024  refrelsredund3  39030  refrelredund3  39033  disjimeceqim  39116  eqvrel0  39201  eqvrelid  39204  prter2  39318  renegclALT  39400  mapdunirnN  42087  lcmeprodgcdi  42438  3factsumint2  42453  3factsumint3  42454  3factsumint4  42455  3factsumint  42456  lcmineqlem4  42463  3lexlogpow5ineq1  42485  3lexlogpow2ineq1  42489  dvrelogpow2b  42499  aks4d1p1p4  42502  aks4d1p8  42518  aks6d1c1  42547  aks6d1c2p2  42550  aks6d1c4  42555  2ap1caineq  42576  sticksstones1  42577  sticksstones2  42578  aks6d1c7lem2  42612  aks5lem3a  42620  aks5lem6  42623  unitscyglem2  42627  unitscyglem3  42628  sqdeccom12  42720  readvrec2  42792  readvcot  42795  resubf  42812  sn-0ne2  42837  sn-subf  42860  sn-nnne0  42904  sn-0lt1  42919  reneg1lt0  42924  rntrclfvOAI  43122  diophrw  43190  rabren3dioph  43246  pellexlem6  43265  pellex  43266  frmx  43344  frmy  43345  jm2.23  43427  jm2.27dlem3  43442  axac10  43464  pw2f1ocnv  43468  kelac2lem  43495  lmhmlnmsplit  43518  pwfi2f1o  43527  frlmpwfi  43529  insucid  43834  nla0003  43855  ifpbiidcor  43904  sucomisnotcard  43974  alephiso2  43988  alephiso3  43989  cnvnonrel  44018  rnnonrel  44021  resnonrel  44022  cononrel1  44024  cononrel2  44025  fvnonrel  44027  cnvcnvintabd  44030  cnvintabd  44033  rclexi  44045  rtrclex  44047  clcnvlem  44053  cnvrcl0  44055  dmtrcl  44057  rntrcl  44058  dfrtrcl5  44059  iunrelexp0  44132  dmtrclfvRP  44160  rntrclfv  44162  corcltrcl  44169  cotrclrcl  44172  0heALT  44213  frege54cor1a  44294  uneqsn  44455  clsk3nimkb  44470  int-sqdefd  44611  int-sqgeq0d  44616  rr-groth  44729  rr-grothprim  44730  rr-grothshort  44734  seff  44739  expgrowthi  44763  expgrowth  44765  binomcxplemnotnn0  44786  ee233  44949  ax6e2nd  44988  in1  45001  dfvd2ani  45013  dfvd2i  45015  dfvd3i  45022  dfvd3ani  45025  e0bi  45205  uun2221  45242  uun2221p1  45243  uun2221p2  45244  en3lpVD  45274  relopabVD  45330  ax6e2ndVD  45337  ax6e2ndALT  45359  permaxpow  45439  pssnssi  45534  nnf1oxpnn  45628  icof  45651  fnmptif  45697  rn1st  45705  negpilt0  45717  xrgtso  45778  supxrleubrnmptf  45883  xrpnf  45917  rexanuz2nf  45924  ioontr  45945  iccdifioo  45949  iccdifprioo  45950  uzinico2  45995  fsummulc1f  46005  fsumiunss  46009  fnlimfvre2  46109  limsupreuz  46169  limsup10ex  46205  icccncfext  46319  dvcosre  46344  dvsinax  46345  ioodvbdlimc1lem2  46364  ioodvbdlimc2lem  46366  dvmptmulf  46369  dvnmul  46375  dvmptfprodlem  46376  dvnprodlem2  46379  stoweidlem1  46433  stoweidlem26  46458  stoweidlem34  46466  stoweidlem44  46476  stoweid  46495  stirlinglem5  46510  dirkercncflem1  46535  fourierdlem44  46583  fourierdlem56  46594  fourierdlem62  46600  fourierdlem89  46627  fourierdlem91  46629  fourierdlem100  46638  fourierdlem102  46640  fourierdlem103  46641  fourierdlem104  46642  fourierdlem108  46646  fourierdlem112  46650  fourierdlem114  46652  fouriersw  46663  rrndistlt  46722  gsumge0cl  46803  sge0tsms  46812  sge0ltfirpmpt2  46858  ovn0  46998  hoidmv1le  47026  hoidmvle  47032  ovnsubadd2lem  47077  ovolval4lem1  47081  vonioolem2  47113  smflimlem3  47205  nsssmfmbf  47211  chnerlem1  47314  nthrucw  47318  sinnpoly  47325  axorbtnotaiffb  47337  axorbciffatcxorb  47339  abnotbtaxb  47349  euabsneu  47462  ceilhalf1  47768  sprval  47913  fmtnoinf  47970  1nevenALTV  48125  nfermltl8rev  48176  nfermltl2rev  48177  nnsum3primes4  48222  tgblthelfgott  48249  tgoldbachlt  48250  cycl3grtri  48381  isubgr3stgrlem3  48402  usgrexmpl1lem  48455  usgrexmpl2lem  48460  usgrexmpl2trifr  48471  gpgprismgr4cycllem7  48535  ldepslinc  48943  ackval42  49130  rrx2plordso  49158  vsn  49245  dmtposss  49309  sepfsepc  49361  basresposfo  49411  rescofuf  49526  oppff1  49581  idfth  49591  idsubc  49593  fuco2eld2  49747  fuco22a  49783  setc1onsubc  50035  alimp-no-surprise  50214  aacllem  50234  amgmwlem  50235  amgmlemALT  50236