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  820  biadanii  822  imori  855  ori  862  pm5.16  1016  dn1  1058  3ori  1427  cadan  1611  nic-dfim  1671  nic-dfneg  1672  nic-mp  1673  nic-mpALT  1674  tbw-negdf  1701  rb-imdf  1752  nfri  1791  mpgbi  1800  19.35i  1880  nfim1  2207  19.36i  2239  ax6  2389  sbie  2507  datisi  2681  disamis  2682  dimatis  2689  fresison  2690  bamalip  2693  axi12  2707  eqcomi  2746  eqtri  2760  eleqtri  2835  nfnfc  2912  neii  2935  necomi  2987  neeqtri  3005  neli  3039  nrex  3066  rexlimi  3238  eueqi  3656  euxfr2w  3667  euxfr2  3669  reuxfrd  3695  cdeqri  3713  sseqtri  3971  pssn2lp  4045  equncomi  4101  unssi  4132  ssini  4181  unabs  4206  inabs  4207  dfin4  4219  vn0  4286  inindif  4316  difidALT  4318  ab0orv  4324  ab0orvALT  4325  disjdif  4413  difin0  4415  pwundif  4566  snid  4607  rabrsn  4669  iinrab2  5013  symdifv  5029  rintn0  5052  breqtri  5111  axsepgfromrep  5229  bm1.3iiOLD  5237  ax6vsep  5238  notzfaus  5300  zfpow  5303  dtruALT2  5307  dtruALT  5325  reusv2lem4  5338  dtru  5384  elOLD  5386  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  7013  fmpti  7058  funiunfv  7196  oprabss  7468  relmptopab  7610  zfun  7683  tfinds2  7808  omon  7822  2nd0  7942  f1stres  7959  f2ndres  7960  cnvoprab  8006  relmpoopab  8037  df1st2  8041  df2nd2  8042  fsplit  8060  frpoins3xpg  8083  frpoins3xp3g  8084  poxp2  8086  poseq  8101  reldmtpos  8177  dftpos4  8188  tpostpos  8189  tpos0  8199  frrlem4  8232  smo0  8291  tfrlem14  8323  tfrlem16  8325  rdgsucg  8355  rdglimg  8357  frfnom  8367  oawordeulem  8482  uniixp  8862  dfdom2  8918  ssdomg  8940  xpcomf1o  8997  sbthlem5  9022  sdom0  9040  limensuci  9084  1sdom2  9151  fiint  9230  fidomdm  9237  residfi  9241  mptfi  9254  fisn  9333  dffi3  9337  ordtypelem6  9431  ordtypelem7  9432  wemaplem2  9455  harwdom  9499  nelaneq  9509  suc11reg  9531  zfinf  9551  axinf2  9552  noinfep  9572  cantnfvalf  9577  cantnflt  9584  cantnf0  9587  cantnf  9605  ttrclco  9630  tz9.1c  9642  tc2  9652  setinds  9661  r111  9690  r1tr2  9692  r1ordg  9693  r1sssuc  9698  r1val1  9701  tz9.13  9706  r1elssi  9720  pwwf  9722  rankopb  9767  rankeq0b  9775  ranksuc  9780  rankmapu  9793  rankxplim3  9796  rankxpsuc  9797  cp  9806  karden  9810  card0  9873  cardlim  9887  cardom  9901  infxpenlem  9926  alephsuc2  9993  alephgeom  9995  unialeph  10014  dfac4  10035  dfacacn  10055  dju1dif  10086  dju1p1e2  10087  infdju1  10103  ackbij1lem13  10144  ackbij2  10155  cf0  10164  cfsuc  10170  cfom  10177  cfslb2n  10181  ominf4  10225  fin23lem17  10251  fin23lem28  10253  fin23lem30  10255  fin23lem31  10256  fin23lem40  10264  isfin1-3  10299  dfacfin7  10312  fin1a2lem6  10318  itunitc1  10333  axcc3  10351  dcomex  10360  axdc2lem  10361  axcclem  10370  zfac  10373  ac3  10375  ackm  10378  axac2  10379  axac  10380  axaci  10381  cardeqv  10382  numth2  10384  numth  10385  dmct  10437  brdom3  10441  fin71ac  10446  cardf  10463  aleph1  10485  cfpwsdom  10498  smobeth  10500  zfcndrep  10528  zfcndpow  10530  zfcndac  10533  gch2  10589  wunex3  10655  tskpr  10684  inar1  10689  rankcf  10691  tskcard  10695  tskuni  10697  grothpw  10740  axgroth4  10746  grothprim  10748  inaprc  10750  dmaddpi  10804  dmmulpi  10805  1lt2pi  10819  addpqf  10858  mulpqf  10860  1lt2nq  10887  supsrlem  11025  ssxr  11206  gtso  11218  subf  11386  negne0i  11460  mulnzcnf  11787  infrenegsup  12130  neg1lt0  12138  nnne0  12202  halflt1  12385  nn0ssz  12538  3halfnz  12599  zeo  12606  numlt  12660  numltc  12661  le9lt10  12662  decle  12669  uzf  12782  xaddf  13167  xsubge0  13204  xmulf  13215  ixxf  13299  ixxssxr  13301  iooval2  13322  ioof  13391  unirnioo  13393  dfioo2  13394  fzval2  13455  fzf  13456  0nelfz1  13488  fz10  13490  fzpreddisj  13518  4fvwrd4  13593  fzof  13601  fzo0  13629  fldiv4p1lem1div2  13785  fldiv4lem1div2  13787  om2uzoi  13908  faclbnd4lem1  14246  hashkf  14285  hashgval  14286  hashinf  14288  hashresfn  14293  hashnn0n0nn  14344  hashge3el3dif  14440  hash3tpde  14446  rev0  14717  s2dm  14843  f1oun2prg  14870  trclublem  14948  sqrt2gt1lt2  15227  limsupgord  15425  fclim  15506  fsumrelem  15761  ackbijnn  15784  incexclem  15792  incexc  15793  arisum2  15817  georeclim  15828  geoisumr  15834  0.999...  15837  risefall0lem  15982  ege2le3  16046  sin0  16107  ef01bndlem  16142  cos2bnd  16146  cos01gt0  16149  sincos2sgn  16152  sin4lt0  16153  rpnnen2lem3  16174  rpnnen2lem9  16180  rexpen  16186  cnso  16205  dvdslelem  16269  divalglem1  16354  divalglem5  16357  divalglem6  16358  divalglem10  16362  flodddiv4  16375  0bits  16399  sadcf  16413  sadcadd  16418  bitsshft  16435  smupf  16438  gcdf  16472  eucalgf  16543  2prm  16652  dfphi2  16735  pockthi  16869  prmrec  16884  vdwapf  16934  vdwlem6  16948  karatsuba  17045  1259lem5  17096  2503lem3  17100  4001lem4  17105  structcnvcnv  17114  structfn  17117  strleun  17118  imasvscafn  17492  xpsff1o  17522  xrge0base  17562  wunnat  17917  dfinito3  17963  dftermo3  17964  eldmcoa  18023  coapm  18029  catcfuccl  18076  catcxpccl  18164  yonedainv  18238  chnub  18579  smndex1bas  18868  smndex1n0mnd  18874  grpinvfvi  18949  mulgfvi  19040  ressmulgnnd  19045  symgsssg  19433  symgfisg  19434  psgnunilem5  19460  sylow3lem2  19594  oppglsm  19608  efgmf  19679  efgval  19683  efgsf  19695  0frgp  19745  dmdprd  19966  dprdval  19971  invrfval  20360  drngui  20703  rmodislmod  20916  lssintcl  20950  cnfldadd  21350  cnfldmul  21352  cnfldfunALT  21359  dfcnfldOLD  21360  cnfldfunALTOLD  21372  cnfld0  21382  cnfld1  21383  cnfld1OLD  21384  cnfldsub  21387  xrsds  21399  pzriprnglem4  21474  pzriprnglem9  21479  pzriprnglem14  21484  psgnghm  21570  zrhpsgnmhm  21574  ocv1  21669  dsmmbas2  21727  mplsubrglem  21992  opsrtoslem2  22044  evl1maprhm  22354  mdetralt  22583  maducoeval2  22615  eltpsi  22919  unitg  22942  fctop  22979  cctop  22981  ppttop  22982  epttop  22984  leordtvallem1  23185  leordtvallem2  23186  iccordt  23189  iscnp2  23214  discmp  23373  conncompcld  23409  1stcrestlem  23427  2ndcdisj  23431  topnlly  23466  disllycmp  23473  dis1stc  23474  txuni2  23540  xkotf  23560  dfac14lem  23592  prdstps  23604  txindis  23609  tx1stc  23625  xkohaus  23628  xkoptsub  23629  cnmpt1st  23643  cnmpt2nd  23644  ptcmpfi  23788  trfil1  23861  fin1aufil  23907  tgpconncompeqg  24087  tgpconncomp  24088  trust  24204  met1stc  24496  dscmet  24547  retopon  24738  cnfldtopon  24757  xrsxmet  24785  xrsmopn  24788  iimulcn  24915  icopnfhmeo  24920  iccpnfhmeo  24922  xrhmeo  24923  cnheiborlem  24931  lebnumii  24943  ishtpy  24949  htpycc  24957  pco1  24992  pcohtpylem  24996  pcopt  24999  pcopt2  25000  pcoass  25001  pcorevlem  25003  rrxcph  25369  rrx0el  25375  ovoliunlem3  25481  ovolicc1  25493  ovolicc2  25499  volf  25506  ioorf  25550  dyadf  25568  dyadmbl  25577  vitalilem5  25589  vitali  25590  mbfimaopnlem  25632  mbflimsup  25643  0plef  25649  i1fima  25655  i1fima2  25656  i1fd  25658  itg1ge0  25663  itg10  25665  i1f1lem  25666  i1fadd  25672  i1fmul  25673  i1fmulc  25680  mbfi1fseqlem5  25696  itg2addlem  25735  reldv  25847  dvbsss  25879  dvef  25957  lhop1lem  25990  deg1fvi  26060  plypf1  26187  coeeulem  26199  coeeu  26200  vieta1lem2  26288  aannenlem3  26307  aalioulem3  26311  dvradcnv  26399  pserulm  26400  pserdvlem2  26406  sinhalfpilem  26440  sincos4thpi  26490  tan4thpiOLD  26492  sincos6thpi  26493  pige3ALT  26497  resinf1o  26513  tanord1  26514  tanregt0  26516  efabl  26527  relogrn  26538  dfrelog  26542  logi  26564  logneg  26565  logltb  26577  logcn  26624  logf1o2  26627  dvlog  26628  efopnlem2  26634  efopn  26635  logccv  26640  dvsqrt  26719  dvcnsqrt  26721  cxpcn3  26725  logblog  26769  angpined  26807  1cubr  26819  asinsin  26869  asin1  26871  reasinsin  26873  atan0  26885  atanbnd  26903  atan1  26905  log2cnv  26921  log2ub  26926  log2le1  26927  birthday  26931  amgmlem  26967  emcllem5  26977  emgt0  26984  harmonicbnd3  26985  ftalem3  27052  basellem4  27061  sgmf  27122  ppi1  27141  cht1  27142  vma1  27143  ppiltx  27154  sqff1o  27159  ppiublem1  27179  ppiublem2  27180  ppiub  27181  chtub  27189  dchreq  27235  bposlem7  27267  bposlem8  27268  bposlem9  27269  lgsdir2lem2  27303  lgsdir2lem3  27304  chebbnd1  27449  chto1ub  27453  chpo1ubb  27458  pntibndlem1  27566  nosgnn0  27636  ltssolem1  27653  bdayfo  27655  nolt02o  27673  nogt01o  27674  noetasuplem4  27714  noetainflem4  27718  cutbdaybnd2lim  27803  madeun  27890  cutsfo  27911  addsproplem2  27976  addsproplem7  27981  addsprop  27982  negsprop  28041  subsf  28070  mulsproplem13  28134  mulsproplem14  28135  mulsprop  28136  oniso  28277  n0cut  28340  bdayn0sf1o  28376  twocut  28429  bdaypw2n0bndlem  28469  bdayfinbndlem1  28473  0reno  28502  tgldimor  28584  tglnfn  28629  axlowdimlem4  29028  axlowdimlem16  29040  axlowdim  29044  upgrfi  29174  lfgrnloop  29208  lfuhgr1v0e  29337  usgrexmplef  29342  usgrres  29391  vdegp1bi  29621  vtxdginducedm1lem2  29624  dfpth2  29812  pthdlem2  29851  wpthswwlks2on  30047  0ewlk  30199  0pth  30210  konigsbergiedgw  30333  konigsberglem1  30337  konigsberglem2  30338  konigsberglem3  30339  konigsberglem4  30340  konigsberglem5  30341  ex-dif  30508  ex-un  30509  ex-in  30510  ex-fl  30532  avril1  30548  9p10ne21fool  30556  n0lplig  30569  cnidOLD  30668  cnnvm  30768  ipasslem8  30923  ipasslem10  30925  hvsubf  31101  normlem1  31196  normlem6  31201  normlem7  31202  norm-ii-i  31223  norm3adifii  31234  hilid  31247  hlimf  31323  hhssabloi  31348  hhssnv  31350  hhshsslem1  31353  shincli  31448  shsval2i  31473  shs0i  31535  chj0i  31541  chm1i  31542  chincli  31546  chdmm1i  31563  shjshsi  31578  chsup0  31634  h1de2bi  31640  spansnpji  31664  cmcmlem  31677  cmcmii  31683  cmcm2ii  31684  cmcm3ii  31685  pjidmi  31759  pjssmii  31767  pj0i  31779  pjocini  31784  mayetes3i  31815  df0op2  31838  hoaddcomi  31858  hoaddassi  31862  hocadddiri  31865  hocsubdiri  31866  hoaddridi  31872  ho0coi  31874  hoid1i  31875  hoid1ri  31876  hodseqi  31880  honegsubi  31882  adj1o  31980  hoddii  32075  lnopunilem1  32096  lnopunilem2  32097  nmcopexi  32113  nmcopex  32115  nmcoplb  32116  nmcfnexi  32137  nmcfnex  32139  nmcfnlb  32140  adjbd1o  32171  adjcoi  32186  nmopcoadji  32187  opsqrlem6  32231  pjsdii  32241  pjddii  32242  pjidmcoi  32263  pjtoi  32265  pjin1i  32278  pjclem1  32281  stji1i  32328  reuxfrdf  32575  iuninc  32645  fnresin  32712  rinvf1o  32718  suppss2f  32726  xppreima  32733  ofoprabco  32752  partfun2  32764  fressupp  32776  supppreima  32779  fsupprnfi  32780  gtiso  32789  df1stres  32792  df2ndres  32793  snct  32800  padct  32806  fsuppcurry1  32812  fsuppcurry2  32813  ffsrn  32816  fpwrelmapffs  32822  fzodif1  32880  nnindf  32908  nn0min  32909  dp2lt  32959  dp2ltsuc  32960  dp2ltc  32961  dplti  32979  dpmul  32987  dpmul4  32988  ressplusf  33038  xrsclat  33086  xrge00  33089  xrnarchi  33260  elrgspnlem2  33319  1fldgenq  33398  xrge0slmod  33423  zringfrac  33629  esplyind  33734  ply1degltdimlem  33782  ccfldsrarelvec  33831  ccfldextdgrr  33832  locfinreflem  34000  locfinref  34001  unicls  34063  sqsscirc1  34068  mhmhmeotmd  34087  raddcn  34089  xrge0iifiso  34095  xrge0iifhmeo  34096  lmxrge0  34112  cnzh  34128  rezh  34129  qqh0  34144  qqh1  34145  qqhre  34180  rrhre  34181  esumnul  34208  esum0  34209  esumsnf  34224  esumpfinvallem  34234  esumpfinvalf  34236  esumpcvgval  34238  esumcvgsum  34248  esumsup  34249  esumcvgre  34251  sigaclfu2  34281  dmsigagen  34304  ddemeas  34396  mbfmvolf  34426  br2base  34429  omssubadd  34460  sibfof  34500  sitg0  34506  eulerpartlemt  34531  eulerpartgbij  34532  0rrv  34611  coinfliplem  34639  coinflipprob  34640  coinfliprv  34643  ballotlem2  34649  ballotlem4  34659  ballotlem5  34660  ballotlemi1  34663  ballotlem7  34696  ballotth  34698  signsplypnf  34710  signsply0  34711  signsw0g  34716  signswch  34721  signsvf0  34740  hashreprin  34780  reprfz1  34784  chtvalz  34789  hgt750lemd  34808  hgt750lem  34811  hgt750lem2  34812  bnj1098  34942  bnj1109  34945  bnj1131  34946  bnj1533  35010  bnj151  35035  bnj580  35071  bnj852  35079  bnj864  35080  bnj865  35081  bnj978  35107  bnj1021  35124  bnj907  35125  bnj1093  35138  bnj1145  35151  bnj1172  35159  bnj1174  35161  bnj1176  35163  bnj1186  35165  nfan1c  35231  xoromon  35248  fineqvac  35276  tz9.1regs  35294  onvf1odlem4  35304  onvf1od  35305  subfacf  35373  subfacp1lem1  35377  subfacp1lem5  35382  subfacp1lem6  35383  subfacval3  35387  erdszelem2  35390  kur14lem4  35407  ioosconn  35445  iccllysconn  35448  satfn  35553  fmlaomn0  35588  gonan0  35590  goaln0  35591  elnanelprv  35627  msrfo  35744  mthmpps  35780  problem5  35867  quad3  35868  circum  35872  antnestALT  35892  axextprim  35899  axrepprim  35900  axunprim  35901  axinfprim  35904  axacprim  35905  bcneg1  35934  dfon2lem2  35980  dfon2lem4  35982  axextdfeq  35993  fobigcup  36096  snelsingles  36118  fullfunfnv  36144  fullfunfv  36145  rankaltopb  36177  rank0  36368  rankeq1o  36369  hfuni  36382  in-ax8  36422  fneer  36551  neibastop1  36557  nabi1i  36592  nabi2i  36593  limsucncmpi  36643  tz9.1ctco  36680  ttctr3  36693  ttcpwss  36713  knoppcnlem8  36776  knoppcnlem11  36779  cnndvlem1  36813  bj-consensusALT  36860  bj-sbidmOLD  37173  bj-n0i  37274  bj-snsetex  37286  bj-tagss  37303  bj-2upln0  37346  bj-2upln1upl  37347  bj-nuliota  37380  bj-axseprep  37397  bj-0int  37429  bj-elid5  37499  bj-inftyexpitaufo  37532  bj-pinftyccb  37551  bj-minftyccb  37555  bj-pinftynminfty  37557  bj-isrvec  37624  iccioo01  37657  f1omptsnlem  37666  mptsnunlem  37668  topdifinffinlem  37677  relowlpssretop  37694  1oequni2o  37698  pibt2  37747  imadifss  37930  tan2h  37947  poimirlem3  37958  poimirlem9  37964  poimirlem16  37971  poimirlem17  37972  poimirlem18  37973  poimirlem19  37974  poimirlem20  37975  poimirlem22  37977  poimirlem30  37985  mblfinlem1  37992  mblfinlem2  37993  ovoliunnfl  37997  voliunnfl  37999  itg2addnclem  38006  itg2addnclem2  38007  asindmre  38038  areacirclem1  38043  fdc  38080  cntotbnd  38131  heiborlem6  38151  rrnval  38162  reheibor  38174  rngosn3  38259  brcnvrabga  38677  cnvresrn  38683  moantr  38707  inxp2  38710  dfxrn2  38720  dfsucmap3  38798  dfpre4  38815  cnvcosseq  38862  refrelcosslem  38887  1cosscnvxrn  38900  redundss3  39047  refrelsredund3  39053  refrelredund3  39056  disjimeceqim  39139  eqvrel0  39224  eqvrelid  39227  prter2  39341  renegclALT  39423  mapdunirnN  42110  lcmeprodgcdi  42460  3factsumint2  42475  3factsumint3  42476  3factsumint4  42477  3factsumint  42478  lcmineqlem4  42485  3lexlogpow5ineq1  42507  3lexlogpow2ineq1  42511  dvrelogpow2b  42521  aks4d1p1p4  42524  aks4d1p8  42540  aks6d1c1  42569  aks6d1c2p2  42572  aks6d1c4  42577  2ap1caineq  42598  sticksstones1  42599  sticksstones2  42600  aks6d1c7lem2  42634  aks5lem3a  42642  aks5lem6  42645  unitscyglem2  42649  unitscyglem3  42650  sqdeccom12  42735  readvrec2  42807  readvcot  42810  resubf  42827  sn-0ne2  42852  sn-subf  42875  sn-nnne0  42919  sn-0lt1  42934  reneg1lt0  42939  rntrclfvOAI  43137  diophrw  43205  rabren3dioph  43261  pellexlem6  43280  pellex  43281  frmx  43359  frmy  43360  jm2.23  43442  jm2.27dlem3  43457  axac10  43479  pw2f1ocnv  43483  kelac2lem  43510  lmhmlnmsplit  43533  pwfi2f1o  43542  frlmpwfi  43544  insucid  43849  nla0003  43870  ifpbiidcor  43919  sucomisnotcard  43989  alephiso2  44003  alephiso3  44004  cnvnonrel  44033  rnnonrel  44036  resnonrel  44037  cononrel1  44039  cononrel2  44040  fvnonrel  44042  cnvcnvintabd  44045  cnvintabd  44048  rclexi  44060  rtrclex  44062  clcnvlem  44068  cnvrcl0  44070  dmtrcl  44072  rntrcl  44073  dfrtrcl5  44074  iunrelexp0  44147  dmtrclfvRP  44175  rntrclfv  44177  corcltrcl  44184  cotrclrcl  44187  0heALT  44228  frege54cor1a  44309  uneqsn  44470  clsk3nimkb  44485  int-sqdefd  44626  int-sqgeq0d  44631  rr-groth  44744  rr-grothprim  44745  rr-grothshort  44749  seff  44754  expgrowthi  44778  expgrowth  44780  binomcxplemnotnn0  44801  ee233  44964  ax6e2nd  45003  in1  45016  dfvd2ani  45028  dfvd2i  45030  dfvd3i  45037  dfvd3ani  45040  e0bi  45220  uun2221  45257  uun2221p1  45258  uun2221p2  45259  en3lpVD  45289  relopabVD  45345  ax6e2ndVD  45352  ax6e2ndALT  45374  permaxpow  45454  pssnssi  45549  nnf1oxpnn  45643  icof  45666  fnmptif  45712  rn1st  45720  negpilt0  45732  xrgtso  45793  supxrleubrnmptf  45897  xrpnf  45931  rexanuz2nf  45938  ioontr  45959  iccdifioo  45963  iccdifprioo  45964  uzinico2  46009  fsummulc1f  46019  fsumiunss  46023  fnlimfvre2  46123  limsupreuz  46183  limsup10ex  46219  icccncfext  46333  dvcosre  46358  dvsinax  46359  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  dvmptmulf  46383  dvnmul  46389  dvmptfprodlem  46390  dvnprodlem2  46393  stoweidlem1  46447  stoweidlem26  46472  stoweidlem34  46480  stoweidlem44  46490  stoweid  46509  stirlinglem5  46524  dirkercncflem1  46549  fourierdlem44  46597  fourierdlem56  46608  fourierdlem62  46614  fourierdlem89  46641  fourierdlem91  46643  fourierdlem100  46652  fourierdlem102  46654  fourierdlem103  46655  fourierdlem104  46656  fourierdlem108  46660  fourierdlem112  46664  fourierdlem114  46666  fouriersw  46677  rrndistlt  46736  gsumge0cl  46817  sge0tsms  46826  sge0ltfirpmpt2  46872  ovn0  47012  hoidmv1le  47040  hoidmvle  47046  ovnsubadd2lem  47091  ovolval4lem1  47095  vonioolem2  47127  smflimlem3  47219  nsssmfmbf  47225  chnerlem1  47328  nthrucw  47332  goldrasin  47344  goldrapos  47345  sinnpoly  47351  axorbtnotaiffb  47363  axorbciffatcxorb  47365  abnotbtaxb  47375  euabsneu  47488  ceilhalf1  47798  sprval  47951  fmtnoinf  48011  nprmdvdsfacm1lem2  48096  ppivalnnnprmge6  48101  ppivalnn4  48102  ppivalnn  48107  1nevenALTV  48179  nfermltl8rev  48230  nfermltl2rev  48231  nnsum3primes4  48276  tgblthelfgott  48303  tgoldbachlt  48304  cycl3grtri  48435  isubgr3stgrlem3  48456  usgrexmpl1lem  48509  usgrexmpl2lem  48514  usgrexmpl2trifr  48525  gpgprismgr4cycllem7  48589  ldepslinc  48997  ackval42  49184  rrx2plordso  49212  vsn  49299  dmtposss  49363  sepfsepc  49415  basresposfo  49465  rescofuf  49580  oppff1  49635  idfth  49645  idsubc  49647  fuco2eld2  49801  fuco22a  49837  setc1onsubc  50089  alimp-no-surprise  50268  aacllem  50288  amgmwlem  50289  amgmlemALT  50290