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  819  biadanii  821  imori  853  ori  860  pm5.16  1014  dn1  1058  3ori  1424  cadan  1606  nic-dfim  1667  nic-dfneg  1668  nic-mp  1669  nic-mpALT  1670  tbw-negdf  1697  rb-imdf  1748  nfri  1787  mpgbi  1796  19.35i  1877  nfim1  2200  19.36i  2232  ax6  2392  sbie  2510  datisi  2683  disamis  2684  dimatis  2691  fresison  2692  bamalip  2695  axi12  2709  eqcomi  2749  eqtri  2768  eleqtri  2842  nfnfc  2921  neii  2948  necomi  3001  neeqtri  3019  neli  3054  nrex  3080  rexlimivOLD  3191  rexlimi  3265  nfra2wOLD  3306  eueqi  3731  euxfr2w  3742  euxfr2  3744  reuxfrd  3770  cdeqri  3788  sseqtri  4045  3sstr3i  4051  pssn2lp  4127  equncomi  4183  unssi  4214  ssini  4261  unabs  4284  inabs  4285  dfin4  4297  vn0  4368  difidALT  4399  ab0orv  4406  ab0orvALT  4407  disjdif  4495  difin0  4497  pwundif  4646  snid  4684  rabrsn  4749  iinrab2  5093  symdifv  5109  rintn0  5132  breqtri  5191  axsepgfromrep  5315  bm1.3ii  5320  ax6vsep  5321  notzfaus  5381  zfpow  5384  dtruALT2  5388  dtruALT  5406  reusv2lem4  5419  dtru  5456  el  5457  dtruOLD  5461  op1stb  5491  copsexgw  5510  copsexg  5511  uniop  5534  rn0  5950  dmresi  6081  somincom  6166  cnvimassrndm  6183  cnvcnv  6223  elid  6230  rescnvcnv  6235  cnvcnvres  6236  cocnvcnv2  6289  cores2  6290  co01  6292  cnviin  6317  predres  6371  iota4an  6555  fnopab  6718  mpt0  6722  fnmpti  6723  f1cnvcnv  6826  f1ovi  6901  eliman0  6960  fvco4i  7023  cnvimainrn  7100  fmpti  7146  funiunfv  7285  oprabss  7557  relmptopab  7700  zfun  7771  tfinds2  7901  omon  7915  2nd0  8037  f1stres  8054  f2ndres  8055  cnvoprab  8101  relmpoopab  8135  df1st2  8139  df2nd2  8140  fsplit  8158  frpoins3xpg  8181  frpoins3xp3g  8182  poxp2  8184  poseq  8199  reldmtpos  8275  dftpos4  8286  tpostpos  8287  tpos0  8297  frrlem4  8330  wfrlem4OLD  8368  smo0  8414  tfrlem14  8447  tfrlem16  8449  rdgsucg  8479  rdglimg  8481  frfnom  8491  oawordeulem  8610  uniixp  8979  dfdom2  9038  ssdomg  9060  xpcomf1o  9127  sbthlem5  9153  sdom0  9174  limensuci  9219  1sdom2  9303  fiint  9394  fiintOLD  9395  fidomdm  9402  residfi  9406  pwfilemOLD  9416  mptfi  9421  fisn  9496  dffi3  9500  ordtypelem6  9592  ordtypelem7  9593  wemaplem2  9616  harwdom  9660  suc11reg  9688  zfinf  9708  axinf2  9709  noinfep  9729  cantnfvalf  9734  cantnflt  9741  cantnf0  9744  cantnf  9762  ttrclco  9787  tz9.1c  9799  tc2  9811  r111  9844  r1tr2  9846  r1ordg  9847  r1sssuc  9852  r1val1  9855  tz9.13  9860  r1elssi  9874  pwwf  9876  rankopb  9921  rankeq0b  9929  ranksuc  9934  rankmapu  9947  rankxplim3  9950  rankxpsuc  9951  cp  9960  karden  9964  card0  10027  cardlim  10041  cardom  10055  infxpenlem  10082  alephsuc2  10149  alephgeom  10151  unialeph  10170  dfac4  10191  dfacacn  10211  dju1dif  10242  dju1p1e2  10243  infdju1  10259  ackbij1lem13  10300  ackbij2  10311  cf0  10320  cfsuc  10326  cfom  10333  cfslb2n  10337  ominf4  10381  fin23lem17  10407  fin23lem28  10409  fin23lem30  10411  fin23lem31  10412  fin23lem40  10420  isfin1-3  10455  dfacfin7  10468  fin1a2lem6  10474  itunitc1  10489  axcc3  10507  dcomex  10516  axdc2lem  10517  axcclem  10526  zfac  10529  ac3  10531  ackm  10534  axac2  10535  axac  10536  axaci  10537  cardeqv  10538  numth2  10540  numth  10541  dmct  10593  brdom3  10597  fin71ac  10602  cardf  10619  aleph1  10640  cfpwsdom  10653  smobeth  10655  zfcndrep  10683  zfcndpow  10685  zfcndac  10688  gch2  10744  wunex3  10810  tskpr  10839  inar1  10844  rankcf  10846  tskcard  10850  tskuni  10852  grothpw  10895  axgroth4  10901  grothprim  10903  inaprc  10905  dmaddpi  10959  dmmulpi  10960  1lt2pi  10974  addpqf  11013  mulpqf  11015  1lt2nq  11042  supsrlem  11180  ssxr  11359  gtso  11371  subf  11538  negne0i  11611  mulnzcnf  11936  infrenegsup  12278  nnne0  12327  halflt1  12511  nn0ssz  12662  3halfnz  12722  zeo  12729  numlt  12783  numltc  12784  le9lt10  12785  decle  12792  uzf  12906  xaddf  13286  xsubge0  13323  xmulf  13334  ixxf  13417  ixxssxr  13419  iooval2  13440  ioof  13507  unirnioo  13509  dfioo2  13510  fzval2  13570  fzf  13571  0nelfz1  13603  fz10  13605  fzpreddisj  13633  4fvwrd4  13705  fzof  13713  fzo0  13740  fldiv4p1lem1div2  13886  fldiv4lem1div2  13888  om2uzoi  14006  faclbnd4lem1  14342  hashkf  14381  hashgval  14382  hashinf  14384  hashresfn  14389  hashnn0n0nn  14440  hashge3el3dif  14536  hash3tpde  14542  rev0  14812  s2dm  14939  f1oun2prg  14966  trclublem  15044  sqrt2gt1lt2  15323  limsupgord  15518  fclim  15599  fsumrelem  15855  ackbijnn  15876  incexclem  15884  incexc  15885  arisum2  15909  georeclim  15920  geoisumr  15926  0.999...  15929  risefall0lem  16074  ege2le3  16138  sin0  16197  ef01bndlem  16232  cos2bnd  16236  cos01gt0  16239  sincos2sgn  16242  sin4lt0  16243  rpnnen2lem3  16264  rpnnen2lem9  16270  rexpen  16276  cnso  16295  dvdslelem  16357  divalglem1  16442  divalglem5  16445  divalglem6  16446  divalglem10  16450  flodddiv4  16461  0bits  16485  sadcf  16499  sadcadd  16504  bitsshft  16521  smupf  16524  gcdf  16558  eucalgf  16630  2prm  16739  dfphi2  16821  pockthi  16954  prmrec  16969  vdwapf  17019  vdwlem6  17033  karatsuba  17131  1259lem5  17182  2503lem3  17186  4001lem4  17191  structcnvcnv  17200  structfn  17203  strleun  17204  imasvscafn  17597  xpsff1o  17627  wunnat  18024  wunnatOLD  18025  dfinito3  18072  dftermo3  18073  eldmcoa  18132  coapm  18138  catcfuccl  18186  catcfucclOLD  18187  catcxpccl  18276  catcxpcclOLD  18277  yonedainv  18351  smndex1bas  18941  smndex1n0mnd  18947  grpinvfvi  19022  mulgfvi  19113  ressmulgnnd  19118  symgsssg  19509  symgfisg  19510  psgnunilem5  19536  sylow3lem2  19670  oppglsm  19684  efgmf  19755  efgval  19759  efgsf  19771  0frgp  19821  dmdprd  20042  dprdval  20047  invrfval  20415  drngui  20757  rmodislmod  20950  rmodislmodOLD  20951  lssintcl  20985  cnfldadd  21393  cnfldmul  21395  cnfldfunALT  21402  dfcnfldOLD  21403  cnfldfunALTOLD  21415  cnfldfunALTOLDOLD  21416  cnfld0  21428  cnfld1  21429  cnfld1OLD  21430  cnfldsub  21433  xrsds  21450  pzriprnglem4  21518  pzriprnglem9  21523  pzriprnglem14  21528  psgnghm  21621  zrhpsgnmhm  21625  ocv1  21720  dsmmbas2  21780  mplsubrglem  22047  opsrtoslem2  22103  evl1maprhm  22404  mdetralt  22635  maducoeval2  22667  eltpsi  22972  unitg  22995  fctop  23032  cctop  23034  ppttop  23035  epttop  23037  leordtvallem1  23239  leordtvallem2  23240  iccordt  23243  iscnp2  23268  discmp  23427  conncompcld  23463  1stcrestlem  23481  2ndcdisj  23485  topnlly  23520  disllycmp  23527  dis1stc  23528  txuni2  23594  xkotf  23614  dfac14lem  23646  prdstps  23658  txindis  23663  tx1stc  23679  xkohaus  23682  xkoptsub  23683  cnmpt1st  23697  cnmpt2nd  23698  ptcmpfi  23842  trfil1  23915  fin1aufil  23961  tgpconncompeqg  24141  tgpconncomp  24142  trust  24259  met1stc  24555  dscmet  24606  retopon  24805  cnfldtopon  24824  xrsxmet  24850  xrsmopn  24853  iimulcn  24986  iimulcnOLD  24987  icopnfhmeo  24993  iccpnfhmeo  24995  xrhmeo  24996  cnheiborlem  25005  lebnumii  25017  ishtpy  25023  htpycc  25031  pco1  25067  pcohtpylem  25071  pcopt  25074  pcopt2  25075  pcoass  25076  pcorevlem  25078  rrxcph  25445  rrx0el  25451  ovoliunlem3  25558  ovolicc1  25570  ovolicc2  25576  volf  25583  ioorf  25627  dyadf  25645  dyadmbl  25654  vitalilem5  25666  vitali  25667  mbfimaopnlem  25709  mbflimsup  25720  0plef  25726  i1fima  25732  i1fima2  25733  i1fd  25735  itg1ge0  25740  itg10  25742  i1f1lem  25743  i1fadd  25749  i1fmul  25750  i1fmulc  25758  mbfi1fseqlem5  25774  itg2addlem  25813  reldv  25925  dvbsss  25957  dvef  26038  lhop1lem  26072  deg1fvi  26144  plypf1  26271  coeeulem  26283  coeeu  26284  vieta1lem2  26371  aannenlem3  26390  aalioulem3  26394  dvradcnv  26482  pserulm  26483  pserdvlem2  26490  sinhalfpilem  26523  sincos4thpi  26573  tan4thpiOLD  26575  sincos6thpi  26576  pige3ALT  26580  resinf1o  26596  tanord1  26597  tanregt0  26599  efabl  26610  relogrn  26621  dfrelog  26625  logi  26647  logneg  26648  logltb  26660  logcn  26707  logf1o2  26710  dvlog  26711  efopnlem2  26717  efopn  26718  logccv  26723  dvsqrt  26802  dvcnsqrt  26804  cxpcn3  26809  logblog  26853  angpined  26891  1cubr  26903  asinsin  26953  asin1  26955  reasinsin  26957  atan0  26969  atanbnd  26987  atan1  26989  log2cnv  27005  log2ub  27010  log2le1  27011  birthday  27015  amgmlem  27051  emcllem5  27061  emgt0  27068  harmonicbnd3  27069  ftalem3  27136  basellem4  27145  sgmf  27206  ppi1  27225  cht1  27226  vma1  27227  ppiltx  27238  sqff1o  27243  ppiublem1  27264  ppiublem2  27265  ppiub  27266  chtub  27274  dchreq  27320  bposlem7  27352  bposlem8  27353  bposlem9  27354  lgsdir2lem2  27388  lgsdir2lem3  27389  chebbnd1  27534  chto1ub  27538  chpo1ubb  27543  pntibndlem1  27651  nosgnn0  27721  sltsolem1  27738  bdayfo  27740  nolt02o  27758  nogt01o  27759  noetasuplem4  27799  noetainflem4  27803  scutbdaybnd2lim  27880  madeun  27940  scutfo  27960  addsproplem2  28021  addsproplem7  28026  addsprop  28027  negsprop  28085  subsf  28112  mulsproplem13  28172  mulsproplem14  28173  mulsprop  28174  n0scut  28356  nohalf  28425  pw2bday  28436  0reno  28447  tgldimor  28528  tglnfn  28573  axlowdimlem4  28978  axlowdimlem16  28990  axlowdim  28994  upgrfi  29126  lfgrnloop  29160  lfuhgr1v0e  29289  usgrexmplef  29294  usgrres  29343  vdegp1bi  29573  vtxdginducedm1lem2  29576  pthdlem2  29804  wpthswwlks2on  29994  0ewlk  30146  0pth  30157  konigsbergiedgw  30280  konigsberglem1  30284  konigsberglem2  30285  konigsberglem3  30286  konigsberglem4  30287  konigsberglem5  30288  ex-dif  30455  ex-un  30456  ex-in  30457  ex-fl  30479  avril1  30495  9p10ne21fool  30503  n0lplig  30515  cnidOLD  30614  cnnvm  30714  ipasslem8  30869  ipasslem10  30871  hvsubf  31047  normlem1  31142  normlem6  31147  normlem7  31148  norm-ii-i  31169  norm3adifii  31180  hilid  31193  hlimf  31269  hhssabloi  31294  hhssnv  31296  hhshsslem1  31299  shincli  31394  shsval2i  31419  shs0i  31481  chj0i  31487  chm1i  31488  chincli  31492  chdmm1i  31509  shjshsi  31524  chsup0  31580  h1de2bi  31586  spansnpji  31610  cmcmlem  31623  cmcmii  31629  cmcm2ii  31630  cmcm3ii  31631  pjidmi  31705  pjssmii  31713  pj0i  31725  pjocini  31730  mayetes3i  31761  df0op2  31784  hoaddcomi  31804  hoaddassi  31808  hocadddiri  31811  hocsubdiri  31812  hoaddridi  31818  ho0coi  31820  hoid1i  31821  hoid1ri  31822  hodseqi  31826  honegsubi  31828  adj1o  31926  hoddii  32021  lnopunilem1  32042  lnopunilem2  32043  nmcopexi  32059  nmcopex  32061  nmcoplb  32062  nmcfnexi  32083  nmcfnex  32085  nmcfnlb  32086  adjbd1o  32117  adjcoi  32132  nmopcoadji  32133  opsqrlem6  32177  pjsdii  32187  pjddii  32188  pjidmcoi  32209  pjtoi  32211  pjin1i  32224  pjclem1  32227  stji1i  32274  reuxfrdf  32519  inindif  32546  iuninc  32583  fnresin  32645  rinvf1o  32649  suppss2f  32657  xppreima  32664  ofoprabco  32682  fressupp  32700  supppreima  32703  fsupprnfi  32704  gtiso  32712  df1stres  32715  df2ndres  32716  snct  32727  padct  32733  fsuppcurry1  32739  fsuppcurry2  32740  ffsrn  32743  fpwrelmapffs  32748  fzodif1  32798  nnindf  32823  nn0min  32824  dp2lt  32849  dp2ltsuc  32850  dp2ltc  32851  dplti  32869  dpmul  32877  dpmul4  32878  ressplusf  32930  chnub  32984  xrsclat  32994  xrge0base  32997  xrge00  32998  xrnarchi  33164  1fldgenq  33289  xrge0slmod  33341  zringfrac  33547  ply1degltdimlem  33635  ccfldsrarelvec  33681  ccfldextdgrr  33682  locfinreflem  33786  locfinref  33787  unicls  33849  sqsscirc1  33854  mhmhmeotmd  33873  raddcn  33875  xrge0iifiso  33881  xrge0iifhmeo  33882  lmxrge0  33898  cnzh  33916  rezh  33917  qqh0  33930  qqh1  33931  qqhre  33966  rrhre  33967  esumnul  34012  esum0  34013  esumsnf  34028  esumpfinvallem  34038  esumpfinvalf  34040  esumpcvgval  34042  esumcvgsum  34052  esumsup  34053  esumcvgre  34055  sigaclfu2  34085  dmsigagen  34108  ddemeas  34200  mbfmvolf  34231  br2base  34234  omssubadd  34265  sibfof  34305  sitg0  34311  eulerpartlemt  34336  eulerpartgbij  34337  0rrv  34416  coinfliplem  34443  coinflipprob  34444  coinfliprv  34447  ballotlem2  34453  ballotlem4  34463  ballotlem5  34464  ballotlemi1  34467  ballotlem7  34500  ballotth  34502  signsplypnf  34527  signsply0  34528  signsw0g  34533  signswch  34538  signsvf0  34557  hashreprin  34597  reprfz1  34601  chtvalz  34606  hgt750lemd  34625  hgt750lem  34628  hgt750lem2  34629  bnj1098  34759  bnj1109  34762  bnj1131  34763  bnj1533  34828  bnj151  34853  bnj580  34889  bnj852  34897  bnj864  34898  bnj865  34899  bnj978  34925  bnj1021  34942  bnj907  34943  bnj1093  34956  bnj1145  34969  bnj1172  34977  bnj1174  34979  bnj1176  34981  bnj1186  34983  nfan1c  35049  fineqvac  35073  subfacf  35143  subfacp1lem1  35147  subfacp1lem5  35152  subfacp1lem6  35153  subfacval3  35157  erdszelem2  35160  kur14lem4  35177  ioosconn  35215  iccllysconn  35218  satfn  35323  fmlaomn0  35358  gonan0  35360  goaln0  35361  elnanelprv  35397  msrfo  35514  mthmpps  35550  problem5  35637  quad3  35638  circum  35642  axextprim  35663  axrepprim  35664  axunprim  35665  axinfprim  35668  axacprim  35669  bcneg1  35698  setinds  35742  dfon2lem2  35748  dfon2lem4  35750  axextdfeq  35761  fobigcup  35864  snelsingles  35886  fullfunfnv  35910  fullfunfv  35911  rankaltopb  35943  rank0  36134  rankeq1o  36135  hfuni  36148  in-ax8  36190  fneer  36319  neibastop1  36325  nabi1i  36360  nabi2i  36361  limsucncmpi  36411  knoppcnlem8  36466  knoppcnlem11  36469  cnndvlem1  36503  bj-consensusALT  36545  bj-sbidmOLD  36816  bj-n0i  36917  bj-snsetex  36929  bj-tagss  36946  bj-2upln0  36989  bj-2upln1upl  36990  bj-nuliota  37023  bj-0int  37067  bj-elid5  37135  bj-inftyexpitaufo  37168  bj-pinftyccb  37187  bj-minftyccb  37191  bj-pinftynminfty  37193  bj-isrvec  37260  iccioo01  37293  f1omptsnlem  37302  mptsnunlem  37304  topdifinffinlem  37313  relowlpssretop  37330  1oequni2o  37334  pibt2  37383  imadifss  37555  tan2h  37572  poimirlem3  37583  poimirlem9  37589  poimirlem16  37596  poimirlem17  37597  poimirlem18  37598  poimirlem19  37599  poimirlem20  37600  poimirlem22  37602  poimirlem30  37610  mblfinlem1  37617  mblfinlem2  37618  ovoliunnfl  37622  voliunnfl  37624  itg2addnclem  37631  itg2addnclem2  37632  asindmre  37663  areacirclem1  37668  fdc  37705  cntotbnd  37756  heiborlem6  37776  rrnval  37787  reheibor  37799  rngosn3  37884  brcnvrabga  38298  cnvresrn  38304  moantr  38320  inxp2  38323  dfxrn2  38332  cnvcosseq  38393  refrelcosslem  38418  1cosscnvxrn  38431  redundss3  38584  refrelsredund3  38590  refrelredund3  38593  eqvrel0  38742  eqvrelid  38745  prter2  38837  renegclALT  38919  mapdunirnN  41607  lcmeprodgcdi  41964  3factsumint2  41979  3factsumint3  41980  3factsumint4  41981  3factsumint  41982  lcmineqlem4  41989  3lexlogpow5ineq1  42011  3lexlogpow2ineq1  42015  dvrelogpow2b  42025  aks4d1p1p4  42028  aks4d1p8  42044  aks6d1c1  42073  aks6d1c2p2  42076  aks6d1c4  42081  2ap1caineq  42102  sticksstones1  42103  sticksstones2  42104  aks6d1c7lem2  42138  aks5lem3a  42146  aks5lem6  42149  unitscyglem2  42153  unitscyglem3  42154  metakunt6  42167  metakunt24  42185  sqdeccom12  42278  resubf  42357  sn-0ne2  42382  sn-subf  42404  sn-nnne0  42424  sn-0lt1  42439  reneg1lt0  42442  rntrclfvOAI  42647  diophrw  42715  rabren3dioph  42771  pellexlem6  42790  pellex  42791  frmx  42870  frmy  42871  jm2.23  42953  jm2.27dlem3  42968  axac10  42990  pw2f1ocnv  42994  kelac2lem  43021  lmhmlnmsplit  43044  pwfi2f1o  43053  frlmpwfi  43055  insucid  43365  nla0003  43387  ifpbiidcor  43436  sucomisnotcard  43506  alephiso2  43520  alephiso3  43521  cnvnonrel  43550  rnnonrel  43553  resnonrel  43554  cononrel1  43556  cononrel2  43557  fvnonrel  43559  cnvcnvintabd  43562  cnvintabd  43565  rclexi  43577  rtrclex  43579  clcnvlem  43585  cnvrcl0  43587  dmtrcl  43589  rntrcl  43590  dfrtrcl5  43591  iunrelexp0  43664  dmtrclfvRP  43692  rntrclfv  43694  corcltrcl  43701  cotrclrcl  43704  0heALT  43745  frege54cor1a  43826  uneqsn  43987  clsk3nimkb  44002  int-sqdefd  44143  int-sqgeq0d  44148  rr-groth  44268  rr-grothprim  44269  rr-grothshort  44273  seff  44278  expgrowthi  44302  expgrowth  44304  binomcxplemnotnn0  44325  ee233  44490  ax6e2nd  44529  in1  44542  dfvd2ani  44554  dfvd2i  44556  dfvd3i  44563  dfvd3ani  44566  e0bi  44747  uun2221  44784  uun2221p1  44785  uun2221p2  44786  en3lpVD  44816  relopabVD  44872  ax6e2ndVD  44879  ax6e2ndALT  44901  pssnssi  45003  nnf1oxpnn  45102  icof  45126  fnmptif  45175  rn1st  45183  negpilt0  45195  xrgtso  45260  supxrleubrnmptf  45366  xrpnf  45401  rexanuz2nf  45408  ioontr  45429  iccdifioo  45433  iccdifprioo  45434  uzinico2  45480  fsummulc1f  45492  fsumiunss  45496  fnlimfvre2  45598  limsupreuz  45658  limsupvaluz2  45659  limsup10ex  45694  icccncfext  45808  dvcosre  45833  dvsinax  45834  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dvmptmulf  45858  dvnmul  45864  dvmptfprodlem  45865  dvnprodlem2  45868  stoweidlem1  45922  stoweidlem26  45947  stoweidlem34  45955  stoweidlem44  45965  stoweid  45984  stirlinglem5  45999  dirkercncflem1  46024  fourierdlem44  46072  fourierdlem56  46083  fourierdlem62  46089  fourierdlem89  46116  fourierdlem91  46118  fourierdlem100  46127  fourierdlem102  46129  fourierdlem103  46130  fourierdlem104  46131  fourierdlem108  46135  fourierdlem112  46139  fourierdlem114  46141  fouriersw  46152  rrndistlt  46211  gsumge0cl  46292  sge0tsms  46301  sge0ltfirpmpt2  46347  ovn0  46487  hoidmv1le  46515  hoidmvle  46521  ovnsubadd2lem  46566  ovolval4lem1  46570  vonioolem2  46602  smflimlem3  46694  nsssmfmbf  46700  axorbtnotaiffb  46818  axorbciffatcxorb  46820  abnotbtaxb  46830  euabsneu  46943  sprval  47353  fmtnoinf  47410  1nevenALTV  47565  nfermltl8rev  47616  nfermltl2rev  47617  nnsum3primes4  47662  tgblthelfgott  47689  tgoldbachlt  47690  usgrexmpl1lem  47836  usgrexmpl2lem  47841  usgrexmpl2trifr  47852  ldepslinc  48238  ackval42  48430  rrx2plordso  48458  vsn  48543  sepfsepc  48607  alimp-no-surprise  48875  aacllem  48895  amgmwlem  48896  amgmlemALT  48897