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  1610  nic-dfim  1670  nic-dfneg  1671  nic-mp  1672  nic-mpALT  1673  tbw-negdf  1700  rb-imdf  1751  nfri  1790  mpgbi  1799  19.35i  1879  nfim1  2202  19.36i  2234  ax6  2384  sbie  2502  datisi  2675  disamis  2676  dimatis  2683  fresison  2684  bamalip  2687  axi12  2701  eqcomi  2740  eqtri  2754  eleqtri  2829  nfnfc  2907  neii  2930  necomi  2982  neeqtri  3000  neli  3034  nrex  3060  rexlimi  3232  eueqi  3668  euxfr2w  3679  euxfr2  3681  reuxfrd  3707  cdeqri  3725  sseqtri  3983  pssn2lp  4054  equncomi  4110  unssi  4141  ssini  4190  unabs  4215  inabs  4216  dfin4  4228  vn0  4295  inindif  4325  difidALT  4327  ab0orv  4333  ab0orvALT  4334  disjdif  4422  difin0  4424  pwundif  4574  snid  4615  rabrsn  4677  iinrab2  5018  symdifv  5034  rintn0  5057  breqtri  5116  axsepgfromrep  5232  bm1.3iiOLD  5240  ax6vsep  5241  notzfaus  5301  zfpow  5304  dtruALT2  5308  dtruALT  5326  reusv2lem4  5339  dtru  5379  el  5380  op1stb  5411  copsexgw  5430  copsexg  5431  uniop  5455  rn0  5866  dmresi  6001  somincom  6081  cnvimassrndm  6099  cnvcnv  6139  elid  6146  rescnvcnv  6151  cnvcnvres  6152  cocnvcnv2  6206  cores2  6207  co01  6209  cnviin  6233  predres  6286  iota4an  6463  fnopab  6619  mpt0  6623  fnmpti  6624  f1cnvcnv  6728  f1ovi  6802  eliman0  6859  fvco4i  6923  cnvimainrn  7000  fmpti  7045  funiunfv  7182  oprabss  7454  relmptopab  7596  zfun  7669  tfinds2  7794  omon  7808  2nd0  7928  f1stres  7945  f2ndres  7946  cnvoprab  7992  relmpoopab  8024  df1st2  8028  df2nd2  8029  fsplit  8047  frpoins3xpg  8070  frpoins3xp3g  8071  poxp2  8073  poseq  8088  reldmtpos  8164  dftpos4  8175  tpostpos  8176  tpos0  8186  frrlem4  8219  smo0  8278  tfrlem14  8310  tfrlem16  8312  rdgsucg  8342  rdglimg  8344  frfnom  8354  oawordeulem  8469  uniixp  8845  dfdom2  8900  ssdomg  8922  xpcomf1o  8979  sbthlem5  9004  sdom0  9022  limensuci  9066  1sdom2  9132  fiint  9211  fidomdm  9218  residfi  9222  mptfi  9235  fisn  9311  dffi3  9315  ordtypelem6  9409  ordtypelem7  9410  wemaplem2  9433  harwdom  9477  nelaneq  9487  suc11reg  9509  zfinf  9529  axinf2  9530  noinfep  9550  cantnfvalf  9555  cantnflt  9562  cantnf0  9565  cantnf  9583  ttrclco  9608  tz9.1c  9620  tc2  9632  r111  9665  r1tr2  9667  r1ordg  9668  r1sssuc  9673  r1val1  9676  tz9.13  9681  r1elssi  9695  pwwf  9697  rankopb  9742  rankeq0b  9750  ranksuc  9755  rankmapu  9768  rankxplim3  9771  rankxpsuc  9772  cp  9781  karden  9785  card0  9848  cardlim  9862  cardom  9876  infxpenlem  9901  alephsuc2  9968  alephgeom  9970  unialeph  9989  dfac4  10010  dfacacn  10030  dju1dif  10061  dju1p1e2  10062  infdju1  10078  ackbij1lem13  10119  ackbij2  10130  cf0  10139  cfsuc  10145  cfom  10152  cfslb2n  10156  ominf4  10200  fin23lem17  10226  fin23lem28  10228  fin23lem30  10230  fin23lem31  10231  fin23lem40  10239  isfin1-3  10274  dfacfin7  10287  fin1a2lem6  10293  itunitc1  10308  axcc3  10326  dcomex  10335  axdc2lem  10336  axcclem  10345  zfac  10348  ac3  10350  ackm  10353  axac2  10354  axac  10355  axaci  10356  cardeqv  10357  numth2  10359  numth  10360  dmct  10412  brdom3  10416  fin71ac  10421  cardf  10438  aleph1  10459  cfpwsdom  10472  smobeth  10474  zfcndrep  10502  zfcndpow  10504  zfcndac  10507  gch2  10563  wunex3  10629  tskpr  10658  inar1  10663  rankcf  10665  tskcard  10669  tskuni  10671  grothpw  10714  axgroth4  10720  grothprim  10722  inaprc  10724  dmaddpi  10778  dmmulpi  10779  1lt2pi  10793  addpqf  10832  mulpqf  10834  1lt2nq  10861  supsrlem  10999  ssxr  11179  gtso  11191  subf  11359  negne0i  11433  mulnzcnf  11760  infrenegsup  12102  neg1lt0  12110  nnne0  12156  halflt1  12335  nn0ssz  12488  3halfnz  12549  zeo  12556  numlt  12610  numltc  12611  le9lt10  12612  decle  12619  uzf  12732  xaddf  13120  xsubge0  13157  xmulf  13168  ixxf  13252  ixxssxr  13254  iooval2  13275  ioof  13344  unirnioo  13346  dfioo2  13347  fzval2  13407  fzf  13408  0nelfz1  13440  fz10  13442  fzpreddisj  13470  4fvwrd4  13545  fzof  13553  fzo0  13580  fldiv4p1lem1div2  13736  fldiv4lem1div2  13738  om2uzoi  13859  faclbnd4lem1  14197  hashkf  14236  hashgval  14237  hashinf  14239  hashresfn  14244  hashnn0n0nn  14295  hashge3el3dif  14391  hash3tpde  14397  rev0  14668  s2dm  14794  f1oun2prg  14821  trclublem  14899  sqrt2gt1lt2  15178  limsupgord  15376  fclim  15457  fsumrelem  15711  ackbijnn  15732  incexclem  15740  incexc  15741  arisum2  15765  georeclim  15776  geoisumr  15782  0.999...  15785  risefall0lem  15930  ege2le3  15994  sin0  16055  ef01bndlem  16090  cos2bnd  16094  cos01gt0  16097  sincos2sgn  16100  sin4lt0  16101  rpnnen2lem3  16122  rpnnen2lem9  16128  rexpen  16134  cnso  16153  dvdslelem  16217  divalglem1  16302  divalglem5  16305  divalglem6  16306  divalglem10  16310  flodddiv4  16323  0bits  16347  sadcf  16361  sadcadd  16366  bitsshft  16383  smupf  16386  gcdf  16420  eucalgf  16491  2prm  16600  dfphi2  16682  pockthi  16816  prmrec  16831  vdwapf  16881  vdwlem6  16895  karatsuba  16992  1259lem5  17043  2503lem3  17047  4001lem4  17052  structcnvcnv  17061  structfn  17064  strleun  17065  imasvscafn  17438  xpsff1o  17468  xrge0base  17508  wunnat  17863  dfinito3  17909  dftermo3  17910  eldmcoa  17969  coapm  17975  catcfuccl  18022  catcxpccl  18110  yonedainv  18184  chnub  18525  smndex1bas  18811  smndex1n0mnd  18817  grpinvfvi  18892  mulgfvi  18983  ressmulgnnd  18988  symgsssg  19377  symgfisg  19378  psgnunilem5  19404  sylow3lem2  19538  oppglsm  19552  efgmf  19623  efgval  19627  efgsf  19639  0frgp  19689  dmdprd  19910  dprdval  19915  invrfval  20305  drngui  20648  rmodislmod  20861  lssintcl  20895  cnfldadd  21295  cnfldmul  21297  cnfldfunALT  21304  dfcnfldOLD  21305  cnfldfunALTOLD  21317  cnfld0  21327  cnfld1  21328  cnfld1OLD  21329  cnfldsub  21332  xrsds  21344  pzriprnglem4  21419  pzriprnglem9  21424  pzriprnglem14  21429  psgnghm  21515  zrhpsgnmhm  21519  ocv1  21614  dsmmbas2  21672  mplsubrglem  21939  opsrtoslem2  21989  evl1maprhm  22292  mdetralt  22521  maducoeval2  22553  eltpsi  22857  unitg  22880  fctop  22917  cctop  22919  ppttop  22920  epttop  22922  leordtvallem1  23123  leordtvallem2  23124  iccordt  23127  iscnp2  23152  discmp  23311  conncompcld  23347  1stcrestlem  23365  2ndcdisj  23369  topnlly  23404  disllycmp  23411  dis1stc  23412  txuni2  23478  xkotf  23498  dfac14lem  23530  prdstps  23542  txindis  23547  tx1stc  23563  xkohaus  23566  xkoptsub  23567  cnmpt1st  23581  cnmpt2nd  23582  ptcmpfi  23726  trfil1  23799  fin1aufil  23845  tgpconncompeqg  24025  tgpconncomp  24026  trust  24142  met1stc  24434  dscmet  24485  retopon  24676  cnfldtopon  24695  xrsxmet  24723  xrsmopn  24726  iimulcn  24859  iimulcnOLD  24860  icopnfhmeo  24866  iccpnfhmeo  24868  xrhmeo  24869  cnheiborlem  24878  lebnumii  24890  ishtpy  24896  htpycc  24904  pco1  24940  pcohtpylem  24944  pcopt  24947  pcopt2  24948  pcoass  24949  pcorevlem  24951  rrxcph  25317  rrx0el  25323  ovoliunlem3  25430  ovolicc1  25442  ovolicc2  25448  volf  25455  ioorf  25499  dyadf  25517  dyadmbl  25526  vitalilem5  25538  vitali  25539  mbfimaopnlem  25581  mbflimsup  25592  0plef  25598  i1fima  25604  i1fima2  25605  i1fd  25607  itg1ge0  25612  itg10  25614  i1f1lem  25615  i1fadd  25621  i1fmul  25622  i1fmulc  25629  mbfi1fseqlem5  25645  itg2addlem  25684  reldv  25796  dvbsss  25828  dvef  25909  lhop1lem  25943  deg1fvi  26015  plypf1  26142  coeeulem  26154  coeeu  26155  vieta1lem2  26244  aannenlem3  26263  aalioulem3  26267  dvradcnv  26355  pserulm  26356  pserdvlem2  26363  sinhalfpilem  26397  sincos4thpi  26447  tan4thpiOLD  26449  sincos6thpi  26450  pige3ALT  26454  resinf1o  26470  tanord1  26471  tanregt0  26473  efabl  26484  relogrn  26495  dfrelog  26499  logi  26521  logneg  26522  logltb  26534  logcn  26581  logf1o2  26584  dvlog  26585  efopnlem2  26591  efopn  26592  logccv  26597  dvsqrt  26676  dvcnsqrt  26678  cxpcn3  26683  logblog  26727  angpined  26765  1cubr  26777  asinsin  26827  asin1  26829  reasinsin  26831  atan0  26843  atanbnd  26861  atan1  26863  log2cnv  26879  log2ub  26884  log2le1  26885  birthday  26889  amgmlem  26925  emcllem5  26935  emgt0  26942  harmonicbnd3  26943  ftalem3  27010  basellem4  27019  sgmf  27080  ppi1  27099  cht1  27100  vma1  27101  ppiltx  27112  sqff1o  27117  ppiublem1  27138  ppiublem2  27139  ppiub  27140  chtub  27148  dchreq  27194  bposlem7  27226  bposlem8  27227  bposlem9  27228  lgsdir2lem2  27262  lgsdir2lem3  27263  chebbnd1  27408  chto1ub  27412  chpo1ubb  27417  pntibndlem1  27525  nosgnn0  27595  sltsolem1  27612  bdayfo  27614  nolt02o  27632  nogt01o  27633  noetasuplem4  27673  noetainflem4  27677  scutbdaybnd2lim  27756  madeun  27827  scutfo  27848  addsproplem2  27911  addsproplem7  27916  addsprop  27917  negsprop  27975  subsf  28002  mulsproplem13  28065  mulsproplem14  28066  mulsprop  28067  onsiso  28203  n0scut  28260  bdayn0sf1o  28293  twocut  28344  0reno  28397  tgldimor  28478  tglnfn  28523  axlowdimlem4  28921  axlowdimlem16  28933  axlowdim  28937  upgrfi  29067  lfgrnloop  29101  lfuhgr1v0e  29230  usgrexmplef  29235  usgrres  29284  vdegp1bi  29514  vtxdginducedm1lem2  29517  dfpth2  29705  pthdlem2  29744  wpthswwlks2on  29937  0ewlk  30089  0pth  30100  konigsbergiedgw  30223  konigsberglem1  30227  konigsberglem2  30228  konigsberglem3  30229  konigsberglem4  30230  konigsberglem5  30231  ex-dif  30398  ex-un  30399  ex-in  30400  ex-fl  30422  avril1  30438  9p10ne21fool  30446  n0lplig  30458  cnidOLD  30557  cnnvm  30657  ipasslem8  30812  ipasslem10  30814  hvsubf  30990  normlem1  31085  normlem6  31090  normlem7  31091  norm-ii-i  31112  norm3adifii  31123  hilid  31136  hlimf  31212  hhssabloi  31237  hhssnv  31239  hhshsslem1  31242  shincli  31337  shsval2i  31362  shs0i  31424  chj0i  31430  chm1i  31431  chincli  31435  chdmm1i  31452  shjshsi  31467  chsup0  31523  h1de2bi  31529  spansnpji  31553  cmcmlem  31566  cmcmii  31572  cmcm2ii  31573  cmcm3ii  31574  pjidmi  31648  pjssmii  31656  pj0i  31668  pjocini  31673  mayetes3i  31704  df0op2  31727  hoaddcomi  31747  hoaddassi  31751  hocadddiri  31754  hocsubdiri  31755  hoaddridi  31761  ho0coi  31763  hoid1i  31764  hoid1ri  31765  hodseqi  31769  honegsubi  31771  adj1o  31869  hoddii  31964  lnopunilem1  31985  lnopunilem2  31986  nmcopexi  32002  nmcopex  32004  nmcoplb  32005  nmcfnexi  32026  nmcfnex  32028  nmcfnlb  32029  adjbd1o  32060  adjcoi  32075  nmopcoadji  32076  opsqrlem6  32120  pjsdii  32130  pjddii  32131  pjidmcoi  32152  pjtoi  32154  pjin1i  32167  pjclem1  32170  stji1i  32217  reuxfrdf  32465  iuninc  32535  fnresin  32602  rinvf1o  32607  suppss2f  32615  xppreima  32622  ofoprabco  32641  fressupp  32664  supppreima  32667  fsupprnfi  32668  gtiso  32677  df1stres  32680  df2ndres  32681  snct  32690  padct  32696  fsuppcurry1  32702  fsuppcurry2  32703  ffsrn  32706  fpwrelmapffs  32712  fzodif1  32770  nnindf  32797  nn0min  32798  dp2lt  32860  dp2ltsuc  32861  dp2ltc  32862  dplti  32880  dpmul  32888  dpmul4  32889  ressplusf  32939  xrsclat  32987  xrge00  32990  xrnarchi  33148  elrgspnlem2  33205  1fldgenq  33283  xrge0slmod  33308  zringfrac  33514  ply1degltdimlem  33630  ccfldsrarelvec  33679  ccfldextdgrr  33680  locfinreflem  33848  locfinref  33849  unicls  33911  sqsscirc1  33916  mhmhmeotmd  33935  raddcn  33937  xrge0iifiso  33943  xrge0iifhmeo  33944  lmxrge0  33960  cnzh  33976  rezh  33977  qqh0  33992  qqh1  33993  qqhre  34028  rrhre  34029  esumnul  34056  esum0  34057  esumsnf  34072  esumpfinvallem  34082  esumpfinvalf  34084  esumpcvgval  34086  esumcvgsum  34096  esumsup  34097  esumcvgre  34099  sigaclfu2  34129  dmsigagen  34152  ddemeas  34244  mbfmvolf  34274  br2base  34277  omssubadd  34308  sibfof  34348  sitg0  34354  eulerpartlemt  34379  eulerpartgbij  34380  0rrv  34459  coinfliplem  34487  coinflipprob  34488  coinfliprv  34491  ballotlem2  34497  ballotlem4  34507  ballotlem5  34508  ballotlemi1  34511  ballotlem7  34544  ballotth  34546  signsplypnf  34558  signsply0  34559  signsw0g  34564  signswch  34569  signsvf0  34588  hashreprin  34628  reprfz1  34632  chtvalz  34637  hgt750lemd  34656  hgt750lem  34659  hgt750lem2  34660  bnj1098  34790  bnj1109  34793  bnj1131  34794  bnj1533  34859  bnj151  34884  bnj580  34920  bnj852  34928  bnj864  34929  bnj865  34930  bnj978  34956  bnj1021  34973  bnj907  34974  bnj1093  34987  bnj1145  35000  bnj1172  35008  bnj1174  35010  bnj1176  35012  bnj1186  35014  nfan1c  35080  tz9.1regs  35118  fineqvac  35127  onvf1odlem4  35138  onvf1od  35139  subfacf  35207  subfacp1lem1  35211  subfacp1lem5  35216  subfacp1lem6  35217  subfacval3  35221  erdszelem2  35224  kur14lem4  35241  ioosconn  35279  iccllysconn  35282  satfn  35387  fmlaomn0  35422  gonan0  35424  goaln0  35425  elnanelprv  35461  msrfo  35578  mthmpps  35614  problem5  35701  quad3  35702  circum  35706  antnestALT  35726  axextprim  35733  axrepprim  35734  axunprim  35735  axinfprim  35738  axacprim  35739  bcneg1  35768  setinds  35811  dfon2lem2  35817  dfon2lem4  35819  axextdfeq  35830  fobigcup  35933  snelsingles  35955  fullfunfnv  35979  fullfunfv  35980  rankaltopb  36012  rank0  36203  rankeq1o  36204  hfuni  36217  in-ax8  36257  fneer  36386  neibastop1  36392  nabi1i  36427  nabi2i  36428  limsucncmpi  36478  knoppcnlem8  36533  knoppcnlem11  36536  cnndvlem1  36570  bj-consensusALT  36612  bj-sbidmOLD  36883  bj-n0i  36984  bj-snsetex  36996  bj-tagss  37013  bj-2upln0  37056  bj-2upln1upl  37057  bj-nuliota  37090  bj-0int  37134  bj-elid5  37202  bj-inftyexpitaufo  37235  bj-pinftyccb  37254  bj-minftyccb  37258  bj-pinftynminfty  37260  bj-isrvec  37327  iccioo01  37360  f1omptsnlem  37369  mptsnunlem  37371  topdifinffinlem  37380  relowlpssretop  37397  1oequni2o  37401  pibt2  37450  imadifss  37634  tan2h  37651  poimirlem3  37662  poimirlem9  37668  poimirlem16  37675  poimirlem17  37676  poimirlem18  37677  poimirlem19  37678  poimirlem20  37679  poimirlem22  37681  poimirlem30  37689  mblfinlem1  37696  mblfinlem2  37697  ovoliunnfl  37701  voliunnfl  37703  itg2addnclem  37710  itg2addnclem2  37711  asindmre  37742  areacirclem1  37747  fdc  37784  cntotbnd  37835  heiborlem6  37855  rrnval  37866  reheibor  37878  rngosn3  37963  brcnvrabga  38369  cnvresrn  38375  moantr  38391  inxp2  38394  dfxrn2  38403  cnvcosseq  38473  refrelcosslem  38498  1cosscnvxrn  38511  redundss3  38664  refrelsredund3  38670  refrelredund3  38673  eqvrel0  38823  eqvrelid  38826  prter2  38919  renegclALT  39001  mapdunirnN  41688  lcmeprodgcdi  42039  3factsumint2  42054  3factsumint3  42055  3factsumint4  42056  3factsumint  42057  lcmineqlem4  42064  3lexlogpow5ineq1  42086  3lexlogpow2ineq1  42090  dvrelogpow2b  42100  aks4d1p1p4  42103  aks4d1p8  42119  aks6d1c1  42148  aks6d1c2p2  42151  aks6d1c4  42156  2ap1caineq  42177  sticksstones1  42178  sticksstones2  42179  aks6d1c7lem2  42213  aks5lem3a  42221  aks5lem6  42224  unitscyglem2  42228  unitscyglem3  42229  sqdeccom12  42321  readvrec2  42393  readvcot  42396  resubf  42413  sn-0ne2  42438  sn-subf  42461  sn-nnne0  42492  sn-0lt1  42507  reneg1lt0  42512  rntrclfvOAI  42723  diophrw  42791  rabren3dioph  42847  pellexlem6  42866  pellex  42867  frmx  42945  frmy  42946  jm2.23  43028  jm2.27dlem3  43043  axac10  43065  pw2f1ocnv  43069  kelac2lem  43096  lmhmlnmsplit  43119  pwfi2f1o  43128  frlmpwfi  43130  insucid  43435  nla0003  43457  ifpbiidcor  43506  sucomisnotcard  43576  alephiso2  43590  alephiso3  43591  cnvnonrel  43620  rnnonrel  43623  resnonrel  43624  cononrel1  43626  cononrel2  43627  fvnonrel  43629  cnvcnvintabd  43632  cnvintabd  43635  rclexi  43647  rtrclex  43649  clcnvlem  43655  cnvrcl0  43657  dmtrcl  43659  rntrcl  43660  dfrtrcl5  43661  iunrelexp0  43734  dmtrclfvRP  43762  rntrclfv  43764  corcltrcl  43771  cotrclrcl  43774  0heALT  43815  frege54cor1a  43896  uneqsn  44057  clsk3nimkb  44072  int-sqdefd  44213  int-sqgeq0d  44218  rr-groth  44331  rr-grothprim  44332  rr-grothshort  44336  seff  44341  expgrowthi  44365  expgrowth  44367  binomcxplemnotnn0  44388  ee233  44551  ax6e2nd  44590  in1  44603  dfvd2ani  44615  dfvd2i  44617  dfvd3i  44624  dfvd3ani  44627  e0bi  44807  uun2221  44844  uun2221p1  44845  uun2221p2  44846  en3lpVD  44876  relopabVD  44932  ax6e2ndVD  44939  ax6e2ndALT  44961  permaxpow  45041  pssnssi  45137  nnf1oxpnn  45231  icof  45255  fnmptif  45301  rn1st  45309  negpilt0  45321  xrgtso  45383  supxrleubrnmptf  45488  xrpnf  45522  rexanuz2nf  45529  ioontr  45550  iccdifioo  45554  iccdifprioo  45555  uzinico2  45600  fsummulc1f  45610  fsumiunss  45614  fnlimfvre2  45714  limsupreuz  45774  limsup10ex  45810  icccncfext  45924  dvcosre  45949  dvsinax  45950  ioodvbdlimc1lem2  45969  ioodvbdlimc2lem  45971  dvmptmulf  45974  dvnmul  45980  dvmptfprodlem  45981  dvnprodlem2  45984  stoweidlem1  46038  stoweidlem26  46063  stoweidlem34  46071  stoweidlem44  46081  stoweid  46100  stirlinglem5  46115  dirkercncflem1  46140  fourierdlem44  46188  fourierdlem56  46199  fourierdlem62  46205  fourierdlem89  46232  fourierdlem91  46234  fourierdlem100  46243  fourierdlem102  46245  fourierdlem103  46246  fourierdlem104  46247  fourierdlem108  46251  fourierdlem112  46255  fourierdlem114  46257  fouriersw  46268  rrndistlt  46327  gsumge0cl  46408  sge0tsms  46417  sge0ltfirpmpt2  46463  ovn0  46603  hoidmv1le  46631  hoidmvle  46637  ovnsubadd2lem  46682  ovolval4lem1  46686  vonioolem2  46718  smflimlem3  46810  nsssmfmbf  46816  sinnpoly  46921  axorbtnotaiffb  46933  axorbciffatcxorb  46935  abnotbtaxb  46945  euabsneu  47058  ceilhalf1  47364  sprval  47509  fmtnoinf  47566  1nevenALTV  47721  nfermltl8rev  47772  nfermltl2rev  47773  nnsum3primes4  47818  tgblthelfgott  47845  tgoldbachlt  47846  cycl3grtri  47977  isubgr3stgrlem3  47998  usgrexmpl1lem  48051  usgrexmpl2lem  48056  usgrexmpl2trifr  48067  gpgprismgr4cycllem7  48131  ldepslinc  48540  ackval42  48727  rrx2plordso  48755  vsn  48842  dmtposss  48906  sepfsepc  48958  basresposfo  49008  rescofuf  49124  oppff1  49179  idfth  49189  idsubc  49191  fuco2eld2  49345  fuco22a  49381  setc1onsubc  49633  alimp-no-surprise  49812  aacllem  49832  amgmwlem  49833  amgmlemALT  49834