Theorem mpbi 233

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 219	. 2 ⊢ (𝜑 → 𝜓)
4	1, 3	ax-mp 5	1 ⊢ 𝜓

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  pm5.74i  274  notbii  323  biluk  390  pm5.19  391  pm3.24  408  dfbi  481  pm4.71i  569  pm5.32i  585  biadani  832  biadanii  834  imori  868  ori  875  pm5.16  1031  dn1  1073  3ori  1451  cadan  1642  nic-dfim  1702  nic-dfneg  1703  nic-mp  1704  nic-mpALT  1705  tbw-negdf  1732  rb-imdf  1783  nfri  1822  mpgbi  1831  19.35i  1911  nfim1  2237  19.36i  2269  ax6  2415  sbie  2533  datisi  2706  disamis  2707  dimatis  2714  fresison  2715  bamalip  2718  axi12  2732  eqcomi  2771  eqtri  2785  eleqtri  2860  nfnfc  2936  neii  2959  necomi  3011  neeqtri  3029  neli  3065  nrex  3092  rexlimi  3264  eueqi  3670  euxfr2w  3681  euxfr2  3683  reuxfrd  3709  cdeqri  3727  sseqtri  3982  pssn2lp  4056  equncomi  4110  unssi  4140  ssini  4188  unabs  4214  inabs  4215  dfin4  4227  vn0OLD  4295  inindif  4327  difidALT  4329  ab0orv  4335  ab0orvALT  4336  difin0  4431  pwundif  4585  snid  4626  rabrsn  4688  iinrab2  5032  symdifv  5050  rintn0  5073  breqtri  5134  axsepgfromrep  5253  bm1.3iiOLD  5263  ax6vsep  5264  notsep  5332  zfpow  5335  dtruALT2  5339  dtruALT  5357  reusv2lem4  5370  dtru  5416  el.OLD  5418  op1stb  5451  copsexgw  5470  copsexgwOLD  5471  copsexg  5472  uniop  5496  rn0  5914  dmresi  6052  somincom  6132  cnvimassrndm  6147  cnvcnv  6189  elid  6197  rescnvcnv  6204  cnvcnvres  6205  cocnvcnv2  6259  cores2  6260  co01  6262  cnviin  6288  predres  6341  iota4an  6519  fnopab  6674  mpt0  6678  fnmpti  6679  f1cnvcnv  6786  f1ovi  6862  eliman0  6919  fvco4i  6984  cnvimainrn  7063  fmpti  7109  funiunfv  7249  oprabss  7525  relmptopab  7668  zfun  7741  tfinds2  7864  omon  7878  2nd0  7997  f1stres  8014  f2ndres  8015  cnvoprab  8061  relmpoopab  8095  df1st2  8099  df2nd2  8100  fsplit  8118  frpoins3xpg  8142  frpoins3xp3g  8143  poxp2  8145  poseq  8160  reldmtpos  8236  dftpos4  8247  tpostpos  8248  tpos0  8258  frrlem4  8292  smo0  8351  tfrlem14  8384  tfrlem16  8386  rdgsucg  8416  rdglimg  8418  frfnom  8428  oawordeulem  8545  uniixp  8932  dfdom2  8988  ssdomg  9010  xpcomf1o  9068  sbthlem5  9093  sdom0  9111  limensuci  9155  1sdom2  9222  fiint  9300  fidomdm  9305  residfi  9309  mptfi  9322  fisn  9401  dffi3  9405  ordtypelem6  9499  ordtypelem7  9500  wemaplem2  9523  harwdom  9567  nelaneqOLD  9579  suc11reg  9602  zfinf  9622  axinf2  9623  noinfep  9643  cantnfvalf  9648  cantnflt  9655  cantnf0  9658  cantnf  9676  ttrclco  9701  tz9.1c  9713  tc2  9723  setinds  9732  r111  9761  r1tr2  9763  r1ordg  9764  r1sssuc  9769  r1val1  9772  tz9.13  9777  r1elssi  9791  pwwf  9793  rankopb  9838  rankeq0b  9846  ranksuc  9851  rankmapu  9864  rankxplim3  9867  rankxpsuc  9868  cp  9897  karden  9902  kardenOLD  9903  card0  9967  cardlim  9981  cardom  9995  infxpenlem  10020  alephsuc2  10087  alephgeom  10089  unialeph  10108  dfac4  10129  dfacacn  10148  dju1dif  10179  dju1p1e2  10180  infdju1  10196  ackbij1lem13  10237  ackbij2  10248  cf0  10256  cfsuc  10263  cfom  10270  cfslb2n  10274  ominf4  10318  fin23lem17  10344  fin23lem28  10346  fin23lem30  10348  fin23lem31  10349  fin23lem40  10357  isfin1-3  10392  dfacfin7  10405  fin1a2lem6  10411  itunitc1  10426  axcc3  10444  dcomex  10453  axdc2lem  10454  axcclem  10463  zfac  10466  ac3  10468  ackm  10471  axac2  10472  axac  10473  axaci  10474  cardeqv  10475  numth2  10477  numth  10478  dmct  10530  dmctOLD  10531  brdom3  10535  fin71ac  10540  cardf  10562  aleph1  10584  cfpwsdom  10597  smobeth  10599  zfcndrep  10627  zfcndpow  10629  zfcndac  10632  gch2  10688  wunex3  10754  tskpr  10783  inar1  10788  rankcf  10790  tskcard  10794  tskuni  10796  grothpw  10839  axgroth4  10845  grothprim  10847  inaprc  10849  dmaddpi  10903  dmmulpi  10904  1lt2pi  10918  addpqf  10957  mulpqf  10959  1lt2nq  10986  supsrlem  11124  ssxr  11307  gtso  11319  subf  11487  negne0i  11561  mulnzcnf  11888  infrenegsup  12226  neg1lt0  12234  nnne0  12298  halflt1  12489  nn0ssz  12642  3halfnz  12704  zeo  12711  numlt  12770  numltc  12771  le9lt10  12772  decle  12779  uzf  12894  xaddf  13280  xsubge0  13317  xmulf  13328  ixxf  13412  ixxssxr  13414  iooval2  13435  ioof  13504  unirnioo  13506  dfioo2  13507  fzval2  13568  fzf  13569  0nelfz1  13601  fz10  13603  fz00m1  13604  fzpreddisj  13632  4fvwrd4  13707  fzof  13715  fzo0  13743  fldiv4p1lem1div2  13900  fldiv4lem1div2  13902  om2uzoi  14023  faclbnd4lem1  14361  hashkf  14400  hashgval  14401  hashinf  14403  hashresfn  14408  hashnn0n0nn  14459  hashge3el3dif  14556  hash3tpde  14562  rev0  14837  s2dm  14965  f1oun2prg  14992  trclublem  15072  sqrt2gt1lt2  15365  limsupgord  15563  fclim  15644  fsumrelem  15898  ackbijnn  15921  incexclem  15929  incexc  15930  arisum2  15954  georeclim  15965  geoisumr  15971  0.999...  15974  ege2le3  16182  sin0  16243  ef01bndlem  16278  cos2bnd  16282  cos01gt0  16285  sincos2sgn  16288  sin4lt0  16289  rpnnen2lem3  16310  rpnnen2lem9  16316  rexpen  16322  cnso  16341  dvdslelem  16405  divalglem1  16490  divalglem5  16493  divalglem6  16494  divalglem10  16498  flodddiv4  16511  0bits  16535  sadcf  16549  sadcadd  16554  bitsshft  16571  smupf  16574  gcdf  16608  eucalgf  16679  2prm  16788  dfphi2  16871  pockthi  17005  prmrec  17020  vdwapf  17070  vdwlem6  17084  karatsuba  17181  1259lem5  17233  2503lem3  17237  4001lem4  17242  structcnvcnv  17251  structfn  17254  strleun  17255  imasvscafn  17629  xpsff1o  17659  xrge0base  17699  wunnat  18054  dfinito3  18100  dftermo3  18101  eldmcoa  18160  coapm  18166  catcfuccl  18213  catcxpccl  18301  yonedainv  18375  chnub  18716  smndex1bas  19024  smndex1n0mnd  19030  grpinvfvi  19112  mulgfvi  19202  ressmulgnnd  19207  symgsssg  19600  symgfisg  19601  psgnunilem5  19627  sylow3lem2  19761  oppglsm  19775  efgmf  19846  efgval  19850  efgsf  19862  0frgp  19912  dmdprd  20133  dprdval  20138  invrfval  20536  drngui  20902  rmodislmod  21120  lssintcl  21154  cnfldadd  21597  cnfldmul  21599  cnfldfunALT  21606  cnfld0  21615  cnfld1  21616  cnfldsub  21619  xrsds  21629  pzriprnglem4  21703  pzriprnglem9  21708  pzriprnglem14  21713  psgnghm  21799  zrhpsgnmhm  21803  ocv1  21898  dsmmbas2  21956  mplsubrglem  22224  opsrtoslem2  22278  evl1maprhm  22610  mdetralt  22836  maducoeval2  22868  eltpsi  23175  unitg  23198  fctop  23235  cctop  23237  ppttop  23238  epttop  23240  leordtvallem1  23441  leordtvallem2  23442  iccordt  23445  iscnp2  23470  discmp  23629  conncompcld  23665  1stcrestlem  23683  2ndcdisj  23688  topnlly  23723  disllycmp  23730  dis1stc  23731  txuni2  23797  xkotf  23817  dfac14lem  23849  prdstps  23861  txindis  23866  tx1stc  23882  xkohaus  23885  xkoptsub  23886  cnmpt1st  23900  cnmpt2nd  23901  ptcmpfi  24045  trfil1  24118  fin1aufil  24164  tgpconncompeqg  24344  tgpconncomp  24345  trust  24461  met1stc  24753  dscmet  24804  retopon  24995  cnfldtopon  25014  xrsxmet  25042  xrsmopn  25045  iimulcn  25172  icopnfhmeo  25177  iccpnfhmeo  25179  xrhmeo  25180  cnheiborlem  25188  lebnumii  25200  ishtpy  25206  htpycc  25214  pco1  25249  pcohtpylem  25253  pcopt  25256  pcopt2  25257  pcoass  25258  pcorevlem  25260  rrxcph  25626  rrx0el  25632  ovoliunlem3  25738  ovolicc1  25750  ovolicc2  25756  volf  25763  ioorf  25807  dyadf  25825  dyadmbl  25834  vitalilem5  25846  vitali  25847  mbfimaopnlem  25889  mbflimsup  25900  0plef  25906  i1fima  25912  i1fima2  25913  i1fd  25915  itg1ge0  25920  itg10  25922  i1f1lem  25923  i1fadd  25929  i1fmul  25930  i1fmulc  25937  mbfi1fseqlem5  25953  itg2addlem  25992  reldv  26104  dvbsss  26136  dvef  26214  lhop1lem  26247  deg1fvi  26317  plypf1  26445  coeeulem  26457  coeeu  26458  vieta1lem2  26550  aannenlem3  26573  aalioulem3  26577  dvradcnv  26664  pserulm  26665  pserdvlem2  26671  sinhalfpilem  26708  sincos4thpi  26758  tan4thpiOLD  26760  sincos6thpi  26761  pige3ALT  26765  resinf1o  26781  tanord1  26782  tanregt0  26784  efabl  26795  relogrn  26806  dfrelog  26810  logi  26832  logneg  26833  logltb  26845  logcn  26892  logf1o2  26895  dvlog  26896  efopnlem2  26902  efopn  26903  logccv  26908  dvsqrt  26987  dvcnsqrt  26989  cxpcn3  26993  logblog  27037  angpined  27075  1cubr  27087  asinsin  27137  asin1  27139  reasinsin  27141  atan0  27153  atanbnd  27171  atan1  27173  log2cnv  27189  log2ub  27194  log2le1  27195  birthday  27199  amgmlem  27234  emcllem5  27244  emgt0  27251  harmonicbnd3  27252  ftalem3  27319  basellem4  27328  sgmf  27389  ppi1  27408  cht1  27409  vma1  27410  ppiltx  27421  sqff1o  27426  ppiublem1  27446  ppiublem2  27447  ppiub  27448  chtub  27456  dchreq  27502  bposlem7  27534  bposlem8  27535  bposlem9  27536  lgsdir2lem2  27570  lgsdir2lem3  27571  chebbnd1  27716  chto1ub  27720  chpo1ubb  27725  pntibndlem1  27833  nosgnn0  27902  ltssolem1  27919  bdayfo  27921  nolt02o  27939  nogt01o  27940  noetasuplem4  27980  noetainflem4  27984  cutbdaybnd2lim  28070  madeun  28157  cutsfo  28178  addsproplem2  28243  addsproplem7  28248  addsprop  28249  negsprop  28308  subsf  28337  mulsproplem13  28401  mulsproplem14  28402  mulsprop  28403  oniso  28544  n0cut  28607  bdayn0sf1o  28643  twocut  28696  bdaypw2n0bndlem  28736  bdayfinbndlem1  28740  0reno  28769  tgldimor  28852  tglnfn  28897  tgplnfn  29140  axlowdimlem4  29410  axlowdimlem16  29422  axlowdim  29426  upgrfi  29556  lfgrnloop  29590  lfuhgr1v0e  29722  usgrexmplef  29727  usgrres  29776  vdegp1bi  30005  vtxdginducedm1lem2  30008  dfpth2  30201  pthdlem2  30241  wpthswwlks2on  30440  0ewlk  30592  0pth  30603  konigsbergiedgw  30736  konigsberglem1  30740  konigsberglem2  30741  konigsberglem3  30742  konigsberglem4  30743  konigsberglem5  30744  ex-dif  30911  ex-un  30912  ex-in  30913  ex-fl  30935  avril1  30951  9p10ne21fool  30959  n0lplig  30972  cnidOLD  31071  cnnvm  31171  ipasslem8  31326  ipasslem10  31328  hvsubf  31504  normlem1  31599  normlem6  31604  normlem7  31605  norm-ii-i  31626  norm3adifii  31637  hilid  31650  hlimf  31726  hhssabloi  31751  hhssnv  31753  hhshsslem1  31756  shincli  31851  shsval2i  31876  shs0i  31938  chj0i  31944  chm1i  31945  chincli  31949  chdmm1i  31966  shjshsi  31981  chsup0  32037  h1de2bi  32043  spansnpji  32067  cmcmlem  32080  cmcmii  32086  cmcm2ii  32087  cmcm3ii  32088  pjidmi  32162  pjssmii  32170  pj0i  32182  pjocini  32187  mayetes3i  32218  df0op2  32241  hoaddcomi  32261  hoaddassi  32265  hocadddiri  32268  hocsubdiri  32269  hoaddridi  32275  ho0coi  32277  hoid1i  32278  hoid1ri  32279  hodseqi  32283  honegsubi  32285  adj1o  32383  hoddii  32478  lnopunilem1  32499  lnopunilem2  32500  nmcopexi  32516  nmcopex  32518  nmcoplb  32519  nmcfnexi  32540  nmcfnex  32542  nmcfnlb  32543  adjbd1o  32574  adjcoi  32589  nmopcoadji  32590  opsqrlem6  32634  pjsdii  32644  pjddii  32645  pjidmcoi  32666  pjtoi  32668  pjin1i  32681  pjclem1  32684  stji1i  32731  reuxfrdf  32974  iuninc  33042  fnresin  33105  rinvf1o  33111  suppss2f  33119  xppreima  33126  ofoprabco  33145  partfun2  33157  fressupp  33168  supppreima  33171  fsupprnfi  33172  gtiso  33181  df1stres  33184  df2ndres  33185  snct  33192  padct  33197  fsuppcurry1  33203  fsuppcurry2  33204  ffsrn  33207  fpwrelmapffs  33213  fzodif1  33271  nnindf  33298  nn0min  33299  dp2lt  33338  dp2ltsuc  33339  dp2ltc  33340  dplti  33358  dpmul  33366  dpmul4  33367  ressplusf  33411  xrsclat  33459  xrge00  33462  xrnarchi  33632  elrgspnlem2  33691  1fldgenq  33771  xrge0slmod  33796  zringfrac  33972  esplyind  34093  ply1degltdimlem  34140  ccfldsrarelvec  34189  ccfldextdgrr  34190  locfinreflem  34358  locfinref  34359  unicls  34421  sqsscirc1  34426  mhmhmeotmd  34445  raddcn  34447  xrge0iifiso  34453  xrge0iifhmeo  34454  lmxrge0  34470  cnzh  34486  rezh  34487  qqh0  34502  qqh1  34503  qqhre  34538  rrhre  34539  esumnul  34566  esum0  34567  esumsnf  34582  esumpfinvallem  34592  esumpfinvalf  34594  esumpcvgval  34596  esumcvgsum  34606  esumsup  34607  esumcvgre  34609  sigaclfu2  34639  dmsigagen  34663  ddemeas  34755  mbfmvolf  34785  br2base  34788  omssubadd  34819  sibfof  34859  sitg0  34865  eulerpartlemt  34890  eulerpartgbij  34891  0rrv  34970  coinfliplem  34998  coinflipprob  34999  coinfliprv  35002  ballotlem2  35008  ballotlem4  35018  ballotlem5  35019  ballotlemi1  35022  ballotlem7  35055  ballotth  35057  signsplypnf  35066  signsply0  35067  signsw0g  35072  signswch  35077  signsvf0  35096  hashreprin  35136  reprfz1  35140  chtvalz  35145  hgt750lemd  35164  hgt750lem  35167  hgt750lem2  35168  bnj1098  35301  bnj1109  35304  bnj1131  35305  bnj1533  35369  bnj151  35394  bnj580  35430  bnj852  35438  bnj864  35439  bnj865  35440  bnj978  35466  bnj1021  35483  bnj907  35484  bnj1093  35497  bnj1145  35510  bnj1172  35518  bnj1174  35520  bnj1176  35522  bnj1186  35524  nfan1c  35590  xoromon  35601  rankfo  35627  fineqvac  35650  tz9.1regs  35668  axpowg  35680  onvf1odlem4  35711  onvf1od  35712  subfacf  35762  subfacp1lem1  35766  subfacp1lem5  35771  subfacp1lem6  35772  subfacval3  35776  erdszelem2  35779  kur14lem4  35796  ioosconn  35834  iccllysconn  35837  satfn  35942  fmlaomn0  35977  gonan0  35979  goaln0  35980  elnanelprv  36016  msrfo  36133  mthmpps  36169  problem5  36256  quad3  36257  circum  36261  antnestALT  36281  axextprim  36288  axrepprim  36289  axunprim  36290  axinfprim  36293  axacprim  36294  bcneg1  36323  dfon2lem2  36369  dfon2lem4  36371  axextdfeq  36382  fobigcup  36485  snelsingles  36507  fullfunfnv  36533  fullfunfv  36534  rankaltopb  36567  rank0  36758  rankeq1o  36759  hfuni  36772  in-ax8  36852  fneer  36980  neibastop1  36986  nabi1i  37021  nabi2i  37022  limsucncmpi  37072  tz9.1ctco  37109  ttctr3  37122  ttcpwss  37142  knoppcnlem8  37205  knoppcnlem11  37208  cnndvlem1  37242  bj-consensusALT  37288  bj-sbidmOLD  37601  bj-n0i  37703  bj-snsetex  37715  bj-tagss  37732  bj-2upln0  37775  bj-2upln1upl  37776  bj-nuliota  37809  bj-axseprep  37827  bj-0int  37859  bj-elid5  37929  bj-inftyexpitaufo  37962  bj-pinftyccb  37981  bj-minftyccb  37985  bj-pinftynminfty  37987  bj-isrvec  38054  iccioo01  38089  f1omptsnlem  38098  mptsnunlem  38100  topdifinffinlem  38109  relowlpssretop  38126  1oequni2o  38130  pibt2  38179  imadifss  38362  tan2h  38374  poimirlem3  38380  poimirlem9  38386  poimirlem16  38393  poimirlem17  38394  poimirlem18  38395  poimirlem19  38396  poimirlem20  38397  poimirlem22  38399  poimirlem30  38407  mblfinlem1  38414  mblfinlem2  38415  ovoliunnfl  38419  voliunnfl  38421  itg2addnclem  38428  itg2addnclem2  38429  asindmre  38460  areacirclem1  38465  fdc  38503  cntotbnd  38554  heiborlem6  38574  rrnval  38585  reheibor  38597  rngosn3  38682  brcnvrabga  39098  cnvresrn  39104  moantr  39128  inxp2  39131  dfxrn2  39141  dfsucmap3  39219  dfpre4  39236  cnvcosseq  39283  refrelcosslem  39308  1cosscnvxrn  39321  redundss3  39468  refrelsredund3  39474  refrelredund3  39477  disjimeceqim  39560  eqvrel0  39645  eqvrelid  39648  prter2  39762  renegclALT  39844  mapdunirnN  42531  lcmeprodgcdi  42881  3factsumint2  42896  3factsumint3  42897  3factsumint4  42898  3factsumint  42899  lcmineqlem4  42906  3lexlogpow5ineq1  42928  3lexlogpow2ineq1  42932  dvrelogpow2b  42942  aks4d1p1p4  42945  aks4d1p8  42961  aks6d1c1  42990  aks6d1c2p2  42993  aks6d1c4  42998  2ap1caineq  43019  sticksstones1  43020  sticksstones2  43021  aks6d1c7lem2  43055  aks5lem3a  43063  aks5lem6  43066  unitscyglem2  43070  unitscyglem3  43071  sqdeccom12  43172  readvrec2  43244  readvcot  43247  resubf  43264  sn-0ne2  43289  sn-subf  43312  sn-nnne0  43356  sn-0lt1  43371  reneg1lt0  43376  rntrclfvOAI  43544  diophrw  43612  rabren3dioph  43664  pellexlem6  43683  pellex  43684  frmx  43762  frmy  43763  jm2.23  43845  jm2.27dlem3  43860  axac10  43882  pw2f1ocnv  43886  kelac2lem  43913  lmhmlnmsplit  43936  pwfi2f1o  43945  frlmpwfi  43947  insucid  44252  nla0003  44273  ifpbiidcor  44322  sucomisnotcard  44392  alephiso2  44406  alephiso3  44407  cnvnonrel  44436  rnnonrel  44439  resnonrel  44440  cononrel1  44442  cononrel2  44443  fvnonrel  44445  cnvcnvintabd  44448  cnvintabd  44451  rclexi  44463  rtrclex  44465  clcnvlem  44471  cnvrcl0  44473  dmtrcl  44475  rntrcl  44476  dfrtrcl5  44477  iunrelexp0  44550  dmtrclfvRP  44578  rntrclfv  44580  corcltrcl  44587  cotrclrcl  44590  0heALT  44631  frege54cor1a  44712  uneqsn  44873  clsk3nimkb  44888  int-sqdefd  45029  int-sqgeq0d  45034  rr-groth  45131  rr-grothprim  45132  rr-grothshort  45136  seff  45141  expgrowthi  45165  expgrowth  45167  binomcxplemnotnn0  45188  ee233  45350  ax6e2nd  45389  in1  45402  dfvd2ani  45414  dfvd2i  45416  dfvd3i  45423  dfvd3ani  45426  e0bi  45606  uun2221  45643  uun2221p1  45644  uun2221p2  45645  en3lpVD  45675  relopabVD  45731  ax6e2ndVD  45738  ax6e2ndALT  45760  permaxpow  45840  pssnssi  45941  nnf1oxpnn  46035  icof  46057  fnmptif  46102  rn1st  46110  negpilt0  46122  xrgtso  46183  supxrleubrnmptf  46287  xrpnf  46321  rexanuz2nf  46328  ioontr  46349  iccdifioo  46353  iccdifprioo  46354  uzinico2  46399  fsummulc1f  46409  fsumiunss  46413  fnlimfvre2  46513  limsupreuz  46573  limsup10ex  46609  icccncfext  46723  dvcosre  46748  dvsinax  46749  ioodvbdlimc1lem2  46768  ioodvbdlimc2lem  46770  dvmptmulf  46773  dvnmul  46779  dvmptfprodlem  46780  dvnprodlem2  46783  stoweidlem1  46837  stoweidlem26  46862  stoweidlem34  46870  stoweidlem44  46880  stoweid  46899  stirlinglem5  46914  dirkercncflem1  46939  fourierdlem44  46987  fourierdlem56  46998  fourierdlem62  47004  fourierdlem89  47031  fourierdlem91  47033  fourierdlem100  47042  fourierdlem102  47044  fourierdlem103  47045  fourierdlem104  47046  fourierdlem108  47050  fourierdlem112  47054  fourierdlem114  47056  fouriersw  47067  rrndistlt  47126  gsumge0cl  47207  sge0tsms  47216  sge0ltfirpmpt2  47262  ovn0  47402  hoidmv1le  47430  hoidmvle  47436  ovnsubadd2lem  47481  ovolval4lem1  47485  vonioolem2  47517  smflimlem3  47609  nsssmfmbf  47615  chnerlem1  47718  sqrtnzqaa  47740  numtowerdt  47742  goldrasin  47755  goldrapos  47756  goldratmolem4  47761  goldratval  47762  sqrtnpoly  47769  axorbtnotaiffb  47799  axorbciffatcxorb  47801  abnotbtaxb  47811  euabsneu  47924  ceilhalf1  48234  sprval  48387  fmtnoinf  48447  nprmdvdsfacm1lem2  48532  ppivalnnnprmge6  48537  ppivalnn4  48538  ppivalnn  48543  1nevenALTV  48615  nfermltl8rev  48666  nfermltl2rev  48667  nnsum3primes4  48712  tgblthelfgott  48739  tgoldbachlt  48740  cycl3grtri  48871  isubgr3stgrlem3  48892  usgrexmpl1lem  48945  usgrexmpl2lem  48950  usgrexmpl2trifr  48961  gpgprismgr4cycllem7  49025  ldepslinc  49447  ackval42  49634  rrx2plordso  49662  vsn  49748  dmtposss  49810  sepfsepc  49862  basresposfo  49912  rescofuf  50027  oppff1  50082  idfth  50092  idsubc  50094  fuco2eld2  50248  fuco22a  50284  setc1onsubc  50536  alimp-no-surprise  50718  aacllem  50780  3elfz13  50786  veronesevrowd  50820  veroquadmodzerod  50825  veroquadnolindfd  50826  veroquaddetzerod  50827  amgmwlem  50828  amgmlemALT  50829