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  854  ori  861  pm5.16  1015  dn1  1057  3ori  1426  cadan  1609  nic-dfim  1669  nic-dfneg  1670  nic-mp  1671  nic-mpALT  1672  tbw-negdf  1699  rb-imdf  1750  nfri  1789  mpgbi  1798  19.35i  1878  nfim1  2200  19.36i  2232  ax6  2383  sbie  2501  datisi  2674  disamis  2675  dimatis  2682  fresison  2683  bamalip  2686  axi12  2700  eqcomi  2739  eqtri  2753  eleqtri  2827  nfnfc  2905  neii  2928  necomi  2980  neeqtri  2998  neli  3032  nrex  3058  rexlimivOLD  3164  rexlimi  3238  eueqi  3683  euxfr2w  3694  euxfr2  3696  reuxfrd  3722  cdeqri  3740  sseqtri  3998  pssn2lp  4070  equncomi  4126  unssi  4157  ssini  4206  unabs  4231  inabs  4232  dfin4  4244  vn0  4311  inindif  4341  difidALT  4343  ab0orv  4349  ab0orvALT  4350  disjdif  4438  difin0  4440  pwundif  4590  snid  4629  rabrsn  4691  iinrab2  5037  symdifv  5053  rintn0  5076  breqtri  5135  axsepgfromrep  5252  bm1.3iiOLD  5260  ax6vsep  5261  notzfaus  5321  zfpow  5324  dtruALT2  5328  dtruALT  5346  reusv2lem4  5359  dtru  5399  el  5400  dtruOLD  5404  op1stb  5434  copsexgw  5453  copsexg  5454  uniop  5478  rn0  5892  dmresi  6026  somincom  6110  cnvimassrndm  6128  cnvcnv  6168  elid  6175  rescnvcnv  6180  cnvcnvres  6181  cocnvcnv2  6234  cores2  6235  co01  6237  cnviin  6262  predres  6315  iota4an  6496  fnopab  6659  mpt0  6663  fnmpti  6664  f1cnvcnv  6768  f1ovi  6842  eliman0  6901  fvco4i  6965  cnvimainrn  7042  fmpti  7087  funiunfv  7225  oprabss  7500  relmptopab  7642  zfun  7715  tfinds2  7843  omon  7857  2nd0  7978  f1stres  7995  f2ndres  7996  cnvoprab  8042  relmpoopab  8076  df1st2  8080  df2nd2  8081  fsplit  8099  frpoins3xpg  8122  frpoins3xp3g  8123  poxp2  8125  poseq  8140  reldmtpos  8216  dftpos4  8227  tpostpos  8228  tpos0  8238  frrlem4  8271  smo0  8330  tfrlem14  8362  tfrlem16  8364  rdgsucg  8394  rdglimg  8396  frfnom  8406  oawordeulem  8521  uniixp  8897  dfdom2  8952  ssdomg  8974  xpcomf1o  9035  sbthlem5  9061  sdom0  9079  limensuci  9123  1sdom2  9194  fiint  9284  fiintOLD  9285  fidomdm  9292  residfi  9296  mptfi  9309  fisn  9385  dffi3  9389  ordtypelem6  9483  ordtypelem7  9484  wemaplem2  9507  harwdom  9551  suc11reg  9579  zfinf  9599  axinf2  9600  noinfep  9620  cantnfvalf  9625  cantnflt  9632  cantnf0  9635  cantnf  9653  ttrclco  9678  tz9.1c  9690  tc2  9702  r111  9735  r1tr2  9737  r1ordg  9738  r1sssuc  9743  r1val1  9746  tz9.13  9751  r1elssi  9765  pwwf  9767  rankopb  9812  rankeq0b  9820  ranksuc  9825  rankmapu  9838  rankxplim3  9841  rankxpsuc  9842  cp  9851  karden  9855  card0  9918  cardlim  9932  cardom  9946  infxpenlem  9973  alephsuc2  10040  alephgeom  10042  unialeph  10061  dfac4  10082  dfacacn  10102  dju1dif  10133  dju1p1e2  10134  infdju1  10150  ackbij1lem13  10191  ackbij2  10202  cf0  10211  cfsuc  10217  cfom  10224  cfslb2n  10228  ominf4  10272  fin23lem17  10298  fin23lem28  10300  fin23lem30  10302  fin23lem31  10303  fin23lem40  10311  isfin1-3  10346  dfacfin7  10359  fin1a2lem6  10365  itunitc1  10380  axcc3  10398  dcomex  10407  axdc2lem  10408  axcclem  10417  zfac  10420  ac3  10422  ackm  10425  axac2  10426  axac  10427  axaci  10428  cardeqv  10429  numth2  10431  numth  10432  dmct  10484  brdom3  10488  fin71ac  10493  cardf  10510  aleph1  10531  cfpwsdom  10544  smobeth  10546  zfcndrep  10574  zfcndpow  10576  zfcndac  10579  gch2  10635  wunex3  10701  tskpr  10730  inar1  10735  rankcf  10737  tskcard  10741  tskuni  10743  grothpw  10786  axgroth4  10792  grothprim  10794  inaprc  10796  dmaddpi  10850  dmmulpi  10851  1lt2pi  10865  addpqf  10904  mulpqf  10906  1lt2nq  10933  supsrlem  11071  ssxr  11250  gtso  11262  subf  11430  negne0i  11504  mulnzcnf  11831  infrenegsup  12173  neg1lt0  12181  nnne0  12227  halflt1  12406  nn0ssz  12559  3halfnz  12620  zeo  12627  numlt  12681  numltc  12682  le9lt10  12683  decle  12690  uzf  12803  xaddf  13191  xsubge0  13228  xmulf  13239  ixxf  13323  ixxssxr  13325  iooval2  13346  ioof  13415  unirnioo  13417  dfioo2  13418  fzval2  13478  fzf  13479  0nelfz1  13511  fz10  13513  fzpreddisj  13541  4fvwrd4  13616  fzof  13624  fzo0  13651  fldiv4p1lem1div2  13804  fldiv4lem1div2  13806  om2uzoi  13927  faclbnd4lem1  14265  hashkf  14304  hashgval  14305  hashinf  14307  hashresfn  14312  hashnn0n0nn  14363  hashge3el3dif  14459  hash3tpde  14465  rev0  14736  s2dm  14863  f1oun2prg  14890  trclublem  14968  sqrt2gt1lt2  15247  limsupgord  15445  fclim  15526  fsumrelem  15780  ackbijnn  15801  incexclem  15809  incexc  15810  arisum2  15834  georeclim  15845  geoisumr  15851  0.999...  15854  risefall0lem  15999  ege2le3  16063  sin0  16124  ef01bndlem  16159  cos2bnd  16163  cos01gt0  16166  sincos2sgn  16169  sin4lt0  16170  rpnnen2lem3  16191  rpnnen2lem9  16197  rexpen  16203  cnso  16222  dvdslelem  16286  divalglem1  16371  divalglem5  16374  divalglem6  16375  divalglem10  16379  flodddiv4  16392  0bits  16416  sadcf  16430  sadcadd  16435  bitsshft  16452  smupf  16455  gcdf  16489  eucalgf  16560  2prm  16669  dfphi2  16751  pockthi  16885  prmrec  16900  vdwapf  16950  vdwlem6  16964  karatsuba  17061  1259lem5  17112  2503lem3  17116  4001lem4  17121  structcnvcnv  17130  structfn  17133  strleun  17134  imasvscafn  17507  xpsff1o  17537  wunnat  17928  dfinito3  17974  dftermo3  17975  eldmcoa  18034  coapm  18040  catcfuccl  18087  catcxpccl  18175  yonedainv  18249  smndex1bas  18840  smndex1n0mnd  18846  grpinvfvi  18921  mulgfvi  19012  ressmulgnnd  19017  symgsssg  19404  symgfisg  19405  psgnunilem5  19431  sylow3lem2  19565  oppglsm  19579  efgmf  19650  efgval  19654  efgsf  19666  0frgp  19716  dmdprd  19937  dprdval  19942  invrfval  20305  drngui  20651  rmodislmod  20843  lssintcl  20877  cnfldadd  21277  cnfldmul  21279  cnfldfunALT  21286  dfcnfldOLD  21287  cnfldfunALTOLD  21299  cnfld0  21311  cnfld1  21312  cnfld1OLD  21313  cnfldsub  21316  xrsds  21333  pzriprnglem4  21401  pzriprnglem9  21406  pzriprnglem14  21411  psgnghm  21496  zrhpsgnmhm  21500  ocv1  21595  dsmmbas2  21653  mplsubrglem  21920  opsrtoslem2  21970  evl1maprhm  22273  mdetralt  22502  maducoeval2  22534  eltpsi  22838  unitg  22861  fctop  22898  cctop  22900  ppttop  22901  epttop  22903  leordtvallem1  23104  leordtvallem2  23105  iccordt  23108  iscnp2  23133  discmp  23292  conncompcld  23328  1stcrestlem  23346  2ndcdisj  23350  topnlly  23385  disllycmp  23392  dis1stc  23393  txuni2  23459  xkotf  23479  dfac14lem  23511  prdstps  23523  txindis  23528  tx1stc  23544  xkohaus  23547  xkoptsub  23548  cnmpt1st  23562  cnmpt2nd  23563  ptcmpfi  23707  trfil1  23780  fin1aufil  23826  tgpconncompeqg  24006  tgpconncomp  24007  trust  24124  met1stc  24416  dscmet  24467  retopon  24658  cnfldtopon  24677  xrsxmet  24705  xrsmopn  24708  iimulcn  24841  iimulcnOLD  24842  icopnfhmeo  24848  iccpnfhmeo  24850  xrhmeo  24851  cnheiborlem  24860  lebnumii  24872  ishtpy  24878  htpycc  24886  pco1  24922  pcohtpylem  24926  pcopt  24929  pcopt2  24930  pcoass  24931  pcorevlem  24933  rrxcph  25299  rrx0el  25305  ovoliunlem3  25412  ovolicc1  25424  ovolicc2  25430  volf  25437  ioorf  25481  dyadf  25499  dyadmbl  25508  vitalilem5  25520  vitali  25521  mbfimaopnlem  25563  mbflimsup  25574  0plef  25580  i1fima  25586  i1fima2  25587  i1fd  25589  itg1ge0  25594  itg10  25596  i1f1lem  25597  i1fadd  25603  i1fmul  25604  i1fmulc  25611  mbfi1fseqlem5  25627  itg2addlem  25666  reldv  25778  dvbsss  25810  dvef  25891  lhop1lem  25925  deg1fvi  25997  plypf1  26124  coeeulem  26136  coeeu  26137  vieta1lem2  26226  aannenlem3  26245  aalioulem3  26249  dvradcnv  26337  pserulm  26338  pserdvlem2  26345  sinhalfpilem  26379  sincos4thpi  26429  tan4thpiOLD  26431  sincos6thpi  26432  pige3ALT  26436  resinf1o  26452  tanord1  26453  tanregt0  26455  efabl  26466  relogrn  26477  dfrelog  26481  logi  26503  logneg  26504  logltb  26516  logcn  26563  logf1o2  26566  dvlog  26567  efopnlem2  26573  efopn  26574  logccv  26579  dvsqrt  26658  dvcnsqrt  26660  cxpcn3  26665  logblog  26709  angpined  26747  1cubr  26759  asinsin  26809  asin1  26811  reasinsin  26813  atan0  26825  atanbnd  26843  atan1  26845  log2cnv  26861  log2ub  26866  log2le1  26867  birthday  26871  amgmlem  26907  emcllem5  26917  emgt0  26924  harmonicbnd3  26925  ftalem3  26992  basellem4  27001  sgmf  27062  ppi1  27081  cht1  27082  vma1  27083  ppiltx  27094  sqff1o  27099  ppiublem1  27120  ppiublem2  27121  ppiub  27122  chtub  27130  dchreq  27176  bposlem7  27208  bposlem8  27209  bposlem9  27210  lgsdir2lem2  27244  lgsdir2lem3  27245  chebbnd1  27390  chto1ub  27394  chpo1ubb  27399  pntibndlem1  27507  nosgnn0  27577  sltsolem1  27594  bdayfo  27596  nolt02o  27614  nogt01o  27615  noetasuplem4  27655  noetainflem4  27659  scutbdaybnd2lim  27736  madeun  27802  scutfo  27823  addsproplem2  27884  addsproplem7  27889  addsprop  27890  negsprop  27948  subsf  27975  mulsproplem13  28038  mulsproplem14  28039  mulsprop  28040  onsiso  28176  n0scut  28233  bdayn0sf1o  28266  twocut  28316  0reno  28355  tgldimor  28436  tglnfn  28481  axlowdimlem4  28879  axlowdimlem16  28891  axlowdim  28895  upgrfi  29025  lfgrnloop  29059  lfuhgr1v0e  29188  usgrexmplef  29193  usgrres  29242  vdegp1bi  29472  vtxdginducedm1lem2  29475  dfpth2  29666  pthdlem2  29705  wpthswwlks2on  29898  0ewlk  30050  0pth  30061  konigsbergiedgw  30184  konigsberglem1  30188  konigsberglem2  30189  konigsberglem3  30190  konigsberglem4  30191  konigsberglem5  30192  ex-dif  30359  ex-un  30360  ex-in  30361  ex-fl  30383  avril1  30399  9p10ne21fool  30407  n0lplig  30419  cnidOLD  30518  cnnvm  30618  ipasslem8  30773  ipasslem10  30775  hvsubf  30951  normlem1  31046  normlem6  31051  normlem7  31052  norm-ii-i  31073  norm3adifii  31084  hilid  31097  hlimf  31173  hhssabloi  31198  hhssnv  31200  hhshsslem1  31203  shincli  31298  shsval2i  31323  shs0i  31385  chj0i  31391  chm1i  31392  chincli  31396  chdmm1i  31413  shjshsi  31428  chsup0  31484  h1de2bi  31490  spansnpji  31514  cmcmlem  31527  cmcmii  31533  cmcm2ii  31534  cmcm3ii  31535  pjidmi  31609  pjssmii  31617  pj0i  31629  pjocini  31634  mayetes3i  31665  df0op2  31688  hoaddcomi  31708  hoaddassi  31712  hocadddiri  31715  hocsubdiri  31716  hoaddridi  31722  ho0coi  31724  hoid1i  31725  hoid1ri  31726  hodseqi  31730  honegsubi  31732  adj1o  31830  hoddii  31925  lnopunilem1  31946  lnopunilem2  31947  nmcopexi  31963  nmcopex  31965  nmcoplb  31966  nmcfnexi  31987  nmcfnex  31989  nmcfnlb  31990  adjbd1o  32021  adjcoi  32036  nmopcoadji  32037  opsqrlem6  32081  pjsdii  32091  pjddii  32092  pjidmcoi  32113  pjtoi  32115  pjin1i  32128  pjclem1  32131  stji1i  32178  reuxfrdf  32427  iuninc  32496  fnresin  32557  rinvf1o  32561  suppss2f  32569  xppreima  32576  ofoprabco  32595  fressupp  32618  supppreima  32621  fsupprnfi  32622  gtiso  32631  df1stres  32634  df2ndres  32635  snct  32644  padct  32650  fsuppcurry1  32655  fsuppcurry2  32656  ffsrn  32659  fpwrelmapffs  32664  fzodif1  32722  nnindf  32751  nn0min  32752  dp2lt  32812  dp2ltsuc  32813  dp2ltc  32814  dplti  32832  dpmul  32840  dpmul4  32841  ressplusf  32892  chnub  32945  xrsclat  32956  xrge0base  32959  xrge00  32960  xrnarchi  33145  elrgspnlem2  33201  1fldgenq  33279  xrge0slmod  33326  zringfrac  33532  ply1degltdimlem  33625  ccfldsrarelvec  33673  ccfldextdgrr  33674  locfinreflem  33837  locfinref  33838  unicls  33900  sqsscirc1  33905  mhmhmeotmd  33924  raddcn  33926  xrge0iifiso  33932  xrge0iifhmeo  33933  lmxrge0  33949  cnzh  33965  rezh  33966  qqh0  33981  qqh1  33982  qqhre  34017  rrhre  34018  esumnul  34045  esum0  34046  esumsnf  34061  esumpfinvallem  34071  esumpfinvalf  34073  esumpcvgval  34075  esumcvgsum  34085  esumsup  34086  esumcvgre  34088  sigaclfu2  34118  dmsigagen  34141  ddemeas  34233  mbfmvolf  34264  br2base  34267  omssubadd  34298  sibfof  34338  sitg0  34344  eulerpartlemt  34369  eulerpartgbij  34370  0rrv  34449  coinfliplem  34477  coinflipprob  34478  coinfliprv  34481  ballotlem2  34487  ballotlem4  34497  ballotlem5  34498  ballotlemi1  34501  ballotlem7  34534  ballotth  34536  signsplypnf  34548  signsply0  34549  signsw0g  34554  signswch  34559  signsvf0  34578  hashreprin  34618  reprfz1  34622  chtvalz  34627  hgt750lemd  34646  hgt750lem  34649  hgt750lem2  34650  bnj1098  34780  bnj1109  34783  bnj1131  34784  bnj1533  34849  bnj151  34874  bnj580  34910  bnj852  34918  bnj864  34919  bnj865  34920  bnj978  34946  bnj1021  34963  bnj907  34964  bnj1093  34977  bnj1145  34990  bnj1172  34998  bnj1174  35000  bnj1176  35002  bnj1186  35004  nfan1c  35070  fineqvac  35094  onvf1odlem4  35100  onvf1od  35101  subfacf  35169  subfacp1lem1  35173  subfacp1lem5  35178  subfacp1lem6  35179  subfacval3  35183  erdszelem2  35186  kur14lem4  35203  ioosconn  35241  iccllysconn  35244  satfn  35349  fmlaomn0  35384  gonan0  35386  goaln0  35387  elnanelprv  35423  msrfo  35540  mthmpps  35576  problem5  35663  quad3  35664  circum  35668  antnestALT  35688  axextprim  35695  axrepprim  35696  axunprim  35697  axinfprim  35700  axacprim  35701  bcneg1  35730  setinds  35773  dfon2lem2  35779  dfon2lem4  35781  axextdfeq  35792  fobigcup  35895  snelsingles  35917  fullfunfnv  35941  fullfunfv  35942  rankaltopb  35974  rank0  36165  rankeq1o  36166  hfuni  36179  in-ax8  36219  fneer  36348  neibastop1  36354  nabi1i  36389  nabi2i  36390  limsucncmpi  36440  knoppcnlem8  36495  knoppcnlem11  36498  cnndvlem1  36532  bj-consensusALT  36574  bj-sbidmOLD  36845  bj-n0i  36946  bj-snsetex  36958  bj-tagss  36975  bj-2upln0  37018  bj-2upln1upl  37019  bj-nuliota  37052  bj-0int  37096  bj-elid5  37164  bj-inftyexpitaufo  37197  bj-pinftyccb  37216  bj-minftyccb  37220  bj-pinftynminfty  37222  bj-isrvec  37289  iccioo01  37322  f1omptsnlem  37331  mptsnunlem  37333  topdifinffinlem  37342  relowlpssretop  37359  1oequni2o  37363  pibt2  37412  imadifss  37596  tan2h  37613  poimirlem3  37624  poimirlem9  37630  poimirlem16  37637  poimirlem17  37638  poimirlem18  37639  poimirlem19  37640  poimirlem20  37641  poimirlem22  37643  poimirlem30  37651  mblfinlem1  37658  mblfinlem2  37659  ovoliunnfl  37663  voliunnfl  37665  itg2addnclem  37672  itg2addnclem2  37673  asindmre  37704  areacirclem1  37709  fdc  37746  cntotbnd  37797  heiborlem6  37817  rrnval  37828  reheibor  37840  rngosn3  37925  brcnvrabga  38331  cnvresrn  38337  moantr  38353  inxp2  38356  dfxrn2  38365  cnvcosseq  38435  refrelcosslem  38460  1cosscnvxrn  38473  redundss3  38626  refrelsredund3  38632  refrelredund3  38635  eqvrel0  38785  eqvrelid  38788  prter2  38881  renegclALT  38963  mapdunirnN  41651  lcmeprodgcdi  42002  3factsumint2  42017  3factsumint3  42018  3factsumint4  42019  3factsumint  42020  lcmineqlem4  42027  3lexlogpow5ineq1  42049  3lexlogpow2ineq1  42053  dvrelogpow2b  42063  aks4d1p1p4  42066  aks4d1p8  42082  aks6d1c1  42111  aks6d1c2p2  42114  aks6d1c4  42119  2ap1caineq  42140  sticksstones1  42141  sticksstones2  42142  aks6d1c7lem2  42176  aks5lem3a  42184  aks5lem6  42187  unitscyglem2  42191  unitscyglem3  42192  sqdeccom12  42284  readvrec2  42356  readvcot  42359  resubf  42376  sn-0ne2  42401  sn-subf  42424  sn-nnne0  42455  sn-0lt1  42470  reneg1lt0  42475  rntrclfvOAI  42686  diophrw  42754  rabren3dioph  42810  pellexlem6  42829  pellex  42830  frmx  42909  frmy  42910  jm2.23  42992  jm2.27dlem3  43007  axac10  43029  pw2f1ocnv  43033  kelac2lem  43060  lmhmlnmsplit  43083  pwfi2f1o  43092  frlmpwfi  43094  insucid  43399  nla0003  43421  ifpbiidcor  43470  sucomisnotcard  43540  alephiso2  43554  alephiso3  43555  cnvnonrel  43584  rnnonrel  43587  resnonrel  43588  cononrel1  43590  cononrel2  43591  fvnonrel  43593  cnvcnvintabd  43596  cnvintabd  43599  rclexi  43611  rtrclex  43613  clcnvlem  43619  cnvrcl0  43621  dmtrcl  43623  rntrcl  43624  dfrtrcl5  43625  iunrelexp0  43698  dmtrclfvRP  43726  rntrclfv  43728  corcltrcl  43735  cotrclrcl  43738  0heALT  43779  frege54cor1a  43860  uneqsn  44021  clsk3nimkb  44036  int-sqdefd  44177  int-sqgeq0d  44182  rr-groth  44295  rr-grothprim  44296  rr-grothshort  44300  seff  44305  expgrowthi  44329  expgrowth  44331  binomcxplemnotnn0  44352  ee233  44516  ax6e2nd  44555  in1  44568  dfvd2ani  44580  dfvd2i  44582  dfvd3i  44589  dfvd3ani  44592  e0bi  44772  uun2221  44809  uun2221p1  44810  uun2221p2  44811  en3lpVD  44841  relopabVD  44897  ax6e2ndVD  44904  ax6e2ndALT  44926  permaxpow  45006  pssnssi  45102  nnf1oxpnn  45196  icof  45220  fnmptif  45266  rn1st  45274  negpilt0  45286  xrgtso  45348  supxrleubrnmptf  45454  xrpnf  45488  rexanuz2nf  45495  ioontr  45516  iccdifioo  45520  iccdifprioo  45521  uzinico2  45566  fsummulc1f  45576  fsumiunss  45580  fnlimfvre2  45682  limsupreuz  45742  limsup10ex  45778  icccncfext  45892  dvcosre  45917  dvsinax  45918  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  dvmptmulf  45942  dvnmul  45948  dvmptfprodlem  45949  dvnprodlem2  45952  stoweidlem1  46006  stoweidlem26  46031  stoweidlem34  46039  stoweidlem44  46049  stoweid  46068  stirlinglem5  46083  dirkercncflem1  46108  fourierdlem44  46156  fourierdlem56  46167  fourierdlem62  46173  fourierdlem89  46200  fourierdlem91  46202  fourierdlem100  46211  fourierdlem102  46213  fourierdlem103  46214  fourierdlem104  46215  fourierdlem108  46219  fourierdlem112  46223  fourierdlem114  46225  fouriersw  46236  rrndistlt  46295  gsumge0cl  46376  sge0tsms  46385  sge0ltfirpmpt2  46431  ovn0  46571  hoidmv1le  46599  hoidmvle  46605  ovnsubadd2lem  46650  ovolval4lem1  46654  vonioolem2  46686  smflimlem3  46778  nsssmfmbf  46784  axorbtnotaiffb  46908  axorbciffatcxorb  46910  abnotbtaxb  46920  euabsneu  47033  ceilhalf1  47339  sprval  47484  fmtnoinf  47541  1nevenALTV  47696  nfermltl8rev  47747  nfermltl2rev  47748  nnsum3primes4  47793  tgblthelfgott  47820  tgoldbachlt  47821  cycl3grtri  47950  isubgr3stgrlem3  47971  usgrexmpl1lem  48016  usgrexmpl2lem  48021  usgrexmpl2trifr  48032  gpgprismgr4cycllem7  48095  ldepslinc  48502  ackval42  48689  rrx2plordso  48717  vsn  48804  dmtposss  48868  sepfsepc  48920  basresposfo  48970  rescofuf  49086  oppff1  49141  idfth  49151  idsubc  49153  fuco2eld2  49307  fuco22a  49343  setc1onsubc  49595  alimp-no-surprise  49774  aacllem  49794  amgmwlem  49795  amgmlemALT  49796