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  2382  sbie  2500  datisi  2673  disamis  2674  dimatis  2681  fresison  2682  bamalip  2685  axi12  2699  eqcomi  2738  eqtri  2752  eleqtri  2826  nfnfc  2904  neii  2927  necomi  2979  neeqtri  2997  neli  3031  nrex  3057  rexlimivOLD  3163  rexlimi  3237  eueqi  3680  euxfr2w  3691  euxfr2  3693  reuxfrd  3719  cdeqri  3737  sseqtri  3995  pssn2lp  4067  equncomi  4123  unssi  4154  ssini  4203  unabs  4228  inabs  4229  dfin4  4241  vn0  4308  inindif  4338  difidALT  4340  ab0orv  4346  ab0orvALT  4347  disjdif  4435  difin0  4437  pwundif  4587  snid  4626  rabrsn  4688  iinrab2  5034  symdifv  5050  rintn0  5073  breqtri  5132  axsepgfromrep  5249  bm1.3iiOLD  5257  ax6vsep  5258  notzfaus  5318  zfpow  5321  dtruALT2  5325  dtruALT  5343  reusv2lem4  5356  dtru  5396  el  5397  dtruOLD  5401  op1stb  5431  copsexgw  5450  copsexg  5451  uniop  5475  rn0  5889  dmresi  6023  somincom  6107  cnvimassrndm  6125  cnvcnv  6165  elid  6172  rescnvcnv  6177  cnvcnvres  6178  cocnvcnv2  6231  cores2  6232  co01  6234  cnviin  6259  predres  6312  iota4an  6493  fnopab  6656  mpt0  6660  fnmpti  6661  f1cnvcnv  6765  f1ovi  6839  eliman0  6898  fvco4i  6962  cnvimainrn  7039  fmpti  7084  funiunfv  7222  oprabss  7497  relmptopab  7639  zfun  7712  tfinds2  7840  omon  7854  2nd0  7975  f1stres  7992  f2ndres  7993  cnvoprab  8039  relmpoopab  8073  df1st2  8077  df2nd2  8078  fsplit  8096  frpoins3xpg  8119  frpoins3xp3g  8120  poxp2  8122  poseq  8137  reldmtpos  8213  dftpos4  8224  tpostpos  8225  tpos0  8235  frrlem4  8268  smo0  8327  tfrlem14  8359  tfrlem16  8361  rdgsucg  8391  rdglimg  8393  frfnom  8403  oawordeulem  8518  uniixp  8894  dfdom2  8949  ssdomg  8971  xpcomf1o  9030  sbthlem5  9055  sdom0  9073  limensuci  9117  1sdom2  9187  fiint  9277  fiintOLD  9278  fidomdm  9285  residfi  9289  mptfi  9302  fisn  9378  dffi3  9382  ordtypelem6  9476  ordtypelem7  9477  wemaplem2  9500  harwdom  9544  suc11reg  9572  zfinf  9592  axinf2  9593  noinfep  9613  cantnfvalf  9618  cantnflt  9625  cantnf0  9628  cantnf  9646  ttrclco  9671  tz9.1c  9683  tc2  9695  r111  9728  r1tr2  9730  r1ordg  9731  r1sssuc  9736  r1val1  9739  tz9.13  9744  r1elssi  9758  pwwf  9760  rankopb  9805  rankeq0b  9813  ranksuc  9818  rankmapu  9831  rankxplim3  9834  rankxpsuc  9835  cp  9844  karden  9848  card0  9911  cardlim  9925  cardom  9939  infxpenlem  9966  alephsuc2  10033  alephgeom  10035  unialeph  10054  dfac4  10075  dfacacn  10095  dju1dif  10126  dju1p1e2  10127  infdju1  10143  ackbij1lem13  10184  ackbij2  10195  cf0  10204  cfsuc  10210  cfom  10217  cfslb2n  10221  ominf4  10265  fin23lem17  10291  fin23lem28  10293  fin23lem30  10295  fin23lem31  10296  fin23lem40  10304  isfin1-3  10339  dfacfin7  10352  fin1a2lem6  10358  itunitc1  10373  axcc3  10391  dcomex  10400  axdc2lem  10401  axcclem  10410  zfac  10413  ac3  10415  ackm  10418  axac2  10419  axac  10420  axaci  10421  cardeqv  10422  numth2  10424  numth  10425  dmct  10477  brdom3  10481  fin71ac  10486  cardf  10503  aleph1  10524  cfpwsdom  10537  smobeth  10539  zfcndrep  10567  zfcndpow  10569  zfcndac  10572  gch2  10628  wunex3  10694  tskpr  10723  inar1  10728  rankcf  10730  tskcard  10734  tskuni  10736  grothpw  10779  axgroth4  10785  grothprim  10787  inaprc  10789  dmaddpi  10843  dmmulpi  10844  1lt2pi  10858  addpqf  10897  mulpqf  10899  1lt2nq  10926  supsrlem  11064  ssxr  11243  gtso  11255  subf  11423  negne0i  11497  mulnzcnf  11824  infrenegsup  12166  neg1lt0  12174  nnne0  12220  halflt1  12399  nn0ssz  12552  3halfnz  12613  zeo  12620  numlt  12674  numltc  12675  le9lt10  12676  decle  12683  uzf  12796  xaddf  13184  xsubge0  13221  xmulf  13232  ixxf  13316  ixxssxr  13318  iooval2  13339  ioof  13408  unirnioo  13410  dfioo2  13411  fzval2  13471  fzf  13472  0nelfz1  13504  fz10  13506  fzpreddisj  13534  4fvwrd4  13609  fzof  13617  fzo0  13644  fldiv4p1lem1div2  13797  fldiv4lem1div2  13799  om2uzoi  13920  faclbnd4lem1  14258  hashkf  14297  hashgval  14298  hashinf  14300  hashresfn  14305  hashnn0n0nn  14356  hashge3el3dif  14452  hash3tpde  14458  rev0  14729  s2dm  14856  f1oun2prg  14883  trclublem  14961  sqrt2gt1lt2  15240  limsupgord  15438  fclim  15519  fsumrelem  15773  ackbijnn  15794  incexclem  15802  incexc  15803  arisum2  15827  georeclim  15838  geoisumr  15844  0.999...  15847  risefall0lem  15992  ege2le3  16056  sin0  16117  ef01bndlem  16152  cos2bnd  16156  cos01gt0  16159  sincos2sgn  16162  sin4lt0  16163  rpnnen2lem3  16184  rpnnen2lem9  16190  rexpen  16196  cnso  16215  dvdslelem  16279  divalglem1  16364  divalglem5  16367  divalglem6  16368  divalglem10  16372  flodddiv4  16385  0bits  16409  sadcf  16423  sadcadd  16428  bitsshft  16445  smupf  16448  gcdf  16482  eucalgf  16553  2prm  16662  dfphi2  16744  pockthi  16878  prmrec  16893  vdwapf  16943  vdwlem6  16957  karatsuba  17054  1259lem5  17105  2503lem3  17109  4001lem4  17114  structcnvcnv  17123  structfn  17126  strleun  17127  imasvscafn  17500  xpsff1o  17530  wunnat  17921  dfinito3  17967  dftermo3  17968  eldmcoa  18027  coapm  18033  catcfuccl  18080  catcxpccl  18168  yonedainv  18242  smndex1bas  18833  smndex1n0mnd  18839  grpinvfvi  18914  mulgfvi  19005  ressmulgnnd  19010  symgsssg  19397  symgfisg  19398  psgnunilem5  19424  sylow3lem2  19558  oppglsm  19572  efgmf  19643  efgval  19647  efgsf  19659  0frgp  19709  dmdprd  19930  dprdval  19935  invrfval  20298  drngui  20644  rmodislmod  20836  lssintcl  20870  cnfldadd  21270  cnfldmul  21272  cnfldfunALT  21279  dfcnfldOLD  21280  cnfldfunALTOLD  21292  cnfld0  21304  cnfld1  21305  cnfld1OLD  21306  cnfldsub  21309  xrsds  21326  pzriprnglem4  21394  pzriprnglem9  21399  pzriprnglem14  21404  psgnghm  21489  zrhpsgnmhm  21493  ocv1  21588  dsmmbas2  21646  mplsubrglem  21913  opsrtoslem2  21963  evl1maprhm  22266  mdetralt  22495  maducoeval2  22527  eltpsi  22831  unitg  22854  fctop  22891  cctop  22893  ppttop  22894  epttop  22896  leordtvallem1  23097  leordtvallem2  23098  iccordt  23101  iscnp2  23126  discmp  23285  conncompcld  23321  1stcrestlem  23339  2ndcdisj  23343  topnlly  23378  disllycmp  23385  dis1stc  23386  txuni2  23452  xkotf  23472  dfac14lem  23504  prdstps  23516  txindis  23521  tx1stc  23537  xkohaus  23540  xkoptsub  23541  cnmpt1st  23555  cnmpt2nd  23556  ptcmpfi  23700  trfil1  23773  fin1aufil  23819  tgpconncompeqg  23999  tgpconncomp  24000  trust  24117  met1stc  24409  dscmet  24460  retopon  24651  cnfldtopon  24670  xrsxmet  24698  xrsmopn  24701  iimulcn  24834  iimulcnOLD  24835  icopnfhmeo  24841  iccpnfhmeo  24843  xrhmeo  24844  cnheiborlem  24853  lebnumii  24865  ishtpy  24871  htpycc  24879  pco1  24915  pcohtpylem  24919  pcopt  24922  pcopt2  24923  pcoass  24924  pcorevlem  24926  rrxcph  25292  rrx0el  25298  ovoliunlem3  25405  ovolicc1  25417  ovolicc2  25423  volf  25430  ioorf  25474  dyadf  25492  dyadmbl  25501  vitalilem5  25513  vitali  25514  mbfimaopnlem  25556  mbflimsup  25567  0plef  25573  i1fima  25579  i1fima2  25580  i1fd  25582  itg1ge0  25587  itg10  25589  i1f1lem  25590  i1fadd  25596  i1fmul  25597  i1fmulc  25604  mbfi1fseqlem5  25620  itg2addlem  25659  reldv  25771  dvbsss  25803  dvef  25884  lhop1lem  25918  deg1fvi  25990  plypf1  26117  coeeulem  26129  coeeu  26130  vieta1lem2  26219  aannenlem3  26238  aalioulem3  26242  dvradcnv  26330  pserulm  26331  pserdvlem2  26338  sinhalfpilem  26372  sincos4thpi  26422  tan4thpiOLD  26424  sincos6thpi  26425  pige3ALT  26429  resinf1o  26445  tanord1  26446  tanregt0  26448  efabl  26459  relogrn  26470  dfrelog  26474  logi  26496  logneg  26497  logltb  26509  logcn  26556  logf1o2  26559  dvlog  26560  efopnlem2  26566  efopn  26567  logccv  26572  dvsqrt  26651  dvcnsqrt  26653  cxpcn3  26658  logblog  26702  angpined  26740  1cubr  26752  asinsin  26802  asin1  26804  reasinsin  26806  atan0  26818  atanbnd  26836  atan1  26838  log2cnv  26854  log2ub  26859  log2le1  26860  birthday  26864  amgmlem  26900  emcllem5  26910  emgt0  26917  harmonicbnd3  26918  ftalem3  26985  basellem4  26994  sgmf  27055  ppi1  27074  cht1  27075  vma1  27076  ppiltx  27087  sqff1o  27092  ppiublem1  27113  ppiublem2  27114  ppiub  27115  chtub  27123  dchreq  27169  bposlem7  27201  bposlem8  27202  bposlem9  27203  lgsdir2lem2  27237  lgsdir2lem3  27238  chebbnd1  27383  chto1ub  27387  chpo1ubb  27392  pntibndlem1  27500  nosgnn0  27570  sltsolem1  27587  bdayfo  27589  nolt02o  27607  nogt01o  27608  noetasuplem4  27648  noetainflem4  27652  scutbdaybnd2lim  27729  madeun  27795  scutfo  27816  addsproplem2  27877  addsproplem7  27882  addsprop  27883  negsprop  27941  subsf  27968  mulsproplem13  28031  mulsproplem14  28032  mulsprop  28033  onsiso  28169  n0scut  28226  bdayn0sf1o  28259  twocut  28309  0reno  28348  tgldimor  28429  tglnfn  28474  axlowdimlem4  28872  axlowdimlem16  28884  axlowdim  28888  upgrfi  29018  lfgrnloop  29052  lfuhgr1v0e  29181  usgrexmplef  29186  usgrres  29235  vdegp1bi  29465  vtxdginducedm1lem2  29468  dfpth2  29659  pthdlem2  29698  wpthswwlks2on  29891  0ewlk  30043  0pth  30054  konigsbergiedgw  30177  konigsberglem1  30181  konigsberglem2  30182  konigsberglem3  30183  konigsberglem4  30184  konigsberglem5  30185  ex-dif  30352  ex-un  30353  ex-in  30354  ex-fl  30376  avril1  30392  9p10ne21fool  30400  n0lplig  30412  cnidOLD  30511  cnnvm  30611  ipasslem8  30766  ipasslem10  30768  hvsubf  30944  normlem1  31039  normlem6  31044  normlem7  31045  norm-ii-i  31066  norm3adifii  31077  hilid  31090  hlimf  31166  hhssabloi  31191  hhssnv  31193  hhshsslem1  31196  shincli  31291  shsval2i  31316  shs0i  31378  chj0i  31384  chm1i  31385  chincli  31389  chdmm1i  31406  shjshsi  31421  chsup0  31477  h1de2bi  31483  spansnpji  31507  cmcmlem  31520  cmcmii  31526  cmcm2ii  31527  cmcm3ii  31528  pjidmi  31602  pjssmii  31610  pj0i  31622  pjocini  31627  mayetes3i  31658  df0op2  31681  hoaddcomi  31701  hoaddassi  31705  hocadddiri  31708  hocsubdiri  31709  hoaddridi  31715  ho0coi  31717  hoid1i  31718  hoid1ri  31719  hodseqi  31723  honegsubi  31725  adj1o  31823  hoddii  31918  lnopunilem1  31939  lnopunilem2  31940  nmcopexi  31956  nmcopex  31958  nmcoplb  31959  nmcfnexi  31980  nmcfnex  31982  nmcfnlb  31983  adjbd1o  32014  adjcoi  32029  nmopcoadji  32030  opsqrlem6  32074  pjsdii  32084  pjddii  32085  pjidmcoi  32106  pjtoi  32108  pjin1i  32121  pjclem1  32124  stji1i  32171  reuxfrdf  32420  iuninc  32489  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  33138  elrgspnlem2  33194  1fldgenq  33272  xrge0slmod  33319  zringfrac  33525  ply1degltdimlem  33618  ccfldsrarelvec  33666  ccfldextdgrr  33667  locfinreflem  33830  locfinref  33831  unicls  33893  sqsscirc1  33898  mhmhmeotmd  33917  raddcn  33919  xrge0iifiso  33925  xrge0iifhmeo  33926  lmxrge0  33942  cnzh  33958  rezh  33959  qqh0  33974  qqh1  33975  qqhre  34010  rrhre  34011  esumnul  34038  esum0  34039  esumsnf  34054  esumpfinvallem  34064  esumpfinvalf  34066  esumpcvgval  34068  esumcvgsum  34078  esumsup  34079  esumcvgre  34081  sigaclfu2  34111  dmsigagen  34134  ddemeas  34226  mbfmvolf  34257  br2base  34260  omssubadd  34291  sibfof  34331  sitg0  34337  eulerpartlemt  34362  eulerpartgbij  34363  0rrv  34442  coinfliplem  34470  coinflipprob  34471  coinfliprv  34474  ballotlem2  34480  ballotlem4  34490  ballotlem5  34491  ballotlemi1  34494  ballotlem7  34527  ballotth  34529  signsplypnf  34541  signsply0  34542  signsw0g  34547  signswch  34552  signsvf0  34571  hashreprin  34611  reprfz1  34615  chtvalz  34620  hgt750lemd  34639  hgt750lem  34642  hgt750lem2  34643  bnj1098  34773  bnj1109  34776  bnj1131  34777  bnj1533  34842  bnj151  34867  bnj580  34903  bnj852  34911  bnj864  34912  bnj865  34913  bnj978  34939  bnj1021  34956  bnj907  34957  bnj1093  34970  bnj1145  34983  bnj1172  34991  bnj1174  34993  bnj1176  34995  bnj1186  34997  nfan1c  35063  fineqvac  35087  onvf1odlem4  35093  onvf1od  35094  subfacf  35162  subfacp1lem1  35166  subfacp1lem5  35171  subfacp1lem6  35172  subfacval3  35176  erdszelem2  35179  kur14lem4  35196  ioosconn  35234  iccllysconn  35237  satfn  35342  fmlaomn0  35377  gonan0  35379  goaln0  35380  elnanelprv  35416  msrfo  35533  mthmpps  35569  problem5  35656  quad3  35657  circum  35661  antnestALT  35681  axextprim  35688  axrepprim  35689  axunprim  35690  axinfprim  35693  axacprim  35694  bcneg1  35723  setinds  35766  dfon2lem2  35772  dfon2lem4  35774  axextdfeq  35785  fobigcup  35888  snelsingles  35910  fullfunfnv  35934  fullfunfv  35935  rankaltopb  35967  rank0  36158  rankeq1o  36159  hfuni  36172  in-ax8  36212  fneer  36341  neibastop1  36347  nabi1i  36382  nabi2i  36383  limsucncmpi  36433  knoppcnlem8  36488  knoppcnlem11  36491  cnndvlem1  36525  bj-consensusALT  36567  bj-sbidmOLD  36838  bj-n0i  36939  bj-snsetex  36951  bj-tagss  36968  bj-2upln0  37011  bj-2upln1upl  37012  bj-nuliota  37045  bj-0int  37089  bj-elid5  37157  bj-inftyexpitaufo  37190  bj-pinftyccb  37209  bj-minftyccb  37213  bj-pinftynminfty  37215  bj-isrvec  37282  iccioo01  37315  f1omptsnlem  37324  mptsnunlem  37326  topdifinffinlem  37335  relowlpssretop  37352  1oequni2o  37356  pibt2  37405  imadifss  37589  tan2h  37606  poimirlem3  37617  poimirlem9  37623  poimirlem16  37630  poimirlem17  37631  poimirlem18  37632  poimirlem19  37633  poimirlem20  37634  poimirlem22  37636  poimirlem30  37644  mblfinlem1  37651  mblfinlem2  37652  ovoliunnfl  37656  voliunnfl  37658  itg2addnclem  37665  itg2addnclem2  37666  asindmre  37697  areacirclem1  37702  fdc  37739  cntotbnd  37790  heiborlem6  37810  rrnval  37821  reheibor  37833  rngosn3  37918  brcnvrabga  38324  cnvresrn  38330  moantr  38346  inxp2  38349  dfxrn2  38358  cnvcosseq  38428  refrelcosslem  38453  1cosscnvxrn  38466  redundss3  38619  refrelsredund3  38625  refrelredund3  38628  eqvrel0  38778  eqvrelid  38781  prter2  38874  renegclALT  38956  mapdunirnN  41644  lcmeprodgcdi  41995  3factsumint2  42010  3factsumint3  42011  3factsumint4  42012  3factsumint  42013  lcmineqlem4  42020  3lexlogpow5ineq1  42042  3lexlogpow2ineq1  42046  dvrelogpow2b  42056  aks4d1p1p4  42059  aks4d1p8  42075  aks6d1c1  42104  aks6d1c2p2  42107  aks6d1c4  42112  2ap1caineq  42133  sticksstones1  42134  sticksstones2  42135  aks6d1c7lem2  42169  aks5lem3a  42177  aks5lem6  42180  unitscyglem2  42184  unitscyglem3  42185  sqdeccom12  42277  readvrec2  42349  readvcot  42352  resubf  42369  sn-0ne2  42394  sn-subf  42417  sn-nnne0  42448  sn-0lt1  42463  reneg1lt0  42468  rntrclfvOAI  42679  diophrw  42747  rabren3dioph  42803  pellexlem6  42822  pellex  42823  frmx  42902  frmy  42903  jm2.23  42985  jm2.27dlem3  43000  axac10  43022  pw2f1ocnv  43026  kelac2lem  43053  lmhmlnmsplit  43076  pwfi2f1o  43085  frlmpwfi  43087  insucid  43392  nla0003  43414  ifpbiidcor  43463  sucomisnotcard  43533  alephiso2  43547  alephiso3  43548  cnvnonrel  43577  rnnonrel  43580  resnonrel  43581  cononrel1  43583  cononrel2  43584  fvnonrel  43586  cnvcnvintabd  43589  cnvintabd  43592  rclexi  43604  rtrclex  43606  clcnvlem  43612  cnvrcl0  43614  dmtrcl  43616  rntrcl  43617  dfrtrcl5  43618  iunrelexp0  43691  dmtrclfvRP  43719  rntrclfv  43721  corcltrcl  43728  cotrclrcl  43731  0heALT  43772  frege54cor1a  43853  uneqsn  44014  clsk3nimkb  44029  int-sqdefd  44170  int-sqgeq0d  44175  rr-groth  44288  rr-grothprim  44289  rr-grothshort  44293  seff  44298  expgrowthi  44322  expgrowth  44324  binomcxplemnotnn0  44345  ee233  44509  ax6e2nd  44548  in1  44561  dfvd2ani  44573  dfvd2i  44575  dfvd3i  44582  dfvd3ani  44585  e0bi  44765  uun2221  44802  uun2221p1  44803  uun2221p2  44804  en3lpVD  44834  relopabVD  44890  ax6e2ndVD  44897  ax6e2ndALT  44919  permaxpow  44999  pssnssi  45095  nnf1oxpnn  45189  icof  45213  fnmptif  45259  rn1st  45267  negpilt0  45279  xrgtso  45341  supxrleubrnmptf  45447  xrpnf  45481  rexanuz2nf  45488  ioontr  45509  iccdifioo  45513  iccdifprioo  45514  uzinico2  45559  fsummulc1f  45569  fsumiunss  45573  fnlimfvre2  45675  limsupreuz  45735  limsup10ex  45771  icccncfext  45885  dvcosre  45910  dvsinax  45911  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvmptmulf  45935  dvnmul  45941  dvmptfprodlem  45942  dvnprodlem2  45945  stoweidlem1  45999  stoweidlem26  46024  stoweidlem34  46032  stoweidlem44  46042  stoweid  46061  stirlinglem5  46076  dirkercncflem1  46101  fourierdlem44  46149  fourierdlem56  46160  fourierdlem62  46166  fourierdlem89  46193  fourierdlem91  46195  fourierdlem100  46204  fourierdlem102  46206  fourierdlem103  46207  fourierdlem104  46208  fourierdlem108  46212  fourierdlem112  46216  fourierdlem114  46218  fouriersw  46229  rrndistlt  46288  gsumge0cl  46369  sge0tsms  46378  sge0ltfirpmpt2  46424  ovn0  46564  hoidmv1le  46592  hoidmvle  46598  ovnsubadd2lem  46643  ovolval4lem1  46647  vonioolem2  46679  smflimlem3  46771  nsssmfmbf  46777  sinnpoly  46892  axorbtnotaiffb  46904  axorbciffatcxorb  46906  abnotbtaxb  46916  euabsneu  47029  ceilhalf1  47335  sprval  47480  fmtnoinf  47537  1nevenALTV  47692  nfermltl8rev  47743  nfermltl2rev  47744  nnsum3primes4  47789  tgblthelfgott  47816  tgoldbachlt  47817  cycl3grtri  47946  isubgr3stgrlem3  47967  usgrexmpl1lem  48012  usgrexmpl2lem  48017  usgrexmpl2trifr  48028  gpgprismgr4cycllem7  48091  ldepslinc  48498  ackval42  48685  rrx2plordso  48713  vsn  48800  dmtposss  48864  sepfsepc  48916  basresposfo  48966  rescofuf  49082  oppff1  49137  idfth  49147  idsubc  49149  fuco2eld2  49303  fuco22a  49339  setc1onsubc  49591  alimp-no-surprise  49770  aacllem  49790  amgmwlem  49791  amgmlemALT  49792