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  2206  19.36i  2238  ax6  2388  sbie  2506  datisi  2680  disamis  2681  dimatis  2688  fresison  2689  bamalip  2692  axi12  2706  eqcomi  2745  eqtri  2759  eleqtri  2834  nfnfc  2911  neii  2934  necomi  2986  neeqtri  3004  neli  3038  nrex  3064  rexlimi  3236  eueqi  3667  euxfr2w  3678  euxfr2  3680  reuxfrd  3706  cdeqri  3724  sseqtri  3982  pssn2lp  4056  equncomi  4112  unssi  4143  ssini  4192  unabs  4217  inabs  4218  dfin4  4230  vn0  4297  inindif  4327  difidALT  4329  ab0orv  4335  ab0orvALT  4336  disjdif  4424  difin0  4426  pwundif  4578  snid  4619  rabrsn  4681  iinrab2  5025  symdifv  5041  rintn0  5064  breqtri  5123  axsepgfromrep  5239  bm1.3iiOLD  5247  ax6vsep  5248  notzfaus  5308  zfpow  5311  dtruALT2  5315  dtruALT  5333  reusv2lem4  5346  dtru  5386  el  5387  op1stb  5419  copsexgw  5438  copsexg  5439  uniop  5463  rn0  5875  dmresi  6011  somincom  6091  cnvimassrndm  6110  cnvcnv  6150  elid  6157  rescnvcnv  6162  cnvcnvres  6163  cocnvcnv2  6217  cores2  6218  co01  6220  cnviin  6244  predres  6297  iota4an  6474  fnopab  6630  mpt0  6634  fnmpti  6635  f1cnvcnv  6739  f1ovi  6814  eliman0  6871  fvco4i  6935  cnvimainrn  7012  fmpti  7057  funiunfv  7194  oprabss  7466  relmptopab  7608  zfun  7681  tfinds2  7806  omon  7820  2nd0  7940  f1stres  7957  f2ndres  7958  cnvoprab  8004  relmpoopab  8036  df1st2  8040  df2nd2  8041  fsplit  8059  frpoins3xpg  8082  frpoins3xp3g  8083  poxp2  8085  poseq  8100  reldmtpos  8176  dftpos4  8187  tpostpos  8188  tpos0  8198  frrlem4  8231  smo0  8290  tfrlem14  8322  tfrlem16  8324  rdgsucg  8354  rdglimg  8356  frfnom  8366  oawordeulem  8481  uniixp  8859  dfdom2  8915  ssdomg  8937  xpcomf1o  8994  sbthlem5  9019  sdom0  9037  limensuci  9081  1sdom2  9148  fiint  9227  fidomdm  9234  residfi  9238  mptfi  9251  fisn  9330  dffi3  9334  ordtypelem6  9428  ordtypelem7  9429  wemaplem2  9452  harwdom  9496  nelaneq  9506  suc11reg  9528  zfinf  9548  axinf2  9549  noinfep  9569  cantnfvalf  9574  cantnflt  9581  cantnf0  9584  cantnf  9602  ttrclco  9627  tz9.1c  9639  tc2  9649  setinds  9658  r111  9687  r1tr2  9689  r1ordg  9690  r1sssuc  9695  r1val1  9698  tz9.13  9703  r1elssi  9717  pwwf  9719  rankopb  9764  rankeq0b  9772  ranksuc  9777  rankmapu  9790  rankxplim3  9793  rankxpsuc  9794  cp  9803  karden  9807  card0  9870  cardlim  9884  cardom  9898  infxpenlem  9923  alephsuc2  9990  alephgeom  9992  unialeph  10011  dfac4  10032  dfacacn  10052  dju1dif  10083  dju1p1e2  10084  infdju1  10100  ackbij1lem13  10141  ackbij2  10152  cf0  10161  cfsuc  10167  cfom  10174  cfslb2n  10178  ominf4  10222  fin23lem17  10248  fin23lem28  10250  fin23lem30  10252  fin23lem31  10253  fin23lem40  10261  isfin1-3  10296  dfacfin7  10309  fin1a2lem6  10315  itunitc1  10330  axcc3  10348  dcomex  10357  axdc2lem  10358  axcclem  10367  zfac  10370  ac3  10372  ackm  10375  axac2  10376  axac  10377  axaci  10378  cardeqv  10379  numth2  10381  numth  10382  dmct  10434  brdom3  10438  fin71ac  10443  cardf  10460  aleph1  10482  cfpwsdom  10495  smobeth  10497  zfcndrep  10525  zfcndpow  10527  zfcndac  10530  gch2  10586  wunex3  10652  tskpr  10681  inar1  10686  rankcf  10688  tskcard  10692  tskuni  10694  grothpw  10737  axgroth4  10743  grothprim  10745  inaprc  10747  dmaddpi  10801  dmmulpi  10802  1lt2pi  10816  addpqf  10855  mulpqf  10857  1lt2nq  10884  supsrlem  11022  ssxr  11202  gtso  11214  subf  11382  negne0i  11456  mulnzcnf  11783  infrenegsup  12125  neg1lt0  12133  nnne0  12179  halflt1  12358  nn0ssz  12511  3halfnz  12571  zeo  12578  numlt  12632  numltc  12633  le9lt10  12634  decle  12641  uzf  12754  xaddf  13139  xsubge0  13176  xmulf  13187  ixxf  13271  ixxssxr  13273  iooval2  13294  ioof  13363  unirnioo  13365  dfioo2  13366  fzval2  13426  fzf  13427  0nelfz1  13459  fz10  13461  fzpreddisj  13489  4fvwrd4  13564  fzof  13572  fzo0  13599  fldiv4p1lem1div2  13755  fldiv4lem1div2  13757  om2uzoi  13878  faclbnd4lem1  14216  hashkf  14255  hashgval  14256  hashinf  14258  hashresfn  14263  hashnn0n0nn  14314  hashge3el3dif  14410  hash3tpde  14416  rev0  14687  s2dm  14813  f1oun2prg  14840  trclublem  14918  sqrt2gt1lt2  15197  limsupgord  15395  fclim  15476  fsumrelem  15730  ackbijnn  15751  incexclem  15759  incexc  15760  arisum2  15784  georeclim  15795  geoisumr  15801  0.999...  15804  risefall0lem  15949  ege2le3  16013  sin0  16074  ef01bndlem  16109  cos2bnd  16113  cos01gt0  16116  sincos2sgn  16119  sin4lt0  16120  rpnnen2lem3  16141  rpnnen2lem9  16147  rexpen  16153  cnso  16172  dvdslelem  16236  divalglem1  16321  divalglem5  16324  divalglem6  16325  divalglem10  16329  flodddiv4  16342  0bits  16366  sadcf  16380  sadcadd  16385  bitsshft  16402  smupf  16405  gcdf  16439  eucalgf  16510  2prm  16619  dfphi2  16701  pockthi  16835  prmrec  16850  vdwapf  16900  vdwlem6  16914  karatsuba  17011  1259lem5  17062  2503lem3  17066  4001lem4  17071  structcnvcnv  17080  structfn  17083  strleun  17084  imasvscafn  17458  xpsff1o  17488  xrge0base  17528  wunnat  17883  dfinito3  17929  dftermo3  17930  eldmcoa  17989  coapm  17995  catcfuccl  18042  catcxpccl  18130  yonedainv  18204  chnub  18545  smndex1bas  18831  smndex1n0mnd  18837  grpinvfvi  18912  mulgfvi  19003  ressmulgnnd  19008  symgsssg  19396  symgfisg  19397  psgnunilem5  19423  sylow3lem2  19557  oppglsm  19571  efgmf  19642  efgval  19646  efgsf  19658  0frgp  19708  dmdprd  19929  dprdval  19934  invrfval  20325  drngui  20668  rmodislmod  20881  lssintcl  20915  cnfldadd  21315  cnfldmul  21317  cnfldfunALT  21324  dfcnfldOLD  21325  cnfldfunALTOLD  21337  cnfld0  21347  cnfld1  21348  cnfld1OLD  21349  cnfldsub  21352  xrsds  21364  pzriprnglem4  21439  pzriprnglem9  21444  pzriprnglem14  21449  psgnghm  21535  zrhpsgnmhm  21539  ocv1  21634  dsmmbas2  21692  mplsubrglem  21959  opsrtoslem2  22011  evl1maprhm  22323  mdetralt  22552  maducoeval2  22584  eltpsi  22888  unitg  22911  fctop  22948  cctop  22950  ppttop  22951  epttop  22953  leordtvallem1  23154  leordtvallem2  23155  iccordt  23158  iscnp2  23183  discmp  23342  conncompcld  23378  1stcrestlem  23396  2ndcdisj  23400  topnlly  23435  disllycmp  23442  dis1stc  23443  txuni2  23509  xkotf  23529  dfac14lem  23561  prdstps  23573  txindis  23578  tx1stc  23594  xkohaus  23597  xkoptsub  23598  cnmpt1st  23612  cnmpt2nd  23613  ptcmpfi  23757  trfil1  23830  fin1aufil  23876  tgpconncompeqg  24056  tgpconncomp  24057  trust  24173  met1stc  24465  dscmet  24516  retopon  24707  cnfldtopon  24726  xrsxmet  24754  xrsmopn  24757  iimulcn  24890  iimulcnOLD  24891  icopnfhmeo  24897  iccpnfhmeo  24899  xrhmeo  24900  cnheiborlem  24909  lebnumii  24921  ishtpy  24927  htpycc  24935  pco1  24971  pcohtpylem  24975  pcopt  24978  pcopt2  24979  pcoass  24980  pcorevlem  24982  rrxcph  25348  rrx0el  25354  ovoliunlem3  25461  ovolicc1  25473  ovolicc2  25479  volf  25486  ioorf  25530  dyadf  25548  dyadmbl  25557  vitalilem5  25569  vitali  25570  mbfimaopnlem  25612  mbflimsup  25623  0plef  25629  i1fima  25635  i1fima2  25636  i1fd  25638  itg1ge0  25643  itg10  25645  i1f1lem  25646  i1fadd  25652  i1fmul  25653  i1fmulc  25660  mbfi1fseqlem5  25676  itg2addlem  25715  reldv  25827  dvbsss  25859  dvef  25940  lhop1lem  25974  deg1fvi  26046  plypf1  26173  coeeulem  26185  coeeu  26186  vieta1lem2  26275  aannenlem3  26294  aalioulem3  26298  dvradcnv  26386  pserulm  26387  pserdvlem2  26394  sinhalfpilem  26428  sincos4thpi  26478  tan4thpiOLD  26480  sincos6thpi  26481  pige3ALT  26485  resinf1o  26501  tanord1  26502  tanregt0  26504  efabl  26515  relogrn  26526  dfrelog  26530  logi  26552  logneg  26553  logltb  26565  logcn  26612  logf1o2  26615  dvlog  26616  efopnlem2  26622  efopn  26623  logccv  26628  dvsqrt  26707  dvcnsqrt  26709  cxpcn3  26714  logblog  26758  angpined  26796  1cubr  26808  asinsin  26858  asin1  26860  reasinsin  26862  atan0  26874  atanbnd  26892  atan1  26894  log2cnv  26910  log2ub  26915  log2le1  26916  birthday  26920  amgmlem  26956  emcllem5  26966  emgt0  26973  harmonicbnd3  26974  ftalem3  27041  basellem4  27050  sgmf  27111  ppi1  27130  cht1  27131  vma1  27132  ppiltx  27143  sqff1o  27148  ppiublem1  27169  ppiublem2  27170  ppiub  27171  chtub  27179  dchreq  27225  bposlem7  27257  bposlem8  27258  bposlem9  27259  lgsdir2lem2  27293  lgsdir2lem3  27294  chebbnd1  27439  chto1ub  27443  chpo1ubb  27448  pntibndlem1  27556  nosgnn0  27626  ltssolem1  27643  bdayfo  27645  nolt02o  27663  nogt01o  27664  noetasuplem4  27704  noetainflem4  27708  cutbdaybnd2lim  27793  madeun  27880  cutsfo  27901  addsproplem2  27966  addsproplem7  27971  addsprop  27972  negsprop  28031  subsf  28060  mulsproplem13  28124  mulsproplem14  28125  mulsprop  28126  oniso  28267  n0cut  28330  bdayn0sf1o  28366  twocut  28419  bdaypw2n0bndlem  28459  bdayfinbndlem1  28463  0reno  28492  tgldimor  28574  tglnfn  28619  axlowdimlem4  29018  axlowdimlem16  29030  axlowdim  29034  upgrfi  29164  lfgrnloop  29198  lfuhgr1v0e  29327  usgrexmplef  29332  usgrres  29381  vdegp1bi  29611  vtxdginducedm1lem2  29614  dfpth2  29802  pthdlem2  29841  wpthswwlks2on  30037  0ewlk  30189  0pth  30200  konigsbergiedgw  30323  konigsberglem1  30327  konigsberglem2  30328  konigsberglem3  30329  konigsberglem4  30330  konigsberglem5  30331  ex-dif  30498  ex-un  30499  ex-in  30500  ex-fl  30522  avril1  30538  9p10ne21fool  30546  n0lplig  30558  cnidOLD  30657  cnnvm  30757  ipasslem8  30912  ipasslem10  30914  hvsubf  31090  normlem1  31185  normlem6  31190  normlem7  31191  norm-ii-i  31212  norm3adifii  31223  hilid  31236  hlimf  31312  hhssabloi  31337  hhssnv  31339  hhshsslem1  31342  shincli  31437  shsval2i  31462  shs0i  31524  chj0i  31530  chm1i  31531  chincli  31535  chdmm1i  31552  shjshsi  31567  chsup0  31623  h1de2bi  31629  spansnpji  31653  cmcmlem  31666  cmcmii  31672  cmcm2ii  31673  cmcm3ii  31674  pjidmi  31748  pjssmii  31756  pj0i  31768  pjocini  31773  mayetes3i  31804  df0op2  31827  hoaddcomi  31847  hoaddassi  31851  hocadddiri  31854  hocsubdiri  31855  hoaddridi  31861  ho0coi  31863  hoid1i  31864  hoid1ri  31865  hodseqi  31869  honegsubi  31871  adj1o  31969  hoddii  32064  lnopunilem1  32085  lnopunilem2  32086  nmcopexi  32102  nmcopex  32104  nmcoplb  32105  nmcfnexi  32126  nmcfnex  32128  nmcfnlb  32129  adjbd1o  32160  adjcoi  32175  nmopcoadji  32176  opsqrlem6  32220  pjsdii  32230  pjddii  32231  pjidmcoi  32252  pjtoi  32254  pjin1i  32267  pjclem1  32270  stji1i  32317  reuxfrdf  32565  iuninc  32635  fnresin  32702  rinvf1o  32708  suppss2f  32716  xppreima  32723  ofoprabco  32742  partfun2  32755  fressupp  32767  supppreima  32770  fsupprnfi  32771  gtiso  32780  df1stres  32783  df2ndres  32784  snct  32791  padct  32797  fsuppcurry1  32803  fsuppcurry2  32804  ffsrn  32807  fpwrelmapffs  32813  fzodif1  32872  nnindf  32900  nn0min  32901  dp2lt  32966  dp2ltsuc  32967  dp2ltc  32968  dplti  32986  dpmul  32994  dpmul4  32995  ressplusf  33045  xrsclat  33093  xrge00  33096  xrnarchi  33266  elrgspnlem2  33325  1fldgenq  33404  xrge0slmod  33429  zringfrac  33635  esplyind  33731  ply1degltdimlem  33779  ccfldsrarelvec  33828  ccfldextdgrr  33829  locfinreflem  33997  locfinref  33998  unicls  34060  sqsscirc1  34065  mhmhmeotmd  34084  raddcn  34086  xrge0iifiso  34092  xrge0iifhmeo  34093  lmxrge0  34109  cnzh  34125  rezh  34126  qqh0  34141  qqh1  34142  qqhre  34177  rrhre  34178  esumnul  34205  esum0  34206  esumsnf  34221  esumpfinvallem  34231  esumpfinvalf  34233  esumpcvgval  34235  esumcvgsum  34245  esumsup  34246  esumcvgre  34248  sigaclfu2  34278  dmsigagen  34301  ddemeas  34393  mbfmvolf  34423  br2base  34426  omssubadd  34457  sibfof  34497  sitg0  34503  eulerpartlemt  34528  eulerpartgbij  34529  0rrv  34608  coinfliplem  34636  coinflipprob  34637  coinfliprv  34640  ballotlem2  34646  ballotlem4  34656  ballotlem5  34657  ballotlemi1  34660  ballotlem7  34693  ballotth  34695  signsplypnf  34707  signsply0  34708  signsw0g  34713  signswch  34718  signsvf0  34737  hashreprin  34777  reprfz1  34781  chtvalz  34786  hgt750lemd  34805  hgt750lem  34808  hgt750lem2  34809  bnj1098  34939  bnj1109  34942  bnj1131  34943  bnj1533  35008  bnj151  35033  bnj580  35069  bnj852  35077  bnj864  35078  bnj865  35079  bnj978  35105  bnj1021  35122  bnj907  35123  bnj1093  35136  bnj1145  35149  bnj1172  35157  bnj1174  35159  bnj1176  35161  bnj1186  35163  nfan1c  35229  xoromon  35245  fineqvac  35272  tz9.1regs  35290  onvf1odlem4  35300  onvf1od  35301  subfacf  35369  subfacp1lem1  35373  subfacp1lem5  35378  subfacp1lem6  35379  subfacval3  35383  erdszelem2  35386  kur14lem4  35403  ioosconn  35441  iccllysconn  35444  satfn  35549  fmlaomn0  35584  gonan0  35586  goaln0  35587  elnanelprv  35623  msrfo  35740  mthmpps  35776  problem5  35863  quad3  35864  circum  35868  antnestALT  35888  axextprim  35895  axrepprim  35896  axunprim  35897  axinfprim  35900  axacprim  35901  bcneg1  35930  dfon2lem2  35976  dfon2lem4  35978  axextdfeq  35989  fobigcup  36092  snelsingles  36114  fullfunfnv  36140  fullfunfv  36141  rankaltopb  36173  rank0  36364  rankeq1o  36365  hfuni  36378  in-ax8  36418  fneer  36547  neibastop1  36553  nabi1i  36588  nabi2i  36589  limsucncmpi  36639  knoppcnlem8  36700  knoppcnlem11  36703  cnndvlem1  36737  bj-consensusALT  36779  bj-sbidmOLD  37051  bj-n0i  37152  bj-snsetex  37164  bj-tagss  37181  bj-2upln0  37224  bj-2upln1upl  37225  bj-nuliota  37258  bj-0int  37302  bj-elid5  37370  bj-inftyexpitaufo  37403  bj-pinftyccb  37422  bj-minftyccb  37426  bj-pinftynminfty  37428  bj-isrvec  37495  iccioo01  37528  f1omptsnlem  37537  mptsnunlem  37539  topdifinffinlem  37548  relowlpssretop  37565  1oequni2o  37569  pibt2  37618  imadifss  37792  tan2h  37809  poimirlem3  37820  poimirlem9  37826  poimirlem16  37833  poimirlem17  37834  poimirlem18  37835  poimirlem19  37836  poimirlem20  37837  poimirlem22  37839  poimirlem30  37847  mblfinlem1  37854  mblfinlem2  37855  ovoliunnfl  37859  voliunnfl  37861  itg2addnclem  37868  itg2addnclem2  37869  asindmre  37900  areacirclem1  37905  fdc  37942  cntotbnd  37993  heiborlem6  38013  rrnval  38024  reheibor  38036  rngosn3  38121  brcnvrabga  38531  cnvresrn  38537  moantr  38553  inxp2  38556  dfxrn2  38566  dfsucmap3  38633  dfpre4  38650  cnvcosseq  38696  refrelcosslem  38721  1cosscnvxrn  38734  redundss3  38881  refrelsredund3  38887  refrelredund3  38890  eqvrel0  39041  eqvrelid  39044  prter2  39137  renegclALT  39219  mapdunirnN  41906  lcmeprodgcdi  42257  3factsumint2  42272  3factsumint3  42273  3factsumint4  42274  3factsumint  42275  lcmineqlem4  42282  3lexlogpow5ineq1  42304  3lexlogpow2ineq1  42308  dvrelogpow2b  42318  aks4d1p1p4  42321  aks4d1p8  42337  aks6d1c1  42366  aks6d1c2p2  42369  aks6d1c4  42374  2ap1caineq  42395  sticksstones1  42396  sticksstones2  42397  aks6d1c7lem2  42431  aks5lem3a  42439  aks5lem6  42442  unitscyglem2  42446  unitscyglem3  42447  sqdeccom12  42540  readvrec2  42612  readvcot  42615  resubf  42632  sn-0ne2  42657  sn-subf  42680  sn-nnne0  42711  sn-0lt1  42726  reneg1lt0  42731  rntrclfvOAI  42929  diophrw  42997  rabren3dioph  43053  pellexlem6  43072  pellex  43073  frmx  43151  frmy  43152  jm2.23  43234  jm2.27dlem3  43249  axac10  43271  pw2f1ocnv  43275  kelac2lem  43302  lmhmlnmsplit  43325  pwfi2f1o  43334  frlmpwfi  43336  insucid  43641  nla0003  43662  ifpbiidcor  43711  sucomisnotcard  43781  alephiso2  43795  alephiso3  43796  cnvnonrel  43825  rnnonrel  43828  resnonrel  43829  cononrel1  43831  cononrel2  43832  fvnonrel  43834  cnvcnvintabd  43837  cnvintabd  43840  rclexi  43852  rtrclex  43854  clcnvlem  43860  cnvrcl0  43862  dmtrcl  43864  rntrcl  43865  dfrtrcl5  43866  iunrelexp0  43939  dmtrclfvRP  43967  rntrclfv  43969  corcltrcl  43976  cotrclrcl  43979  0heALT  44020  frege54cor1a  44101  uneqsn  44262  clsk3nimkb  44277  int-sqdefd  44418  int-sqgeq0d  44423  rr-groth  44536  rr-grothprim  44537  rr-grothshort  44541  seff  44546  expgrowthi  44570  expgrowth  44572  binomcxplemnotnn0  44593  ee233  44756  ax6e2nd  44795  in1  44808  dfvd2ani  44820  dfvd2i  44822  dfvd3i  44829  dfvd3ani  44832  e0bi  45012  uun2221  45049  uun2221p1  45050  uun2221p2  45051  en3lpVD  45081  relopabVD  45137  ax6e2ndVD  45144  ax6e2ndALT  45166  permaxpow  45246  pssnssi  45341  nnf1oxpnn  45435  icof  45459  fnmptif  45505  rn1st  45513  negpilt0  45525  xrgtso  45586  supxrleubrnmptf  45691  xrpnf  45725  rexanuz2nf  45732  ioontr  45753  iccdifioo  45757  iccdifprioo  45758  uzinico2  45803  fsummulc1f  45813  fsumiunss  45817  fnlimfvre2  45917  limsupreuz  45977  limsup10ex  46013  icccncfext  46127  dvcosre  46152  dvsinax  46153  ioodvbdlimc1lem2  46172  ioodvbdlimc2lem  46174  dvmptmulf  46177  dvnmul  46183  dvmptfprodlem  46184  dvnprodlem2  46187  stoweidlem1  46241  stoweidlem26  46266  stoweidlem34  46274  stoweidlem44  46284  stoweid  46303  stirlinglem5  46318  dirkercncflem1  46343  fourierdlem44  46391  fourierdlem56  46402  fourierdlem62  46408  fourierdlem89  46435  fourierdlem91  46437  fourierdlem100  46446  fourierdlem102  46448  fourierdlem103  46449  fourierdlem104  46450  fourierdlem108  46454  fourierdlem112  46458  fourierdlem114  46460  fouriersw  46471  rrndistlt  46530  gsumge0cl  46611  sge0tsms  46620  sge0ltfirpmpt2  46666  ovn0  46806  hoidmv1le  46834  hoidmvle  46840  ovnsubadd2lem  46885  ovolval4lem1  46889  vonioolem2  46921  smflimlem3  47013  nsssmfmbf  47019  chnerlem1  47122  nthrucw  47126  sinnpoly  47133  axorbtnotaiffb  47145  axorbciffatcxorb  47147  abnotbtaxb  47157  euabsneu  47270  ceilhalf1  47576  sprval  47721  fmtnoinf  47778  1nevenALTV  47933  nfermltl8rev  47984  nfermltl2rev  47985  nnsum3primes4  48030  tgblthelfgott  48057  tgoldbachlt  48058  cycl3grtri  48189  isubgr3stgrlem3  48210  usgrexmpl1lem  48263  usgrexmpl2lem  48268  usgrexmpl2trifr  48279  gpgprismgr4cycllem7  48343  ldepslinc  48751  ackval42  48938  rrx2plordso  48966  vsn  49053  dmtposss  49117  sepfsepc  49169  basresposfo  49219  rescofuf  49334  oppff1  49389  idfth  49399  idsubc  49401  fuco2eld2  49555  fuco22a  49591  setc1onsubc  49843  alimp-no-surprise  50022  aacllem  50042  amgmwlem  50043  amgmlemALT  50044