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  2199  19.36i  2231  ax6  2388  sbie  2506  datisi  2679  disamis  2680  dimatis  2687  fresison  2688  bamalip  2691  axi12  2705  eqcomi  2744  eqtri  2758  eleqtri  2832  nfnfc  2911  neii  2934  necomi  2986  neeqtri  3004  neli  3038  nrex  3064  rexlimivOLD  3170  rexlimi  3242  eueqi  3692  euxfr2w  3703  euxfr2  3705  reuxfrd  3731  cdeqri  3749  sseqtri  4007  pssn2lp  4079  equncomi  4135  unssi  4166  ssini  4215  unabs  4240  inabs  4241  dfin4  4253  vn0  4320  inindif  4350  difidALT  4352  ab0orv  4358  ab0orvALT  4359  disjdif  4447  difin0  4449  pwundif  4599  snid  4638  rabrsn  4700  iinrab2  5046  symdifv  5062  rintn0  5085  breqtri  5144  axsepgfromrep  5264  bm1.3iiOLD  5272  ax6vsep  5273  notzfaus  5333  zfpow  5336  dtruALT2  5340  dtruALT  5358  reusv2lem4  5371  dtru  5411  el  5412  dtruOLD  5416  op1stb  5446  copsexgw  5465  copsexg  5466  uniop  5490  rn0  5905  dmresi  6039  somincom  6123  cnvimassrndm  6141  cnvcnv  6181  elid  6188  rescnvcnv  6193  cnvcnvres  6194  cocnvcnv2  6247  cores2  6248  co01  6250  cnviin  6275  predres  6328  iota4an  6512  fnopab  6675  mpt0  6679  fnmpti  6680  f1cnvcnv  6782  f1ovi  6856  eliman0  6915  fvco4i  6979  cnvimainrn  7056  fmpti  7101  funiunfv  7239  oprabss  7513  relmptopab  7655  zfun  7728  tfinds2  7857  omon  7871  2nd0  7993  f1stres  8010  f2ndres  8011  cnvoprab  8057  relmpoopab  8091  df1st2  8095  df2nd2  8096  fsplit  8114  frpoins3xpg  8137  frpoins3xp3g  8138  poxp2  8140  poseq  8155  reldmtpos  8231  dftpos4  8242  tpostpos  8243  tpos0  8253  frrlem4  8286  wfrlem4OLD  8324  smo0  8370  tfrlem14  8403  tfrlem16  8405  rdgsucg  8435  rdglimg  8437  frfnom  8447  oawordeulem  8564  uniixp  8933  dfdom2  8990  ssdomg  9012  xpcomf1o  9073  sbthlem5  9099  sdom0  9120  limensuci  9165  1sdom2  9246  fiint  9336  fiintOLD  9337  fidomdm  9344  residfi  9348  mptfi  9361  fisn  9437  dffi3  9441  ordtypelem6  9535  ordtypelem7  9536  wemaplem2  9559  harwdom  9603  suc11reg  9631  zfinf  9651  axinf2  9652  noinfep  9672  cantnfvalf  9677  cantnflt  9684  cantnf0  9687  cantnf  9705  ttrclco  9730  tz9.1c  9742  tc2  9754  r111  9787  r1tr2  9789  r1ordg  9790  r1sssuc  9795  r1val1  9798  tz9.13  9803  r1elssi  9817  pwwf  9819  rankopb  9864  rankeq0b  9872  ranksuc  9877  rankmapu  9890  rankxplim3  9893  rankxpsuc  9894  cp  9903  karden  9907  card0  9970  cardlim  9984  cardom  9998  infxpenlem  10025  alephsuc2  10092  alephgeom  10094  unialeph  10113  dfac4  10134  dfacacn  10154  dju1dif  10185  dju1p1e2  10186  infdju1  10202  ackbij1lem13  10243  ackbij2  10254  cf0  10263  cfsuc  10269  cfom  10276  cfslb2n  10280  ominf4  10324  fin23lem17  10350  fin23lem28  10352  fin23lem30  10354  fin23lem31  10355  fin23lem40  10363  isfin1-3  10398  dfacfin7  10411  fin1a2lem6  10417  itunitc1  10432  axcc3  10450  dcomex  10459  axdc2lem  10460  axcclem  10469  zfac  10472  ac3  10474  ackm  10477  axac2  10478  axac  10479  axaci  10480  cardeqv  10481  numth2  10483  numth  10484  dmct  10536  brdom3  10540  fin71ac  10545  cardf  10562  aleph1  10583  cfpwsdom  10596  smobeth  10598  zfcndrep  10626  zfcndpow  10628  zfcndac  10631  gch2  10687  wunex3  10753  tskpr  10782  inar1  10787  rankcf  10789  tskcard  10793  tskuni  10795  grothpw  10838  axgroth4  10844  grothprim  10846  inaprc  10848  dmaddpi  10902  dmmulpi  10903  1lt2pi  10917  addpqf  10956  mulpqf  10958  1lt2nq  10985  supsrlem  11123  ssxr  11302  gtso  11314  subf  11482  negne0i  11556  mulnzcnf  11881  infrenegsup  12223  nnne0  12272  halflt1  12456  nn0ssz  12609  3halfnz  12670  zeo  12677  numlt  12731  numltc  12732  le9lt10  12733  decle  12740  uzf  12853  xaddf  13238  xsubge0  13275  xmulf  13286  ixxf  13370  ixxssxr  13372  iooval2  13393  ioof  13462  unirnioo  13464  dfioo2  13465  fzval2  13525  fzf  13526  0nelfz1  13558  fz10  13560  fzpreddisj  13588  4fvwrd4  13663  fzof  13671  fzo0  13698  fldiv4p1lem1div2  13850  fldiv4lem1div2  13852  om2uzoi  13971  faclbnd4lem1  14309  hashkf  14348  hashgval  14349  hashinf  14351  hashresfn  14356  hashnn0n0nn  14407  hashge3el3dif  14503  hash3tpde  14509  rev0  14780  s2dm  14907  f1oun2prg  14934  trclublem  15012  sqrt2gt1lt2  15291  limsupgord  15486  fclim  15567  fsumrelem  15821  ackbijnn  15842  incexclem  15850  incexc  15851  arisum2  15875  georeclim  15886  geoisumr  15892  0.999...  15895  risefall0lem  16040  ege2le3  16104  sin0  16165  ef01bndlem  16200  cos2bnd  16204  cos01gt0  16207  sincos2sgn  16210  sin4lt0  16211  rpnnen2lem3  16232  rpnnen2lem9  16238  rexpen  16244  cnso  16263  dvdslelem  16326  divalglem1  16411  divalglem5  16414  divalglem6  16415  divalglem10  16419  flodddiv4  16432  0bits  16456  sadcf  16470  sadcadd  16475  bitsshft  16492  smupf  16495  gcdf  16529  eucalgf  16600  2prm  16709  dfphi2  16791  pockthi  16925  prmrec  16940  vdwapf  16990  vdwlem6  17004  karatsuba  17101  1259lem5  17152  2503lem3  17156  4001lem4  17161  structcnvcnv  17170  structfn  17173  strleun  17174  imasvscafn  17549  xpsff1o  17579  wunnat  17970  dfinito3  18016  dftermo3  18017  eldmcoa  18076  coapm  18082  catcfuccl  18129  catcxpccl  18217  yonedainv  18291  smndex1bas  18882  smndex1n0mnd  18888  grpinvfvi  18963  mulgfvi  19054  ressmulgnnd  19059  symgsssg  19446  symgfisg  19447  psgnunilem5  19473  sylow3lem2  19607  oppglsm  19621  efgmf  19692  efgval  19696  efgsf  19708  0frgp  19758  dmdprd  19979  dprdval  19984  invrfval  20347  drngui  20693  rmodislmod  20885  lssintcl  20919  cnfldadd  21319  cnfldmul  21321  cnfldfunALT  21328  dfcnfldOLD  21329  cnfldfunALTOLD  21341  cnfld0  21353  cnfld1  21354  cnfld1OLD  21355  cnfldsub  21358  xrsds  21375  pzriprnglem4  21443  pzriprnglem9  21448  pzriprnglem14  21453  psgnghm  21538  zrhpsgnmhm  21542  ocv1  21637  dsmmbas2  21695  mplsubrglem  21962  opsrtoslem2  22012  evl1maprhm  22315  mdetralt  22544  maducoeval2  22576  eltpsi  22880  unitg  22903  fctop  22940  cctop  22942  ppttop  22943  epttop  22945  leordtvallem1  23146  leordtvallem2  23147  iccordt  23150  iscnp2  23175  discmp  23334  conncompcld  23370  1stcrestlem  23388  2ndcdisj  23392  topnlly  23427  disllycmp  23434  dis1stc  23435  txuni2  23501  xkotf  23521  dfac14lem  23553  prdstps  23565  txindis  23570  tx1stc  23586  xkohaus  23589  xkoptsub  23590  cnmpt1st  23604  cnmpt2nd  23605  ptcmpfi  23749  trfil1  23822  fin1aufil  23868  tgpconncompeqg  24048  tgpconncomp  24049  trust  24166  met1stc  24458  dscmet  24509  retopon  24700  cnfldtopon  24719  xrsxmet  24747  xrsmopn  24750  iimulcn  24883  iimulcnOLD  24884  icopnfhmeo  24890  iccpnfhmeo  24892  xrhmeo  24893  cnheiborlem  24902  lebnumii  24914  ishtpy  24920  htpycc  24928  pco1  24964  pcohtpylem  24968  pcopt  24971  pcopt2  24972  pcoass  24973  pcorevlem  24975  rrxcph  25342  rrx0el  25348  ovoliunlem3  25455  ovolicc1  25467  ovolicc2  25473  volf  25480  ioorf  25524  dyadf  25542  dyadmbl  25551  vitalilem5  25563  vitali  25564  mbfimaopnlem  25606  mbflimsup  25617  0plef  25623  i1fima  25629  i1fima2  25630  i1fd  25632  itg1ge0  25637  itg10  25639  i1f1lem  25640  i1fadd  25646  i1fmul  25647  i1fmulc  25654  mbfi1fseqlem5  25670  itg2addlem  25709  reldv  25821  dvbsss  25853  dvef  25934  lhop1lem  25968  deg1fvi  26040  plypf1  26167  coeeulem  26179  coeeu  26180  vieta1lem2  26269  aannenlem3  26288  aalioulem3  26292  dvradcnv  26380  pserulm  26381  pserdvlem2  26388  sinhalfpilem  26422  sincos4thpi  26472  tan4thpiOLD  26474  sincos6thpi  26475  pige3ALT  26479  resinf1o  26495  tanord1  26496  tanregt0  26498  efabl  26509  relogrn  26520  dfrelog  26524  logi  26546  logneg  26547  logltb  26559  logcn  26606  logf1o2  26609  dvlog  26610  efopnlem2  26616  efopn  26617  logccv  26622  dvsqrt  26701  dvcnsqrt  26703  cxpcn3  26708  logblog  26752  angpined  26790  1cubr  26802  asinsin  26852  asin1  26854  reasinsin  26856  atan0  26868  atanbnd  26886  atan1  26888  log2cnv  26904  log2ub  26909  log2le1  26910  birthday  26914  amgmlem  26950  emcllem5  26960  emgt0  26967  harmonicbnd3  26968  ftalem3  27035  basellem4  27044  sgmf  27105  ppi1  27124  cht1  27125  vma1  27126  ppiltx  27137  sqff1o  27142  ppiublem1  27163  ppiublem2  27164  ppiub  27165  chtub  27173  dchreq  27219  bposlem7  27251  bposlem8  27252  bposlem9  27253  lgsdir2lem2  27287  lgsdir2lem3  27288  chebbnd1  27433  chto1ub  27437  chpo1ubb  27442  pntibndlem1  27550  nosgnn0  27620  sltsolem1  27637  bdayfo  27639  nolt02o  27657  nogt01o  27658  noetasuplem4  27698  noetainflem4  27702  scutbdaybnd2lim  27779  madeun  27839  scutfo  27859  addsproplem2  27920  addsproplem7  27925  addsprop  27926  negsprop  27984  subsf  28011  mulsproplem13  28071  mulsproplem14  28072  mulsprop  28073  n0scut  28255  nohalf  28324  pw2bday  28335  0reno  28346  tgldimor  28427  tglnfn  28472  axlowdimlem4  28870  axlowdimlem16  28882  axlowdim  28886  upgrfi  29016  lfgrnloop  29050  lfuhgr1v0e  29179  usgrexmplef  29184  usgrres  29233  vdegp1bi  29463  vtxdginducedm1lem2  29466  dfpth2  29657  pthdlem2  29696  wpthswwlks2on  29889  0ewlk  30041  0pth  30052  konigsbergiedgw  30175  konigsberglem1  30179  konigsberglem2  30180  konigsberglem3  30181  konigsberglem4  30182  konigsberglem5  30183  ex-dif  30350  ex-un  30351  ex-in  30352  ex-fl  30374  avril1  30390  9p10ne21fool  30398  n0lplig  30410  cnidOLD  30509  cnnvm  30609  ipasslem8  30764  ipasslem10  30766  hvsubf  30942  normlem1  31037  normlem6  31042  normlem7  31043  norm-ii-i  31064  norm3adifii  31075  hilid  31088  hlimf  31164  hhssabloi  31189  hhssnv  31191  hhshsslem1  31194  shincli  31289  shsval2i  31314  shs0i  31376  chj0i  31382  chm1i  31383  chincli  31387  chdmm1i  31404  shjshsi  31419  chsup0  31475  h1de2bi  31481  spansnpji  31505  cmcmlem  31518  cmcmii  31524  cmcm2ii  31525  cmcm3ii  31526  pjidmi  31600  pjssmii  31608  pj0i  31620  pjocini  31625  mayetes3i  31656  df0op2  31679  hoaddcomi  31699  hoaddassi  31703  hocadddiri  31706  hocsubdiri  31707  hoaddridi  31713  ho0coi  31715  hoid1i  31716  hoid1ri  31717  hodseqi  31721  honegsubi  31723  adj1o  31821  hoddii  31916  lnopunilem1  31937  lnopunilem2  31938  nmcopexi  31954  nmcopex  31956  nmcoplb  31957  nmcfnexi  31978  nmcfnex  31980  nmcfnlb  31981  adjbd1o  32012  adjcoi  32027  nmopcoadji  32028  opsqrlem6  32072  pjsdii  32082  pjddii  32083  pjidmcoi  32104  pjtoi  32106  pjin1i  32119  pjclem1  32122  stji1i  32169  reuxfrdf  32418  iuninc  32487  fnresin  32550  rinvf1o  32554  suppss2f  32562  xppreima  32569  ofoprabco  32588  fressupp  32611  supppreima  32614  fsupprnfi  32615  gtiso  32624  df1stres  32627  df2ndres  32628  snct  32637  padct  32643  fsuppcurry1  32648  fsuppcurry2  32649  ffsrn  32652  fpwrelmapffs  32657  fzodif1  32715  nnindf  32744  nn0min  32745  dp2lt  32805  dp2ltsuc  32806  dp2ltc  32807  dplti  32825  dpmul  32833  dpmul4  32834  ressplusf  32885  chnub  32938  xrsclat  32949  xrge0base  32952  xrge00  32953  xrnarchi  33128  elrgspnlem2  33184  1fldgenq  33262  xrge0slmod  33309  zringfrac  33515  ply1degltdimlem  33608  ccfldsrarelvec  33658  ccfldextdgrr  33659  locfinreflem  33817  locfinref  33818  unicls  33880  sqsscirc1  33885  mhmhmeotmd  33904  raddcn  33906  xrge0iifiso  33912  xrge0iifhmeo  33913  lmxrge0  33929  cnzh  33945  rezh  33946  qqh0  33961  qqh1  33962  qqhre  33997  rrhre  33998  esumnul  34025  esum0  34026  esumsnf  34041  esumpfinvallem  34051  esumpfinvalf  34053  esumpcvgval  34055  esumcvgsum  34065  esumsup  34066  esumcvgre  34068  sigaclfu2  34098  dmsigagen  34121  ddemeas  34213  mbfmvolf  34244  br2base  34247  omssubadd  34278  sibfof  34318  sitg0  34324  eulerpartlemt  34349  eulerpartgbij  34350  0rrv  34429  coinfliplem  34457  coinflipprob  34458  coinfliprv  34461  ballotlem2  34467  ballotlem4  34477  ballotlem5  34478  ballotlemi1  34481  ballotlem7  34514  ballotth  34516  signsplypnf  34528  signsply0  34529  signsw0g  34534  signswch  34539  signsvf0  34558  hashreprin  34598  reprfz1  34602  chtvalz  34607  hgt750lemd  34626  hgt750lem  34629  hgt750lem2  34630  bnj1098  34760  bnj1109  34763  bnj1131  34764  bnj1533  34829  bnj151  34854  bnj580  34890  bnj852  34898  bnj864  34899  bnj865  34900  bnj978  34926  bnj1021  34943  bnj907  34944  bnj1093  34957  bnj1145  34970  bnj1172  34978  bnj1174  34980  bnj1176  34982  bnj1186  34984  nfan1c  35050  fineqvac  35074  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  35664  axrepprim  35665  axunprim  35666  axinfprim  35669  axacprim  35670  bcneg1  35699  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  36188  fneer  36317  neibastop1  36323  nabi1i  36358  nabi2i  36359  limsucncmpi  36409  knoppcnlem8  36464  knoppcnlem11  36467  cnndvlem1  36501  bj-consensusALT  36543  bj-sbidmOLD  36814  bj-n0i  36915  bj-snsetex  36927  bj-tagss  36944  bj-2upln0  36987  bj-2upln1upl  36988  bj-nuliota  37021  bj-0int  37065  bj-elid5  37133  bj-inftyexpitaufo  37166  bj-pinftyccb  37185  bj-minftyccb  37189  bj-pinftynminfty  37191  bj-isrvec  37258  iccioo01  37291  f1omptsnlem  37300  mptsnunlem  37302  topdifinffinlem  37311  relowlpssretop  37328  1oequni2o  37332  pibt2  37381  imadifss  37565  tan2h  37582  poimirlem3  37593  poimirlem9  37599  poimirlem16  37606  poimirlem17  37607  poimirlem18  37608  poimirlem19  37609  poimirlem20  37610  poimirlem22  37612  poimirlem30  37620  mblfinlem1  37627  mblfinlem2  37628  ovoliunnfl  37632  voliunnfl  37634  itg2addnclem  37641  itg2addnclem2  37642  asindmre  37673  areacirclem1  37678  fdc  37715  cntotbnd  37766  heiborlem6  37786  rrnval  37797  reheibor  37809  rngosn3  37894  brcnvrabga  38306  cnvresrn  38312  moantr  38328  inxp2  38331  dfxrn2  38340  cnvcosseq  38401  refrelcosslem  38426  1cosscnvxrn  38439  redundss3  38592  refrelsredund3  38598  refrelredund3  38601  eqvrel0  38750  eqvrelid  38753  prter2  38845  renegclALT  38927  mapdunirnN  41615  lcmeprodgcdi  41966  3factsumint2  41981  3factsumint3  41982  3factsumint4  41983  3factsumint  41984  lcmineqlem4  41991  3lexlogpow5ineq1  42013  3lexlogpow2ineq1  42017  dvrelogpow2b  42027  aks4d1p1p4  42030  aks4d1p8  42046  aks6d1c1  42075  aks6d1c2p2  42078  aks6d1c4  42083  2ap1caineq  42104  sticksstones1  42105  sticksstones2  42106  aks6d1c7lem2  42140  aks5lem3a  42148  aks5lem6  42151  unitscyglem2  42155  unitscyglem3  42156  metakunt6  42169  metakunt24  42187  sqdeccom12  42286  readvrec2  42351  readvcot  42354  resubf  42371  sn-0ne2  42396  sn-subf  42418  sn-nnne0  42438  sn-0lt1  42453  reneg1lt0  42456  rntrclfvOAI  42661  diophrw  42729  rabren3dioph  42785  pellexlem6  42804  pellex  42805  frmx  42884  frmy  42885  jm2.23  42967  jm2.27dlem3  42982  axac10  43004  pw2f1ocnv  43008  kelac2lem  43035  lmhmlnmsplit  43058  pwfi2f1o  43067  frlmpwfi  43069  insucid  43374  nla0003  43396  ifpbiidcor  43445  sucomisnotcard  43515  alephiso2  43529  alephiso3  43530  cnvnonrel  43559  rnnonrel  43562  resnonrel  43563  cononrel1  43565  cononrel2  43566  fvnonrel  43568  cnvcnvintabd  43571  cnvintabd  43574  rclexi  43586  rtrclex  43588  clcnvlem  43594  cnvrcl0  43596  dmtrcl  43598  rntrcl  43599  dfrtrcl5  43600  iunrelexp0  43673  dmtrclfvRP  43701  rntrclfv  43703  corcltrcl  43710  cotrclrcl  43713  0heALT  43754  frege54cor1a  43835  uneqsn  43996  clsk3nimkb  44011  int-sqdefd  44152  int-sqgeq0d  44157  rr-groth  44271  rr-grothprim  44272  rr-grothshort  44276  seff  44281  expgrowthi  44305  expgrowth  44307  binomcxplemnotnn0  44328  ee233  44492  ax6e2nd  44531  in1  44544  dfvd2ani  44556  dfvd2i  44558  dfvd3i  44565  dfvd3ani  44568  e0bi  44748  uun2221  44785  uun2221p1  44786  uun2221p2  44787  en3lpVD  44817  relopabVD  44873  ax6e2ndVD  44880  ax6e2ndALT  44902  permaxpow  44982  pssnssi  45073  nnf1oxpnn  45167  icof  45191  fnmptif  45237  rn1st  45245  negpilt0  45257  xrgtso  45320  supxrleubrnmptf  45426  xrpnf  45460  rexanuz2nf  45467  ioontr  45488  iccdifioo  45492  iccdifprioo  45493  uzinico2  45538  fsummulc1f  45548  fsumiunss  45552  fnlimfvre2  45654  limsupreuz  45714  limsup10ex  45750  icccncfext  45864  dvcosre  45889  dvsinax  45890  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  dvmptmulf  45914  dvnmul  45920  dvmptfprodlem  45921  dvnprodlem2  45924  stoweidlem1  45978  stoweidlem26  46003  stoweidlem34  46011  stoweidlem44  46021  stoweid  46040  stirlinglem5  46055  dirkercncflem1  46080  fourierdlem44  46128  fourierdlem56  46139  fourierdlem62  46145  fourierdlem89  46172  fourierdlem91  46174  fourierdlem100  46183  fourierdlem102  46185  fourierdlem103  46186  fourierdlem104  46187  fourierdlem108  46191  fourierdlem112  46195  fourierdlem114  46197  fouriersw  46208  rrndistlt  46267  gsumge0cl  46348  sge0tsms  46357  sge0ltfirpmpt2  46403  ovn0  46543  hoidmv1le  46571  hoidmvle  46577  ovnsubadd2lem  46622  ovolval4lem1  46626  vonioolem2  46658  smflimlem3  46750  nsssmfmbf  46756  axorbtnotaiffb  46880  axorbciffatcxorb  46882  abnotbtaxb  46892  euabsneu  47005  ceilhalf1  47311  sprval  47441  fmtnoinf  47498  1nevenALTV  47653  nfermltl8rev  47704  nfermltl2rev  47705  nnsum3primes4  47750  tgblthelfgott  47777  tgoldbachlt  47778  cycl3grtri  47907  isubgr3stgrlem3  47928  usgrexmpl1lem  47973  usgrexmpl2lem  47978  usgrexmpl2trifr  47989  gpgprismgr4cycllem7  48048  ldepslinc  48433  ackval42  48624  rrx2plordso  48652  vsn  48738  dmtposss  48799  sepfsepc  48850  basresposfo  48900  rescofuf  49004  idfth  49046  idsubc  49047  fuco2eld2  49173  fuco22a  49209  setc1onsubc  49427  alimp-no-surprise  49593  aacllem  49613  amgmwlem  49614  amgmlemALT  49615