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  3669  euxfr2w  3680  euxfr2  3682  reuxfrd  3708  cdeqri  3726  sseqtri  3984  pssn2lp  4058  equncomi  4114  unssi  4145  ssini  4194  unabs  4219  inabs  4220  dfin4  4232  vn0  4299  inindif  4329  difidALT  4331  ab0orv  4337  ab0orvALT  4338  disjdif  4426  difin0  4428  pwundif  4580  snid  4621  rabrsn  4683  iinrab2  5027  symdifv  5043  rintn0  5066  breqtri  5125  axsepgfromrep  5241  bm1.3iiOLD  5249  ax6vsep  5250  notzfaus  5310  zfpow  5313  dtruALT2  5317  dtruALT  5335  reusv2lem4  5348  dtru  5393  el  5394  op1stb  5427  copsexgw  5446  copsexg  5447  uniop  5471  rn0  5883  dmresi  6019  somincom  6099  cnvimassrndm  6118  cnvcnv  6158  elid  6165  rescnvcnv  6170  cnvcnvres  6171  cocnvcnv2  6225  cores2  6226  co01  6228  cnviin  6252  predres  6305  iota4an  6482  fnopab  6638  mpt0  6642  fnmpti  6643  f1cnvcnv  6747  f1ovi  6822  eliman0  6879  fvco4i  6943  cnvimainrn  7021  fmpti  7066  funiunfv  7204  oprabss  7476  relmptopab  7618  zfun  7691  tfinds2  7816  omon  7830  2nd0  7950  f1stres  7967  f2ndres  7968  cnvoprab  8014  relmpoopab  8046  df1st2  8050  df2nd2  8051  fsplit  8069  frpoins3xpg  8092  frpoins3xp3g  8093  poxp2  8095  poseq  8110  reldmtpos  8186  dftpos4  8197  tpostpos  8198  tpos0  8208  frrlem4  8241  smo0  8300  tfrlem14  8332  tfrlem16  8334  rdgsucg  8364  rdglimg  8366  frfnom  8376  oawordeulem  8491  uniixp  8871  dfdom2  8927  ssdomg  8949  xpcomf1o  9006  sbthlem5  9031  sdom0  9049  limensuci  9093  1sdom2  9160  fiint  9239  fidomdm  9246  residfi  9250  mptfi  9263  fisn  9342  dffi3  9346  ordtypelem6  9440  ordtypelem7  9441  wemaplem2  9464  harwdom  9508  nelaneq  9518  suc11reg  9540  zfinf  9560  axinf2  9561  noinfep  9581  cantnfvalf  9586  cantnflt  9593  cantnf0  9596  cantnf  9614  ttrclco  9639  tz9.1c  9651  tc2  9661  setinds  9670  r111  9699  r1tr2  9701  r1ordg  9702  r1sssuc  9707  r1val1  9710  tz9.13  9715  r1elssi  9729  pwwf  9731  rankopb  9776  rankeq0b  9784  ranksuc  9789  rankmapu  9802  rankxplim3  9805  rankxpsuc  9806  cp  9815  karden  9819  card0  9882  cardlim  9896  cardom  9910  infxpenlem  9935  alephsuc2  10002  alephgeom  10004  unialeph  10023  dfac4  10044  dfacacn  10064  dju1dif  10095  dju1p1e2  10096  infdju1  10112  ackbij1lem13  10153  ackbij2  10164  cf0  10173  cfsuc  10179  cfom  10186  cfslb2n  10190  ominf4  10234  fin23lem17  10260  fin23lem28  10262  fin23lem30  10264  fin23lem31  10265  fin23lem40  10273  isfin1-3  10308  dfacfin7  10321  fin1a2lem6  10327  itunitc1  10342  axcc3  10360  dcomex  10369  axdc2lem  10370  axcclem  10379  zfac  10382  ac3  10384  ackm  10387  axac2  10388  axac  10389  axaci  10390  cardeqv  10391  numth2  10393  numth  10394  dmct  10446  brdom3  10450  fin71ac  10455  cardf  10472  aleph1  10494  cfpwsdom  10507  smobeth  10509  zfcndrep  10537  zfcndpow  10539  zfcndac  10542  gch2  10598  wunex3  10664  tskpr  10693  inar1  10698  rankcf  10700  tskcard  10704  tskuni  10706  grothpw  10749  axgroth4  10755  grothprim  10757  inaprc  10759  dmaddpi  10813  dmmulpi  10814  1lt2pi  10828  addpqf  10867  mulpqf  10869  1lt2nq  10896  supsrlem  11034  ssxr  11214  gtso  11226  subf  11394  negne0i  11468  mulnzcnf  11795  infrenegsup  12137  neg1lt0  12145  nnne0  12191  halflt1  12370  nn0ssz  12523  3halfnz  12583  zeo  12590  numlt  12644  numltc  12645  le9lt10  12646  decle  12653  uzf  12766  xaddf  13151  xsubge0  13188  xmulf  13199  ixxf  13283  ixxssxr  13285  iooval2  13306  ioof  13375  unirnioo  13377  dfioo2  13378  fzval2  13438  fzf  13439  0nelfz1  13471  fz10  13473  fzpreddisj  13501  4fvwrd4  13576  fzof  13584  fzo0  13611  fldiv4p1lem1div2  13767  fldiv4lem1div2  13769  om2uzoi  13890  faclbnd4lem1  14228  hashkf  14267  hashgval  14268  hashinf  14270  hashresfn  14275  hashnn0n0nn  14326  hashge3el3dif  14422  hash3tpde  14428  rev0  14699  s2dm  14825  f1oun2prg  14852  trclublem  14930  sqrt2gt1lt2  15209  limsupgord  15407  fclim  15488  fsumrelem  15742  ackbijnn  15763  incexclem  15771  incexc  15772  arisum2  15796  georeclim  15807  geoisumr  15813  0.999...  15816  risefall0lem  15961  ege2le3  16025  sin0  16086  ef01bndlem  16121  cos2bnd  16125  cos01gt0  16128  sincos2sgn  16131  sin4lt0  16132  rpnnen2lem3  16153  rpnnen2lem9  16159  rexpen  16165  cnso  16184  dvdslelem  16248  divalglem1  16333  divalglem5  16336  divalglem6  16337  divalglem10  16341  flodddiv4  16354  0bits  16378  sadcf  16392  sadcadd  16397  bitsshft  16414  smupf  16417  gcdf  16451  eucalgf  16522  2prm  16631  dfphi2  16713  pockthi  16847  prmrec  16862  vdwapf  16912  vdwlem6  16926  karatsuba  17023  1259lem5  17074  2503lem3  17078  4001lem4  17083  structcnvcnv  17092  structfn  17095  strleun  17096  imasvscafn  17470  xpsff1o  17500  xrge0base  17540  wunnat  17895  dfinito3  17941  dftermo3  17942  eldmcoa  18001  coapm  18007  catcfuccl  18054  catcxpccl  18142  yonedainv  18216  chnub  18557  smndex1bas  18843  smndex1n0mnd  18849  grpinvfvi  18924  mulgfvi  19015  ressmulgnnd  19020  symgsssg  19408  symgfisg  19409  psgnunilem5  19435  sylow3lem2  19569  oppglsm  19583  efgmf  19654  efgval  19658  efgsf  19670  0frgp  19720  dmdprd  19941  dprdval  19946  invrfval  20337  drngui  20680  rmodislmod  20893  lssintcl  20927  cnfldadd  21327  cnfldmul  21329  cnfldfunALT  21336  dfcnfldOLD  21337  cnfldfunALTOLD  21349  cnfld0  21359  cnfld1  21360  cnfld1OLD  21361  cnfldsub  21364  xrsds  21376  pzriprnglem4  21451  pzriprnglem9  21456  pzriprnglem14  21461  psgnghm  21547  zrhpsgnmhm  21551  ocv1  21646  dsmmbas2  21704  mplsubrglem  21971  opsrtoslem2  22023  evl1maprhm  22335  mdetralt  22564  maducoeval2  22596  eltpsi  22900  unitg  22923  fctop  22960  cctop  22962  ppttop  22963  epttop  22965  leordtvallem1  23166  leordtvallem2  23167  iccordt  23170  iscnp2  23195  discmp  23354  conncompcld  23390  1stcrestlem  23408  2ndcdisj  23412  topnlly  23447  disllycmp  23454  dis1stc  23455  txuni2  23521  xkotf  23541  dfac14lem  23573  prdstps  23585  txindis  23590  tx1stc  23606  xkohaus  23609  xkoptsub  23610  cnmpt1st  23624  cnmpt2nd  23625  ptcmpfi  23769  trfil1  23842  fin1aufil  23888  tgpconncompeqg  24068  tgpconncomp  24069  trust  24185  met1stc  24477  dscmet  24528  retopon  24719  cnfldtopon  24738  xrsxmet  24766  xrsmopn  24769  iimulcn  24902  iimulcnOLD  24903  icopnfhmeo  24909  iccpnfhmeo  24911  xrhmeo  24912  cnheiborlem  24921  lebnumii  24933  ishtpy  24939  htpycc  24947  pco1  24983  pcohtpylem  24987  pcopt  24990  pcopt2  24991  pcoass  24992  pcorevlem  24994  rrxcph  25360  rrx0el  25366  ovoliunlem3  25473  ovolicc1  25485  ovolicc2  25491  volf  25498  ioorf  25542  dyadf  25560  dyadmbl  25569  vitalilem5  25581  vitali  25582  mbfimaopnlem  25624  mbflimsup  25635  0plef  25641  i1fima  25647  i1fima2  25648  i1fd  25650  itg1ge0  25655  itg10  25657  i1f1lem  25658  i1fadd  25664  i1fmul  25665  i1fmulc  25672  mbfi1fseqlem5  25688  itg2addlem  25727  reldv  25839  dvbsss  25871  dvef  25952  lhop1lem  25986  deg1fvi  26058  plypf1  26185  coeeulem  26197  coeeu  26198  vieta1lem2  26287  aannenlem3  26306  aalioulem3  26310  dvradcnv  26398  pserulm  26399  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  26726  logblog  26770  angpined  26808  1cubr  26820  asinsin  26870  asin1  26872  reasinsin  26874  atan0  26886  atanbnd  26904  atan1  26906  log2cnv  26922  log2ub  26927  log2le1  26928  birthday  26932  amgmlem  26968  emcllem5  26978  emgt0  26985  harmonicbnd3  26986  ftalem3  27053  basellem4  27062  sgmf  27123  ppi1  27142  cht1  27143  vma1  27144  ppiltx  27155  sqff1o  27160  ppiublem1  27181  ppiublem2  27182  ppiub  27183  chtub  27191  dchreq  27237  bposlem7  27269  bposlem8  27270  bposlem9  27271  lgsdir2lem2  27305  lgsdir2lem3  27306  chebbnd1  27451  chto1ub  27455  chpo1ubb  27460  pntibndlem1  27568  nosgnn0  27638  ltssolem1  27655  bdayfo  27657  nolt02o  27675  nogt01o  27676  noetasuplem4  27716  noetainflem4  27720  cutbdaybnd2lim  27805  madeun  27892  cutsfo  27913  addsproplem2  27978  addsproplem7  27983  addsprop  27984  negsprop  28043  subsf  28072  mulsproplem13  28136  mulsproplem14  28137  mulsprop  28138  oniso  28279  n0cut  28342  bdayn0sf1o  28378  twocut  28431  bdaypw2n0bndlem  28471  bdayfinbndlem1  28475  0reno  28504  tgldimor  28586  tglnfn  28631  axlowdimlem4  29030  axlowdimlem16  29042  axlowdim  29046  upgrfi  29176  lfgrnloop  29210  lfuhgr1v0e  29339  usgrexmplef  29344  usgrres  29393  vdegp1bi  29623  vtxdginducedm1lem2  29626  dfpth2  29814  pthdlem2  29853  wpthswwlks2on  30049  0ewlk  30201  0pth  30212  konigsbergiedgw  30335  konigsberglem1  30339  konigsberglem2  30340  konigsberglem3  30341  konigsberglem4  30342  konigsberglem5  30343  ex-dif  30510  ex-un  30511  ex-in  30512  ex-fl  30534  avril1  30550  9p10ne21fool  30558  n0lplig  30570  cnidOLD  30669  cnnvm  30769  ipasslem8  30924  ipasslem10  30926  hvsubf  31102  normlem1  31197  normlem6  31202  normlem7  31203  norm-ii-i  31224  norm3adifii  31235  hilid  31248  hlimf  31324  hhssabloi  31349  hhssnv  31351  hhshsslem1  31354  shincli  31449  shsval2i  31474  shs0i  31536  chj0i  31542  chm1i  31543  chincli  31547  chdmm1i  31564  shjshsi  31579  chsup0  31635  h1de2bi  31641  spansnpji  31665  cmcmlem  31678  cmcmii  31684  cmcm2ii  31685  cmcm3ii  31686  pjidmi  31760  pjssmii  31768  pj0i  31780  pjocini  31785  mayetes3i  31816  df0op2  31839  hoaddcomi  31859  hoaddassi  31863  hocadddiri  31866  hocsubdiri  31867  hoaddridi  31873  ho0coi  31875  hoid1i  31876  hoid1ri  31877  hodseqi  31881  honegsubi  31883  adj1o  31981  hoddii  32076  lnopunilem1  32097  lnopunilem2  32098  nmcopexi  32114  nmcopex  32116  nmcoplb  32117  nmcfnexi  32138  nmcfnex  32140  nmcfnlb  32141  adjbd1o  32172  adjcoi  32187  nmopcoadji  32188  opsqrlem6  32232  pjsdii  32242  pjddii  32243  pjidmcoi  32264  pjtoi  32266  pjin1i  32279  pjclem1  32282  stji1i  32329  reuxfrdf  32576  iuninc  32646  fnresin  32713  rinvf1o  32719  suppss2f  32727  xppreima  32734  ofoprabco  32753  partfun2  32765  fressupp  32777  supppreima  32780  fsupprnfi  32781  gtiso  32790  df1stres  32793  df2ndres  32794  snct  32801  padct  32807  fsuppcurry1  32813  fsuppcurry2  32814  ffsrn  32817  fpwrelmapffs  32823  fzodif1  32882  nnindf  32910  nn0min  32911  dp2lt  32976  dp2ltsuc  32977  dp2ltc  32978  dplti  32996  dpmul  33004  dpmul4  33005  ressplusf  33055  xrsclat  33103  xrge00  33106  xrnarchi  33277  elrgspnlem2  33336  1fldgenq  33415  xrge0slmod  33440  zringfrac  33646  esplyind  33751  ply1degltdimlem  33799  ccfldsrarelvec  33848  ccfldextdgrr  33849  locfinreflem  34017  locfinref  34018  unicls  34080  sqsscirc1  34085  mhmhmeotmd  34104  raddcn  34106  xrge0iifiso  34112  xrge0iifhmeo  34113  lmxrge0  34129  cnzh  34145  rezh  34146  qqh0  34161  qqh1  34162  qqhre  34197  rrhre  34198  esumnul  34225  esum0  34226  esumsnf  34241  esumpfinvallem  34251  esumpfinvalf  34253  esumpcvgval  34255  esumcvgsum  34265  esumsup  34266  esumcvgre  34268  sigaclfu2  34298  dmsigagen  34321  ddemeas  34413  mbfmvolf  34443  br2base  34446  omssubadd  34477  sibfof  34517  sitg0  34523  eulerpartlemt  34548  eulerpartgbij  34549  0rrv  34628  coinfliplem  34656  coinflipprob  34657  coinfliprv  34660  ballotlem2  34666  ballotlem4  34676  ballotlem5  34677  ballotlemi1  34680  ballotlem7  34713  ballotth  34715  signsplypnf  34727  signsply0  34728  signsw0g  34733  signswch  34738  signsvf0  34757  hashreprin  34797  reprfz1  34801  chtvalz  34806  hgt750lemd  34825  hgt750lem  34828  hgt750lem2  34829  bnj1098  34959  bnj1109  34962  bnj1131  34963  bnj1533  35027  bnj151  35052  bnj580  35088  bnj852  35096  bnj864  35097  bnj865  35098  bnj978  35124  bnj1021  35141  bnj907  35142  bnj1093  35155  bnj1145  35168  bnj1172  35176  bnj1174  35178  bnj1176  35180  bnj1186  35182  nfan1c  35248  xoromon  35264  fineqvac  35291  tz9.1regs  35309  onvf1odlem4  35319  onvf1od  35320  subfacf  35388  subfacp1lem1  35392  subfacp1lem5  35397  subfacp1lem6  35398  subfacval3  35402  erdszelem2  35405  kur14lem4  35422  ioosconn  35460  iccllysconn  35463  satfn  35568  fmlaomn0  35603  gonan0  35605  goaln0  35606  elnanelprv  35642  msrfo  35759  mthmpps  35795  problem5  35882  quad3  35883  circum  35887  antnestALT  35907  axextprim  35914  axrepprim  35915  axunprim  35916  axinfprim  35919  axacprim  35920  bcneg1  35949  dfon2lem2  35995  dfon2lem4  35997  axextdfeq  36008  fobigcup  36111  snelsingles  36133  fullfunfnv  36159  fullfunfv  36160  rankaltopb  36192  rank0  36383  rankeq1o  36384  hfuni  36397  in-ax8  36437  fneer  36566  neibastop1  36572  nabi1i  36607  nabi2i  36608  limsucncmpi  36658  knoppcnlem8  36719  knoppcnlem11  36722  cnndvlem1  36756  bj-consensusALT  36800  bj-sbidmOLD  37092  bj-n0i  37193  bj-snsetex  37205  bj-tagss  37222  bj-2upln0  37265  bj-2upln1upl  37266  bj-nuliota  37299  bj-axseprep  37316  bj-0int  37348  bj-elid5  37418  bj-inftyexpitaufo  37451  bj-pinftyccb  37470  bj-minftyccb  37474  bj-pinftynminfty  37476  bj-isrvec  37543  iccioo01  37576  f1omptsnlem  37585  mptsnunlem  37587  topdifinffinlem  37596  relowlpssretop  37613  1oequni2o  37617  pibt2  37666  imadifss  37840  tan2h  37857  poimirlem3  37868  poimirlem9  37874  poimirlem16  37881  poimirlem17  37882  poimirlem18  37883  poimirlem19  37884  poimirlem20  37885  poimirlem22  37887  poimirlem30  37895  mblfinlem1  37902  mblfinlem2  37903  ovoliunnfl  37907  voliunnfl  37909  itg2addnclem  37916  itg2addnclem2  37917  asindmre  37948  areacirclem1  37953  fdc  37990  cntotbnd  38041  heiborlem6  38061  rrnval  38072  reheibor  38084  rngosn3  38169  brcnvrabga  38587  cnvresrn  38593  moantr  38617  inxp2  38620  dfxrn2  38630  dfsucmap3  38708  dfpre4  38725  cnvcosseq  38772  refrelcosslem  38797  1cosscnvxrn  38810  redundss3  38957  refrelsredund3  38963  refrelredund3  38966  disjimeceqim  39049  eqvrel0  39134  eqvrelid  39137  prter2  39251  renegclALT  39333  mapdunirnN  42020  lcmeprodgcdi  42371  3factsumint2  42386  3factsumint3  42387  3factsumint4  42388  3factsumint  42389  lcmineqlem4  42396  3lexlogpow5ineq1  42418  3lexlogpow2ineq1  42422  dvrelogpow2b  42432  aks4d1p1p4  42435  aks4d1p8  42451  aks6d1c1  42480  aks6d1c2p2  42483  aks6d1c4  42488  2ap1caineq  42509  sticksstones1  42510  sticksstones2  42511  aks6d1c7lem2  42545  aks5lem3a  42553  aks5lem6  42556  unitscyglem2  42560  unitscyglem3  42561  sqdeccom12  42653  readvrec2  42725  readvcot  42728  resubf  42745  sn-0ne2  42770  sn-subf  42793  sn-nnne0  42824  sn-0lt1  42839  reneg1lt0  42844  rntrclfvOAI  43042  diophrw  43110  rabren3dioph  43166  pellexlem6  43185  pellex  43186  frmx  43264  frmy  43265  jm2.23  43347  jm2.27dlem3  43362  axac10  43384  pw2f1ocnv  43388  kelac2lem  43415  lmhmlnmsplit  43438  pwfi2f1o  43447  frlmpwfi  43449  insucid  43754  nla0003  43775  ifpbiidcor  43824  sucomisnotcard  43894  alephiso2  43908  alephiso3  43909  cnvnonrel  43938  rnnonrel  43941  resnonrel  43942  cononrel1  43944  cononrel2  43945  fvnonrel  43947  cnvcnvintabd  43950  cnvintabd  43953  rclexi  43965  rtrclex  43967  clcnvlem  43973  cnvrcl0  43975  dmtrcl  43977  rntrcl  43978  dfrtrcl5  43979  iunrelexp0  44052  dmtrclfvRP  44080  rntrclfv  44082  corcltrcl  44089  cotrclrcl  44092  0heALT  44133  frege54cor1a  44214  uneqsn  44375  clsk3nimkb  44390  int-sqdefd  44531  int-sqgeq0d  44536  rr-groth  44649  rr-grothprim  44650  rr-grothshort  44654  seff  44659  expgrowthi  44683  expgrowth  44685  binomcxplemnotnn0  44706  ee233  44869  ax6e2nd  44908  in1  44921  dfvd2ani  44933  dfvd2i  44935  dfvd3i  44942  dfvd3ani  44945  e0bi  45125  uun2221  45162  uun2221p1  45163  uun2221p2  45164  en3lpVD  45194  relopabVD  45250  ax6e2ndVD  45257  ax6e2ndALT  45279  permaxpow  45359  pssnssi  45454  nnf1oxpnn  45548  icof  45571  fnmptif  45617  rn1st  45625  negpilt0  45637  xrgtso  45698  supxrleubrnmptf  45803  xrpnf  45837  rexanuz2nf  45844  ioontr  45865  iccdifioo  45869  iccdifprioo  45870  uzinico2  45915  fsummulc1f  45925  fsumiunss  45929  fnlimfvre2  46029  limsupreuz  46089  limsup10ex  46125  icccncfext  46239  dvcosre  46264  dvsinax  46265  ioodvbdlimc1lem2  46284  ioodvbdlimc2lem  46286  dvmptmulf  46289  dvnmul  46295  dvmptfprodlem  46296  dvnprodlem2  46299  stoweidlem1  46353  stoweidlem26  46378  stoweidlem34  46386  stoweidlem44  46396  stoweid  46415  stirlinglem5  46430  dirkercncflem1  46455  fourierdlem44  46503  fourierdlem56  46514  fourierdlem62  46520  fourierdlem89  46547  fourierdlem91  46549  fourierdlem100  46558  fourierdlem102  46560  fourierdlem103  46561  fourierdlem104  46562  fourierdlem108  46566  fourierdlem112  46570  fourierdlem114  46572  fouriersw  46583  rrndistlt  46642  gsumge0cl  46723  sge0tsms  46732  sge0ltfirpmpt2  46778  ovn0  46918  hoidmv1le  46946  hoidmvle  46952  ovnsubadd2lem  46997  ovolval4lem1  47001  vonioolem2  47033  smflimlem3  47125  nsssmfmbf  47131  chnerlem1  47234  nthrucw  47238  sinnpoly  47245  axorbtnotaiffb  47257  axorbciffatcxorb  47259  abnotbtaxb  47269  euabsneu  47382  ceilhalf1  47688  sprval  47833  fmtnoinf  47890  1nevenALTV  48045  nfermltl8rev  48096  nfermltl2rev  48097  nnsum3primes4  48142  tgblthelfgott  48169  tgoldbachlt  48170  cycl3grtri  48301  isubgr3stgrlem3  48322  usgrexmpl1lem  48375  usgrexmpl2lem  48380  usgrexmpl2trifr  48391  gpgprismgr4cycllem7  48455  ldepslinc  48863  ackval42  49050  rrx2plordso  49078  vsn  49165  dmtposss  49229  sepfsepc  49281  basresposfo  49331  rescofuf  49446  oppff1  49501  idfth  49511  idsubc  49513  fuco2eld2  49667  fuco22a  49703  setc1onsubc  49955  alimp-no-surprise  50134  aacllem  50154  amgmwlem  50155  amgmlemALT  50156