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 ⊢ 𝜓

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  pm5.74i  274  notbii  323  biluk  389  pm5.19  390  pm3.24  407  dfbi  480  pm4.71i  568  pm5.32i  584  biadani  831  biadanii  833  imori  867  ori  874  pm5.16  1029  dn1  1071  3ori  1447  cadan  1632  nic-dfim  1692  nic-dfneg  1693  nic-mp  1694  nic-mpALT  1695  tbw-negdf  1722  rb-imdf  1773  nfri  1812  mpgbi  1821  19.35i  1901  nfim1  2237  19.36i  2269  ax6  2418  sbie  2536  datisi  2709  disamis  2710  dimatis  2717  fresison  2718  bamalip  2721  axi12  2735  eqcomi  2774  eqtri  2788  eleqtri  2863  nfnfc  2939  neii  2962  necomi  3014  neeqtri  3032  neli  3066  nrex  3093  rexlimi  3265  eueqi  3675  euxfr2w  3686  euxfr2  3688  reuxfrd  3714  cdeqri  3732  sseqtri  3987  pssn2lp  4061  equncomi  4116  unssi  4146  ssini  4194  unabs  4220  inabs  4221  dfin4  4233  vn0  4300  inindif  4331  difidALT  4333  ab0orv  4339  ab0orvALT  4340  disjdif  4429  difin0  4431  pwundif  4583  snid  4624  rabrsn  4686  iinrab2  5030  symdifv  5048  rintn0  5071  breqtri  5130  axsepgfromrep  5249  bm1.3iiOLD  5257  ax6vsep  5258  notzfaus  5325  zfpow  5328  dtruALT2  5332  dtruALT  5350  reusv2lem4  5363  dtru  5409  elOLD  5411  op1stb  5444  copsexgw  5463  copsexgwOLD  5464  copsexg  5465  uniop  5489  rn0  5907  dmresi  6045  somincom  6125  cnvimassrndm  6141  cnvcnv  6182  elid  6190  rescnvcnv  6195  cnvcnvres  6196  cocnvcnv2  6250  cores2  6251  co01  6253  cnviin  6277  predres  6330  iota4an  6507  fnopab  6663  mpt0  6667  fnmpti  6668  f1cnvcnv  6775  f1ovi  6851  eliman0  6908  fvco4i  6973  cnvimainrn  7052  fmpti  7097  funiunfv  7236  oprabss  7508  relmptopab  7650  zfun  7723  tfinds2  7848  omon  7862  2nd0  7981  f1stres  7998  f2ndres  7999  cnvoprab  8045  relmpoopab  8077  df1st2  8081  df2nd2  8082  fsplit  8100  frpoins3xpg  8124  frpoins3xp3g  8125  poxp2  8127  poseq  8142  reldmtpos  8218  dftpos4  8229  tpostpos  8230  tpos0  8240  frrlem4  8274  smo0  8333  tfrlem14  8366  tfrlem16  8368  rdgsucg  8398  rdglimg  8400  frfnom  8410  oawordeulem  8527  uniixp  8907  dfdom2  8963  ssdomg  8985  xpcomf1o  9042  sbthlem5  9067  sdom0  9085  limensuci  9129  1sdom2  9196  fiint  9274  fidomdm  9279  residfi  9283  mptfi  9296  fisn  9375  dffi3  9379  ordtypelem6  9473  ordtypelem7  9474  wemaplem2  9497  harwdom  9541  nelaneqOLD  9553  suc11reg  9576  zfinf  9596  axinf2  9597  noinfep  9617  cantnfvalf  9622  cantnflt  9629  cantnf0  9632  cantnf  9650  ttrclco  9675  tz9.1c  9687  tc2  9697  setinds  9706  r111  9735  r1tr2  9737  r1ordg  9738  r1sssuc  9743  r1val1  9746  tz9.13  9751  r1elssi  9765  pwwf  9767  rankopb  9812  rankeq0b  9820  ranksuc  9825  rankmapu  9838  rankxplim3  9841  rankxpsuc  9842  cp  9865  karden  9869  card0  9932  cardlim  9946  cardom  9960  infxpenlem  9985  alephsuc2  10052  alephgeom  10054  unialeph  10073  dfac4  10094  dfacacn  10113  dju1dif  10144  dju1p1e2  10145  infdju1  10161  ackbij1lem13  10202  ackbij2  10213  cf0  10222  cfsuc  10229  cfom  10236  cfslb2n  10240  ominf4  10284  fin23lem17  10310  fin23lem28  10312  fin23lem30  10314  fin23lem31  10315  fin23lem40  10323  isfin1-3  10358  dfacfin7  10371  fin1a2lem6  10377  itunitc1  10392  axcc3  10410  dcomex  10419  axdc2lem  10420  axcclem  10429  zfac  10432  ac3  10434  ackm  10437  axac2  10438  axac  10439  axaci  10440  cardeqv  10441  numth2  10443  numth  10444  dmct  10496  brdom3  10500  fin71ac  10505  cardf  10522  aleph1  10544  cfpwsdom  10557  smobeth  10559  zfcndrep  10587  zfcndpow  10589  zfcndac  10592  gch2  10648  wunex3  10714  tskpr  10743  inar1  10748  rankcf  10750  tskcard  10754  tskuni  10756  grothpw  10799  axgroth4  10805  grothprim  10807  inaprc  10809  dmaddpi  10863  dmmulpi  10864  1lt2pi  10878  addpqf  10917  mulpqf  10919  1lt2nq  10946  supsrlem  11084  ssxr  11267  gtso  11279  subf  11447  negne0i  11521  mulnzcnf  11848  infrenegsup  12189  neg1lt0  12197  nnne0  12261  halflt1  12452  nn0ssz  12605  3halfnz  12666  zeo  12673  numlt  12732  numltc  12733  le9lt10  12734  decle  12741  uzf  12856  xaddf  13241  xsubge0  13278  xmulf  13289  ixxf  13373  ixxssxr  13375  iooval2  13396  ioof  13465  unirnioo  13467  dfioo2  13468  fzval2  13529  fzf  13530  0nelfz1  13562  fz10  13564  fzpreddisj  13592  4fvwrd4  13667  fzof  13675  fzo0  13703  fldiv4p1lem1div2  13859  fldiv4lem1div2  13861  om2uzoi  13982  faclbnd4lem1  14320  hashkf  14359  hashgval  14360  hashinf  14362  hashresfn  14367  hashnn0n0nn  14418  hashge3el3dif  14514  hash3tpde  14520  rev0  14791  s2dm  14917  f1oun2prg  14944  trclublem  15022  sqrt2gt1lt2  15315  limsupgord  15513  fclim  15594  fsumrelem  15849  ackbijnn  15872  incexclem  15880  incexc  15881  arisum2  15905  georeclim  15916  geoisumr  15922  0.999...  15925  risefall0lem  16070  ege2le3  16134  sin0  16195  ef01bndlem  16230  cos2bnd  16234  cos01gt0  16237  sincos2sgn  16240  sin4lt0  16241  rpnnen2lem3  16262  rpnnen2lem9  16268  rexpen  16274  cnso  16293  dvdslelem  16357  divalglem1  16442  divalglem5  16445  divalglem6  16446  divalglem10  16450  flodddiv4  16463  0bits  16487  sadcf  16501  sadcadd  16506  bitsshft  16523  smupf  16526  gcdf  16560  eucalgf  16631  2prm  16740  dfphi2  16823  pockthi  16957  prmrec  16972  vdwapf  17022  vdwlem6  17036  karatsuba  17133  1259lem5  17185  2503lem3  17189  4001lem4  17194  structcnvcnv  17203  structfn  17206  strleun  17207  imasvscafn  17581  xpsff1o  17611  xrge0base  17651  wunnat  18006  dfinito3  18052  dftermo3  18053  eldmcoa  18112  coapm  18118  catcfuccl  18165  catcxpccl  18253  yonedainv  18327  chnub  18668  smndex1bas  18958  smndex1n0mnd  18964  grpinvfvi  19039  mulgfvi  19130  ressmulgnnd  19135  symgsssg  19528  symgfisg  19529  psgnunilem5  19555  sylow3lem2  19689  oppglsm  19703  efgmf  19774  efgval  19778  efgsf  19790  0frgp  19840  dmdprd  20061  dprdval  20066  invrfval  20462  drngui  20810  rmodislmod  21020  lssintcl  21054  cnfldadd  21488  cnfldmul  21490  cnfldfunALT  21497  cnfld0  21506  cnfld1  21507  cnfldsub  21510  xrsds  21520  pzriprnglem4  21594  pzriprnglem9  21599  pzriprnglem14  21604  psgnghm  21690  zrhpsgnmhm  21694  ocv1  21789  dsmmbas2  21847  mplsubrglem  22113  opsrtoslem2  22167  evl1maprhm  22500  mdetralt  22726  maducoeval2  22758  eltpsi  23062  unitg  23085  fctop  23122  cctop  23124  ppttop  23125  epttop  23127  leordtvallem1  23328  leordtvallem2  23329  iccordt  23332  iscnp2  23357  discmp  23516  conncompcld  23552  1stcrestlem  23570  2ndcdisj  23574  topnlly  23609  disllycmp  23616  dis1stc  23617  txuni2  23683  xkotf  23703  dfac14lem  23735  prdstps  23747  txindis  23752  tx1stc  23768  xkohaus  23771  xkoptsub  23772  cnmpt1st  23786  cnmpt2nd  23787  ptcmpfi  23931  trfil1  24004  fin1aufil  24050  tgpconncompeqg  24230  tgpconncomp  24231  trust  24347  met1stc  24639  dscmet  24690  retopon  24881  cnfldtopon  24900  xrsxmet  24928  xrsmopn  24931  iimulcn  25058  icopnfhmeo  25063  iccpnfhmeo  25065  xrhmeo  25066  cnheiborlem  25074  lebnumii  25086  ishtpy  25092  htpycc  25100  pco1  25135  pcohtpylem  25139  pcopt  25142  pcopt2  25143  pcoass  25144  pcorevlem  25146  rrxcph  25512  rrx0el  25518  ovoliunlem3  25624  ovolicc1  25636  ovolicc2  25642  volf  25649  ioorf  25693  dyadf  25711  dyadmbl  25720  vitalilem5  25732  vitali  25733  mbfimaopnlem  25775  mbflimsup  25786  0plef  25792  i1fima  25798  i1fima2  25799  i1fd  25801  itg1ge0  25806  itg10  25808  i1f1lem  25809  i1fadd  25815  i1fmul  25816  i1fmulc  25823  mbfi1fseqlem5  25839  itg2addlem  25878  reldv  25990  dvbsss  26022  dvef  26100  lhop1lem  26133  deg1fvi  26203  plypf1  26330  coeeulem  26342  coeeu  26343  vieta1lem2  26433  aannenlem3  26452  aalioulem3  26456  dvradcnv  26542  pserulm  26543  pserdvlem2  26549  sinhalfpilem  26586  sincos4thpi  26636  tan4thpiOLD  26638  sincos6thpi  26639  pige3ALT  26643  resinf1o  26659  tanord1  26660  tanregt0  26662  efabl  26673  relogrn  26684  dfrelog  26688  logi  26710  logneg  26711  logltb  26723  logcn  26770  logf1o2  26773  dvlog  26774  efopnlem2  26780  efopn  26781  logccv  26786  dvsqrt  26865  dvcnsqrt  26867  cxpcn3  26871  logblog  26915  angpined  26953  1cubr  26965  asinsin  27015  asin1  27017  reasinsin  27019  atan0  27031  atanbnd  27049  atan1  27051  log2cnv  27067  log2ub  27072  log2le1  27073  birthday  27077  amgmlem  27112  emcllem5  27122  emgt0  27129  harmonicbnd3  27130  ftalem3  27197  basellem4  27206  sgmf  27267  ppi1  27286  cht1  27287  vma1  27288  ppiltx  27299  sqff1o  27304  ppiublem1  27324  ppiublem2  27325  ppiub  27326  chtub  27334  dchreq  27380  bposlem7  27412  bposlem8  27413  bposlem9  27414  lgsdir2lem2  27448  lgsdir2lem3  27449  chebbnd1  27594  chto1ub  27598  chpo1ubb  27603  pntibndlem1  27711  nosgnn0  27780  ltssolem1  27797  bdayfo  27799  nolt02o  27817  nogt01o  27818  noetasuplem4  27858  noetainflem4  27862  cutbdaybnd2lim  27948  madeun  28035  cutsfo  28056  addsproplem2  28121  addsproplem7  28126  addsprop  28127  negsprop  28186  subsf  28215  mulsproplem13  28279  mulsproplem14  28280  mulsprop  28281  oniso  28422  n0cut  28485  bdayn0sf1o  28521  twocut  28574  bdaypw2n0bndlem  28614  bdayfinbndlem1  28618  0reno  28647  tgldimor  28729  tglnfn  28774  tgplnfn  29005  axlowdimlem4  29204  axlowdimlem16  29216  axlowdim  29220  upgrfi  29350  lfgrnloop  29384  lfuhgr1v0e  29513  usgrexmplef  29518  usgrres  29567  vdegp1bi  29796  vtxdginducedm1lem2  29799  dfpth2  29987  pthdlem2  30026  wpthswwlks2on  30222  0ewlk  30374  0pth  30385  konigsbergiedgw  30508  konigsberglem1  30512  konigsberglem2  30513  konigsberglem3  30514  konigsberglem4  30515  konigsberglem5  30516  ex-dif  30683  ex-un  30684  ex-in  30685  ex-fl  30707  avril1  30723  9p10ne21fool  30731  n0lplig  30744  cnidOLD  30843  cnnvm  30943  ipasslem8  31098  ipasslem10  31100  hvsubf  31276  normlem1  31371  normlem6  31376  normlem7  31377  norm-ii-i  31398  norm3adifii  31409  hilid  31422  hlimf  31498  hhssabloi  31523  hhssnv  31525  hhshsslem1  31528  shincli  31623  shsval2i  31648  shs0i  31710  chj0i  31716  chm1i  31717  chincli  31721  chdmm1i  31738  shjshsi  31753  chsup0  31809  h1de2bi  31815  spansnpji  31839  cmcmlem  31852  cmcmii  31858  cmcm2ii  31859  cmcm3ii  31860  pjidmi  31934  pjssmii  31942  pj0i  31954  pjocini  31959  mayetes3i  31990  df0op2  32013  hoaddcomi  32033  hoaddassi  32037  hocadddiri  32040  hocsubdiri  32041  hoaddridi  32047  ho0coi  32049  hoid1i  32050  hoid1ri  32051  hodseqi  32055  honegsubi  32057  adj1o  32155  hoddii  32250  lnopunilem1  32271  lnopunilem2  32272  nmcopexi  32288  nmcopex  32290  nmcoplb  32291  nmcfnexi  32312  nmcfnex  32314  nmcfnlb  32315  adjbd1o  32346  adjcoi  32361  nmopcoadji  32362  opsqrlem6  32406  pjsdii  32416  pjddii  32417  pjidmcoi  32438  pjtoi  32440  pjin1i  32453  pjclem1  32456  stji1i  32503  reuxfrdf  32747  iuninc  32815  fnresin  32881  rinvf1o  32887  suppss2f  32895  xppreima  32902  ofoprabco  32921  partfun2  32933  fressupp  32945  supppreima  32948  fsupprnfi  32949  gtiso  32958  df1stres  32961  df2ndres  32962  snct  32969  padct  32975  fsuppcurry1  32981  fsuppcurry2  32982  ffsrn  32985  fpwrelmapffs  32991  fzodif1  33049  nnindf  33077  nn0min  33078  dp2lt  33117  dp2ltsuc  33118  dp2ltc  33119  dplti  33137  dpmul  33145  dpmul4  33146  ressplusf  33196  xrsclat  33244  xrge00  33247  xrnarchi  33417  elrgspnlem2  33476  1fldgenq  33558  xrge0slmod  33583  zringfrac  33761  esplyind  33882  ply1degltdimlem  33929  ccfldsrarelvec  33978  ccfldextdgrr  33979  locfinreflem  34147  locfinref  34148  unicls  34210  sqsscirc1  34215  mhmhmeotmd  34234  raddcn  34236  xrge0iifiso  34242  xrge0iifhmeo  34243  lmxrge0  34259  cnzh  34275  rezh  34276  qqh0  34291  qqh1  34292  qqhre  34327  rrhre  34328  esumnul  34355  esum0  34356  esumsnf  34371  esumpfinvallem  34381  esumpfinvalf  34383  esumpcvgval  34385  esumcvgsum  34395  esumsup  34396  esumcvgre  34398  sigaclfu2  34428  dmsigagen  34451  ddemeas  34543  mbfmvolf  34573  br2base  34576  omssubadd  34607  sibfof  34647  sitg0  34653  eulerpartlemt  34678  eulerpartgbij  34679  0rrv  34758  coinfliplem  34786  coinflipprob  34787  coinfliprv  34790  ballotlem2  34796  ballotlem4  34806  ballotlem5  34807  ballotlemi1  34810  ballotlem7  34843  ballotth  34845  signsplypnf  34854  signsply0  34855  signsw0g  34860  signswch  34865  signsvf0  34884  hashreprin  34924  reprfz1  34928  chtvalz  34933  hgt750lemd  34952  hgt750lem  34955  hgt750lem2  34956  bnj1098  35089  bnj1109  35092  bnj1131  35093  bnj1533  35157  bnj151  35182  bnj580  35218  bnj852  35226  bnj864  35227  bnj865  35228  bnj978  35254  bnj1021  35271  bnj907  35272  bnj1093  35285  bnj1145  35298  bnj1172  35306  bnj1174  35308  bnj1176  35310  bnj1186  35312  nfan1c  35378  xoromon  35394  fineqvac  35424  tz9.1regs  35442  axpowg  35454  onvf1odlem4  35461  onvf1od  35462  subfacf  35538  subfacp1lem1  35542  subfacp1lem5  35547  subfacp1lem6  35548  subfacval3  35552  erdszelem2  35555  kur14lem4  35572  ioosconn  35610  iccllysconn  35613  satfn  35718  fmlaomn0  35753  gonan0  35755  goaln0  35756  elnanelprv  35792  msrfo  35909  mthmpps  35945  problem5  36032  quad3  36033  circum  36037  antnestALT  36057  axextprim  36064  axrepprim  36065  axunprim  36066  axinfprim  36069  axacprim  36070  bcneg1  36099  dfon2lem2  36145  dfon2lem4  36147  axextdfeq  36158  fobigcup  36261  snelsingles  36283  fullfunfnv  36309  fullfunfv  36310  rankaltopb  36342  rank0  36533  rankeq1o  36534  hfuni  36547  in-ax8  36597  fneer  36726  neibastop1  36732  nabi1i  36767  nabi2i  36768  limsucncmpi  36818  tz9.1ctco  36855  ttctr3  36868  ttcpwss  36888  knoppcnlem8  36951  knoppcnlem11  36954  cnndvlem1  36988  bj-consensusALT  37034  bj-sbidmOLD  37347  bj-n0i  37448  bj-snsetex  37460  bj-tagss  37477  bj-2upln0  37520  bj-2upln1upl  37521  bj-nuliota  37554  bj-axseprep  37571  bj-0int  37603  bj-elid5  37673  bj-inftyexpitaufo  37706  bj-pinftyccb  37725  bj-minftyccb  37729  bj-pinftynminfty  37731  bj-isrvec  37798  iccioo01  37833  f1omptsnlem  37842  mptsnunlem  37844  topdifinffinlem  37853  relowlpssretop  37870  1oequni2o  37874  pibt2  37923  imadifss  38106  tan2h  38123  poimirlem3  38134  poimirlem9  38140  poimirlem16  38147  poimirlem17  38148  poimirlem18  38149  poimirlem19  38150  poimirlem20  38151  poimirlem22  38153  poimirlem30  38161  mblfinlem1  38168  mblfinlem2  38169  ovoliunnfl  38173  voliunnfl  38175  itg2addnclem  38182  itg2addnclem2  38183  asindmre  38214  areacirclem1  38219  fdc  38256  cntotbnd  38307  heiborlem6  38327  rrnval  38338  reheibor  38350  rngosn3  38435  brcnvrabga  38853  cnvresrn  38859  moantr  38883  inxp2  38886  dfxrn2  38896  dfsucmap3  38974  dfpre4  38991  cnvcosseq  39038  refrelcosslem  39063  1cosscnvxrn  39076  redundss3  39223  refrelsredund3  39229  refrelredund3  39232  disjimeceqim  39315  eqvrel0  39400  eqvrelid  39403  prter2  39517  renegclALT  39599  mapdunirnN  42286  lcmeprodgcdi  42636  3factsumint2  42651  3factsumint3  42652  3factsumint4  42653  3factsumint  42654  lcmineqlem4  42661  3lexlogpow5ineq1  42683  3lexlogpow2ineq1  42687  dvrelogpow2b  42697  aks4d1p1p4  42700  aks4d1p8  42716  aks6d1c1  42745  aks6d1c2p2  42748  aks6d1c4  42753  2ap1caineq  42774  sticksstones1  42775  sticksstones2  42776  aks6d1c7lem2  42810  aks5lem3a  42818  aks5lem6  42821  unitscyglem2  42825  unitscyglem3  42826  sqdeccom12  42910  readvrec2  42982  readvcot  42985  resubf  43002  sn-0ne2  43027  sn-subf  43050  sn-nnne0  43094  sn-0lt1  43109  reneg1lt0  43114  rntrclfvOAI  43284  diophrw  43352  rabren3dioph  43404  pellexlem6  43423  pellex  43424  frmx  43502  frmy  43503  jm2.23  43585  jm2.27dlem3  43600  axac10  43622  pw2f1ocnv  43626  kelac2lem  43653  lmhmlnmsplit  43676  pwfi2f1o  43685  frlmpwfi  43687  insucid  43992  nla0003  44013  ifpbiidcor  44062  sucomisnotcard  44132  alephiso2  44146  alephiso3  44147  cnvnonrel  44176  rnnonrel  44179  resnonrel  44180  cononrel1  44182  cononrel2  44183  fvnonrel  44185  cnvcnvintabd  44188  cnvintabd  44191  rclexi  44203  rtrclex  44205  clcnvlem  44211  cnvrcl0  44213  dmtrcl  44215  rntrcl  44216  dfrtrcl5  44217  iunrelexp0  44290  dmtrclfvRP  44318  rntrclfv  44320  corcltrcl  44327  cotrclrcl  44330  0heALT  44371  frege54cor1a  44452  uneqsn  44613  clsk3nimkb  44628  int-sqdefd  44769  int-sqgeq0d  44774  rr-groth  44873  rr-grothprim  44874  rr-grothshort  44878  seff  44883  expgrowthi  44907  expgrowth  44909  binomcxplemnotnn0  44930  ee233  45093  ax6e2nd  45132  in1  45145  dfvd2ani  45157  dfvd2i  45159  dfvd3i  45166  dfvd3ani  45169  e0bi  45349  uun2221  45386  uun2221p1  45387  uun2221p2  45388  en3lpVD  45418  relopabVD  45474  ax6e2ndVD  45481  ax6e2ndALT  45503  permaxpow  45583  pssnssi  45677  nnf1oxpnn  45771  icof  45793  fnmptif  45838  rn1st  45846  negpilt0  45858  xrgtso  45919  supxrleubrnmptf  46023  xrpnf  46057  rexanuz2nf  46064  ioontr  46085  iccdifioo  46089  iccdifprioo  46090  uzinico2  46135  fsummulc1f  46145  fsumiunss  46149  fnlimfvre2  46249  limsupreuz  46309  limsup10ex  46345  icccncfext  46459  dvcosre  46484  dvsinax  46485  ioodvbdlimc1lem2  46504  ioodvbdlimc2lem  46506  dvmptmulf  46509  dvnmul  46515  dvmptfprodlem  46516  dvnprodlem2  46519  stoweidlem1  46573  stoweidlem26  46598  stoweidlem34  46606  stoweidlem44  46616  stoweid  46635  stirlinglem5  46650  dirkercncflem1  46675  fourierdlem44  46723  fourierdlem56  46734  fourierdlem62  46740  fourierdlem89  46767  fourierdlem91  46769  fourierdlem100  46778  fourierdlem102  46780  fourierdlem103  46781  fourierdlem104  46782  fourierdlem108  46786  fourierdlem112  46790  fourierdlem114  46792  fouriersw  46803  rrndistlt  46862  gsumge0cl  46943  sge0tsms  46952  sge0ltfirpmpt2  46998  ovn0  47138  hoidmv1le  47166  hoidmvle  47172  ovnsubadd2lem  47217  ovolval4lem1  47221  vonioolem2  47253  smflimlem3  47345  nsssmfmbf  47351  chnerlem1  47456  nthrucw  47460  goldrasin  47474  goldrapos  47475  sinnpoly  47483  axorbtnotaiffb  47495  axorbciffatcxorb  47497  abnotbtaxb  47507  euabsneu  47620  ceilhalf1  47930  sprval  48083  fmtnoinf  48143  nprmdvdsfacm1lem2  48228  ppivalnnnprmge6  48233  ppivalnn4  48234  ppivalnn  48239  1nevenALTV  48311  nfermltl8rev  48362  nfermltl2rev  48363  nnsum3primes4  48408  tgblthelfgott  48435  tgoldbachlt  48436  cycl3grtri  48567  isubgr3stgrlem3  48588  usgrexmpl1lem  48641  usgrexmpl2lem  48646  usgrexmpl2trifr  48657  gpgprismgr4cycllem7  48721  ldepslinc  49140  ackval42  49327  rrx2plordso  49355  vsn  49441  dmtposss  49505  sepfsepc  49557  basresposfo  49607  rescofuf  49722  oppff1  49777  idfth  49787  idsubc  49789  fuco2eld2  49943  fuco22a  49979  setc1onsubc  50231  alimp-no-surprise  50410  aacllem  50430  amgmwlem  50431  amgmlemALT  50432