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  1609  nic-dfim  1669  nic-dfneg  1670  nic-mp  1671  nic-mpALT  1672  tbw-negdf  1699  rb-imdf  1750  nfri  1789  mpgbi  1798  19.35i  1878  nfim1  2200  19.36i  2232  ax6  2382  sbie  2500  datisi  2673  disamis  2674  dimatis  2681  fresison  2682  bamalip  2685  axi12  2699  eqcomi  2738  eqtri  2752  eleqtri  2826  nfnfc  2904  neii  2927  necomi  2979  neeqtri  2997  neli  3031  nrex  3057  rexlimi  3229  eueqi  3671  euxfr2w  3682  euxfr2  3684  reuxfrd  3710  cdeqri  3728  sseqtri  3986  pssn2lp  4057  equncomi  4113  unssi  4144  ssini  4193  unabs  4218  inabs  4219  dfin4  4231  vn0  4298  inindif  4328  difidALT  4330  ab0orv  4336  ab0orvALT  4337  disjdif  4425  difin0  4427  pwundif  4577  snid  4616  rabrsn  4678  iinrab2  5022  symdifv  5038  rintn0  5061  breqtri  5120  axsepgfromrep  5236  bm1.3iiOLD  5244  ax6vsep  5245  notzfaus  5305  zfpow  5308  dtruALT2  5312  dtruALT  5330  reusv2lem4  5343  dtru  5383  el  5384  dtruOLD  5388  op1stb  5418  copsexgw  5437  copsexg  5438  uniop  5462  rn0  5872  dmresi  6007  somincom  6087  cnvimassrndm  6105  cnvcnv  6145  elid  6152  rescnvcnv  6157  cnvcnvres  6158  cocnvcnv2  6211  cores2  6212  co01  6214  cnviin  6238  predres  6291  iota4an  6468  fnopab  6624  mpt0  6628  fnmpti  6629  f1cnvcnv  6733  f1ovi  6807  eliman0  6864  fvco4i  6928  cnvimainrn  7005  fmpti  7050  funiunfv  7188  oprabss  7461  relmptopab  7603  zfun  7676  tfinds2  7804  omon  7818  2nd0  7938  f1stres  7955  f2ndres  7956  cnvoprab  8002  relmpoopab  8034  df1st2  8038  df2nd2  8039  fsplit  8057  frpoins3xpg  8080  frpoins3xp3g  8081  poxp2  8083  poseq  8098  reldmtpos  8174  dftpos4  8185  tpostpos  8186  tpos0  8196  frrlem4  8229  smo0  8288  tfrlem14  8320  tfrlem16  8322  rdgsucg  8352  rdglimg  8354  frfnom  8364  oawordeulem  8479  uniixp  8855  dfdom2  8910  ssdomg  8932  xpcomf1o  8990  sbthlem5  9015  sdom0  9033  limensuci  9077  1sdom2  9147  fiint  9235  fiintOLD  9236  fidomdm  9243  residfi  9247  mptfi  9260  fisn  9336  dffi3  9340  ordtypelem6  9434  ordtypelem7  9435  wemaplem2  9458  harwdom  9502  nelaneq  9512  suc11reg  9534  zfinf  9554  axinf2  9555  noinfep  9575  cantnfvalf  9580  cantnflt  9587  cantnf0  9590  cantnf  9608  ttrclco  9633  tz9.1c  9645  tc2  9657  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  10484  cfpwsdom  10497  smobeth  10499  zfcndrep  10527  zfcndpow  10529  zfcndac  10532  gch2  10588  wunex3  10654  tskpr  10683  inar1  10688  rankcf  10690  tskcard  10694  tskuni  10696  grothpw  10739  axgroth4  10745  grothprim  10747  inaprc  10749  dmaddpi  10803  dmmulpi  10804  1lt2pi  10818  addpqf  10857  mulpqf  10859  1lt2nq  10886  supsrlem  11024  ssxr  11203  gtso  11215  subf  11383  negne0i  11457  mulnzcnf  11784  infrenegsup  12126  neg1lt0  12134  nnne0  12180  halflt1  12359  nn0ssz  12512  3halfnz  12573  zeo  12580  numlt  12634  numltc  12635  le9lt10  12636  decle  12643  uzf  12756  xaddf  13144  xsubge0  13181  xmulf  13192  ixxf  13276  ixxssxr  13278  iooval2  13299  ioof  13368  unirnioo  13370  dfioo2  13371  fzval2  13431  fzf  13432  0nelfz1  13464  fz10  13466  fzpreddisj  13494  4fvwrd4  13569  fzof  13577  fzo0  13604  fldiv4p1lem1div2  13757  fldiv4lem1div2  13759  om2uzoi  13880  faclbnd4lem1  14218  hashkf  14257  hashgval  14258  hashinf  14260  hashresfn  14265  hashnn0n0nn  14316  hashge3el3dif  14412  hash3tpde  14418  rev0  14688  s2dm  14815  f1oun2prg  14842  trclublem  14920  sqrt2gt1lt2  15199  limsupgord  15397  fclim  15478  fsumrelem  15732  ackbijnn  15753  incexclem  15761  incexc  15762  arisum2  15786  georeclim  15797  geoisumr  15803  0.999...  15806  risefall0lem  15951  ege2le3  16015  sin0  16076  ef01bndlem  16111  cos2bnd  16115  cos01gt0  16118  sincos2sgn  16121  sin4lt0  16122  rpnnen2lem3  16143  rpnnen2lem9  16149  rexpen  16155  cnso  16174  dvdslelem  16238  divalglem1  16323  divalglem5  16326  divalglem6  16327  divalglem10  16331  flodddiv4  16344  0bits  16368  sadcf  16382  sadcadd  16387  bitsshft  16404  smupf  16407  gcdf  16441  eucalgf  16512  2prm  16621  dfphi2  16703  pockthi  16837  prmrec  16852  vdwapf  16902  vdwlem6  16916  karatsuba  17013  1259lem5  17064  2503lem3  17068  4001lem4  17073  structcnvcnv  17082  structfn  17085  strleun  17086  imasvscafn  17459  xpsff1o  17489  xrge0base  17529  wunnat  17884  dfinito3  17930  dftermo3  17931  eldmcoa  17990  coapm  17996  catcfuccl  18043  catcxpccl  18131  yonedainv  18205  smndex1bas  18798  smndex1n0mnd  18804  grpinvfvi  18879  mulgfvi  18970  ressmulgnnd  18975  symgsssg  19364  symgfisg  19365  psgnunilem5  19391  sylow3lem2  19525  oppglsm  19539  efgmf  19610  efgval  19614  efgsf  19626  0frgp  19676  dmdprd  19897  dprdval  19902  invrfval  20292  drngui  20638  rmodislmod  20851  lssintcl  20885  cnfldadd  21285  cnfldmul  21287  cnfldfunALT  21294  dfcnfldOLD  21295  cnfldfunALTOLD  21307  cnfld0  21317  cnfld1  21318  cnfld1OLD  21319  cnfldsub  21322  xrsds  21334  pzriprnglem4  21409  pzriprnglem9  21414  pzriprnglem14  21419  psgnghm  21505  zrhpsgnmhm  21509  ocv1  21604  dsmmbas2  21662  mplsubrglem  21929  opsrtoslem2  21979  evl1maprhm  22282  mdetralt  22511  maducoeval2  22543  eltpsi  22847  unitg  22870  fctop  22907  cctop  22909  ppttop  22910  epttop  22912  leordtvallem1  23113  leordtvallem2  23114  iccordt  23117  iscnp2  23142  discmp  23301  conncompcld  23337  1stcrestlem  23355  2ndcdisj  23359  topnlly  23394  disllycmp  23401  dis1stc  23402  txuni2  23468  xkotf  23488  dfac14lem  23520  prdstps  23532  txindis  23537  tx1stc  23553  xkohaus  23556  xkoptsub  23557  cnmpt1st  23571  cnmpt2nd  23572  ptcmpfi  23716  trfil1  23789  fin1aufil  23835  tgpconncompeqg  24015  tgpconncomp  24016  trust  24133  met1stc  24425  dscmet  24476  retopon  24667  cnfldtopon  24686  xrsxmet  24714  xrsmopn  24717  iimulcn  24850  iimulcnOLD  24851  icopnfhmeo  24857  iccpnfhmeo  24859  xrhmeo  24860  cnheiborlem  24869  lebnumii  24881  ishtpy  24887  htpycc  24895  pco1  24931  pcohtpylem  24935  pcopt  24938  pcopt2  24939  pcoass  24940  pcorevlem  24942  rrxcph  25308  rrx0el  25314  ovoliunlem3  25421  ovolicc1  25433  ovolicc2  25439  volf  25446  ioorf  25490  dyadf  25508  dyadmbl  25517  vitalilem5  25529  vitali  25530  mbfimaopnlem  25572  mbflimsup  25583  0plef  25589  i1fima  25595  i1fima2  25596  i1fd  25598  itg1ge0  25603  itg10  25605  i1f1lem  25606  i1fadd  25612  i1fmul  25613  i1fmulc  25620  mbfi1fseqlem5  25636  itg2addlem  25675  reldv  25787  dvbsss  25819  dvef  25900  lhop1lem  25934  deg1fvi  26006  plypf1  26133  coeeulem  26145  coeeu  26146  vieta1lem2  26235  aannenlem3  26254  aalioulem3  26258  dvradcnv  26346  pserulm  26347  pserdvlem2  26354  sinhalfpilem  26388  sincos4thpi  26438  tan4thpiOLD  26440  sincos6thpi  26441  pige3ALT  26445  resinf1o  26461  tanord1  26462  tanregt0  26464  efabl  26475  relogrn  26486  dfrelog  26490  logi  26512  logneg  26513  logltb  26525  logcn  26572  logf1o2  26575  dvlog  26576  efopnlem2  26582  efopn  26583  logccv  26588  dvsqrt  26667  dvcnsqrt  26669  cxpcn3  26674  logblog  26718  angpined  26756  1cubr  26768  asinsin  26818  asin1  26820  reasinsin  26822  atan0  26834  atanbnd  26852  atan1  26854  log2cnv  26870  log2ub  26875  log2le1  26876  birthday  26880  amgmlem  26916  emcllem5  26926  emgt0  26933  harmonicbnd3  26934  ftalem3  27001  basellem4  27010  sgmf  27071  ppi1  27090  cht1  27091  vma1  27092  ppiltx  27103  sqff1o  27108  ppiublem1  27129  ppiublem2  27130  ppiub  27131  chtub  27139  dchreq  27185  bposlem7  27217  bposlem8  27218  bposlem9  27219  lgsdir2lem2  27253  lgsdir2lem3  27254  chebbnd1  27399  chto1ub  27403  chpo1ubb  27408  pntibndlem1  27516  nosgnn0  27586  sltsolem1  27603  bdayfo  27605  nolt02o  27623  nogt01o  27624  noetasuplem4  27664  noetainflem4  27668  scutbdaybnd2lim  27746  madeun  27816  scutfo  27837  addsproplem2  27900  addsproplem7  27905  addsprop  27906  negsprop  27964  subsf  27991  mulsproplem13  28054  mulsproplem14  28055  mulsprop  28056  onsiso  28192  n0scut  28249  bdayn0sf1o  28282  twocut  28333  0reno  28384  tgldimor  28465  tglnfn  28510  axlowdimlem4  28908  axlowdimlem16  28920  axlowdim  28924  upgrfi  29054  lfgrnloop  29088  lfuhgr1v0e  29217  usgrexmplef  29222  usgrres  29271  vdegp1bi  29501  vtxdginducedm1lem2  29504  dfpth2  29692  pthdlem2  29731  wpthswwlks2on  29924  0ewlk  30076  0pth  30087  konigsbergiedgw  30210  konigsberglem1  30214  konigsberglem2  30215  konigsberglem3  30216  konigsberglem4  30217  konigsberglem5  30218  ex-dif  30385  ex-un  30386  ex-in  30387  ex-fl  30409  avril1  30425  9p10ne21fool  30433  n0lplig  30445  cnidOLD  30544  cnnvm  30644  ipasslem8  30799  ipasslem10  30801  hvsubf  30977  normlem1  31072  normlem6  31077  normlem7  31078  norm-ii-i  31099  norm3adifii  31110  hilid  31123  hlimf  31199  hhssabloi  31224  hhssnv  31226  hhshsslem1  31229  shincli  31324  shsval2i  31349  shs0i  31411  chj0i  31417  chm1i  31418  chincli  31422  chdmm1i  31439  shjshsi  31454  chsup0  31510  h1de2bi  31516  spansnpji  31540  cmcmlem  31553  cmcmii  31559  cmcm2ii  31560  cmcm3ii  31561  pjidmi  31635  pjssmii  31643  pj0i  31655  pjocini  31660  mayetes3i  31691  df0op2  31714  hoaddcomi  31734  hoaddassi  31738  hocadddiri  31741  hocsubdiri  31742  hoaddridi  31748  ho0coi  31750  hoid1i  31751  hoid1ri  31752  hodseqi  31756  honegsubi  31758  adj1o  31856  hoddii  31951  lnopunilem1  31972  lnopunilem2  31973  nmcopexi  31989  nmcopex  31991  nmcoplb  31992  nmcfnexi  32013  nmcfnex  32015  nmcfnlb  32016  adjbd1o  32047  adjcoi  32062  nmopcoadji  32063  opsqrlem6  32107  pjsdii  32117  pjddii  32118  pjidmcoi  32139  pjtoi  32141  pjin1i  32154  pjclem1  32157  stji1i  32204  reuxfrdf  32453  iuninc  32522  fnresin  32583  rinvf1o  32587  suppss2f  32595  xppreima  32602  ofoprabco  32621  fressupp  32644  supppreima  32647  fsupprnfi  32648  gtiso  32657  df1stres  32660  df2ndres  32661  snct  32670  padct  32676  fsuppcurry1  32681  fsuppcurry2  32682  ffsrn  32685  fpwrelmapffs  32690  fzodif1  32748  nnindf  32777  nn0min  32778  dp2lt  32838  dp2ltsuc  32839  dp2ltc  32840  dplti  32858  dpmul  32866  dpmul4  32867  ressplusf  32918  chnub  32967  xrsclat  32978  xrge00  32981  xrnarchi  33136  elrgspnlem2  33193  1fldgenq  33271  xrge0slmod  33295  zringfrac  33501  ply1degltdimlem  33594  ccfldsrarelvec  33642  ccfldextdgrr  33643  locfinreflem  33806  locfinref  33807  unicls  33869  sqsscirc1  33874  mhmhmeotmd  33893  raddcn  33895  xrge0iifiso  33901  xrge0iifhmeo  33902  lmxrge0  33918  cnzh  33934  rezh  33935  qqh0  33950  qqh1  33951  qqhre  33986  rrhre  33987  esumnul  34014  esum0  34015  esumsnf  34030  esumpfinvallem  34040  esumpfinvalf  34042  esumpcvgval  34044  esumcvgsum  34054  esumsup  34055  esumcvgre  34057  sigaclfu2  34087  dmsigagen  34110  ddemeas  34202  mbfmvolf  34233  br2base  34236  omssubadd  34267  sibfof  34307  sitg0  34313  eulerpartlemt  34338  eulerpartgbij  34339  0rrv  34418  coinfliplem  34446  coinflipprob  34447  coinfliprv  34450  ballotlem2  34456  ballotlem4  34466  ballotlem5  34467  ballotlemi1  34470  ballotlem7  34503  ballotth  34505  signsplypnf  34517  signsply0  34518  signsw0g  34523  signswch  34528  signsvf0  34547  hashreprin  34587  reprfz1  34591  chtvalz  34596  hgt750lemd  34615  hgt750lem  34618  hgt750lem2  34619  bnj1098  34749  bnj1109  34752  bnj1131  34753  bnj1533  34818  bnj151  34843  bnj580  34879  bnj852  34887  bnj864  34888  bnj865  34889  bnj978  34915  bnj1021  34932  bnj907  34933  bnj1093  34946  bnj1145  34959  bnj1172  34967  bnj1174  34969  bnj1176  34971  bnj1186  34973  nfan1c  35039  tz9.1regs  35066  fineqvac  35071  onvf1odlem4  35078  onvf1od  35079  subfacf  35147  subfacp1lem1  35151  subfacp1lem5  35156  subfacp1lem6  35157  subfacval3  35161  erdszelem2  35164  kur14lem4  35181  ioosconn  35219  iccllysconn  35222  satfn  35327  fmlaomn0  35362  gonan0  35364  goaln0  35365  elnanelprv  35401  msrfo  35518  mthmpps  35554  problem5  35641  quad3  35642  circum  35646  antnestALT  35666  axextprim  35673  axrepprim  35674  axunprim  35675  axinfprim  35678  axacprim  35679  bcneg1  35708  setinds  35751  dfon2lem2  35757  dfon2lem4  35759  axextdfeq  35770  fobigcup  35873  snelsingles  35895  fullfunfnv  35919  fullfunfv  35920  rankaltopb  35952  rank0  36143  rankeq1o  36144  hfuni  36157  in-ax8  36197  fneer  36326  neibastop1  36332  nabi1i  36367  nabi2i  36368  limsucncmpi  36418  knoppcnlem8  36473  knoppcnlem11  36476  cnndvlem1  36510  bj-consensusALT  36552  bj-sbidmOLD  36823  bj-n0i  36924  bj-snsetex  36936  bj-tagss  36953  bj-2upln0  36996  bj-2upln1upl  36997  bj-nuliota  37030  bj-0int  37074  bj-elid5  37142  bj-inftyexpitaufo  37175  bj-pinftyccb  37194  bj-minftyccb  37198  bj-pinftynminfty  37200  bj-isrvec  37267  iccioo01  37300  f1omptsnlem  37309  mptsnunlem  37311  topdifinffinlem  37320  relowlpssretop  37337  1oequni2o  37341  pibt2  37390  imadifss  37574  tan2h  37591  poimirlem3  37602  poimirlem9  37608  poimirlem16  37615  poimirlem17  37616  poimirlem18  37617  poimirlem19  37618  poimirlem20  37619  poimirlem22  37621  poimirlem30  37629  mblfinlem1  37636  mblfinlem2  37637  ovoliunnfl  37641  voliunnfl  37643  itg2addnclem  37650  itg2addnclem2  37651  asindmre  37682  areacirclem1  37687  fdc  37724  cntotbnd  37775  heiborlem6  37795  rrnval  37806  reheibor  37818  rngosn3  37903  brcnvrabga  38309  cnvresrn  38315  moantr  38331  inxp2  38334  dfxrn2  38343  cnvcosseq  38413  refrelcosslem  38438  1cosscnvxrn  38451  redundss3  38604  refrelsredund3  38610  refrelredund3  38613  eqvrel0  38763  eqvrelid  38766  prter2  38859  renegclALT  38941  mapdunirnN  41629  lcmeprodgcdi  41980  3factsumint2  41995  3factsumint3  41996  3factsumint4  41997  3factsumint  41998  lcmineqlem4  42005  3lexlogpow5ineq1  42027  3lexlogpow2ineq1  42031  dvrelogpow2b  42041  aks4d1p1p4  42044  aks4d1p8  42060  aks6d1c1  42089  aks6d1c2p2  42092  aks6d1c4  42097  2ap1caineq  42118  sticksstones1  42119  sticksstones2  42120  aks6d1c7lem2  42154  aks5lem3a  42162  aks5lem6  42165  unitscyglem2  42169  unitscyglem3  42170  sqdeccom12  42262  readvrec2  42334  readvcot  42337  resubf  42354  sn-0ne2  42379  sn-subf  42402  sn-nnne0  42433  sn-0lt1  42448  reneg1lt0  42453  rntrclfvOAI  42664  diophrw  42732  rabren3dioph  42788  pellexlem6  42807  pellex  42808  frmx  42886  frmy  42887  jm2.23  42969  jm2.27dlem3  42984  axac10  43006  pw2f1ocnv  43010  kelac2lem  43037  lmhmlnmsplit  43060  pwfi2f1o  43069  frlmpwfi  43071  insucid  43376  nla0003  43398  ifpbiidcor  43447  sucomisnotcard  43517  alephiso2  43531  alephiso3  43532  cnvnonrel  43561  rnnonrel  43564  resnonrel  43565  cononrel1  43567  cononrel2  43568  fvnonrel  43570  cnvcnvintabd  43573  cnvintabd  43576  rclexi  43588  rtrclex  43590  clcnvlem  43596  cnvrcl0  43598  dmtrcl  43600  rntrcl  43601  dfrtrcl5  43602  iunrelexp0  43675  dmtrclfvRP  43703  rntrclfv  43705  corcltrcl  43712  cotrclrcl  43715  0heALT  43756  frege54cor1a  43837  uneqsn  43998  clsk3nimkb  44013  int-sqdefd  44154  int-sqgeq0d  44159  rr-groth  44272  rr-grothprim  44273  rr-grothshort  44277  seff  44282  expgrowthi  44306  expgrowth  44308  binomcxplemnotnn0  44329  ee233  44493  ax6e2nd  44532  in1  44545  dfvd2ani  44557  dfvd2i  44559  dfvd3i  44566  dfvd3ani  44569  e0bi  44749  uun2221  44786  uun2221p1  44787  uun2221p2  44788  en3lpVD  44818  relopabVD  44874  ax6e2ndVD  44881  ax6e2ndALT  44903  permaxpow  44983  pssnssi  45079  nnf1oxpnn  45173  icof  45197  fnmptif  45243  rn1st  45251  negpilt0  45263  xrgtso  45325  supxrleubrnmptf  45431  xrpnf  45465  rexanuz2nf  45472  ioontr  45493  iccdifioo  45497  iccdifprioo  45498  uzinico2  45543  fsummulc1f  45553  fsumiunss  45557  fnlimfvre2  45659  limsupreuz  45719  limsup10ex  45755  icccncfext  45869  dvcosre  45894  dvsinax  45895  ioodvbdlimc1lem2  45914  ioodvbdlimc2lem  45916  dvmptmulf  45919  dvnmul  45925  dvmptfprodlem  45926  dvnprodlem2  45929  stoweidlem1  45983  stoweidlem26  46008  stoweidlem34  46016  stoweidlem44  46026  stoweid  46045  stirlinglem5  46060  dirkercncflem1  46085  fourierdlem44  46133  fourierdlem56  46144  fourierdlem62  46150  fourierdlem89  46177  fourierdlem91  46179  fourierdlem100  46188  fourierdlem102  46190  fourierdlem103  46191  fourierdlem104  46192  fourierdlem108  46196  fourierdlem112  46200  fourierdlem114  46202  fouriersw  46213  rrndistlt  46272  gsumge0cl  46353  sge0tsms  46362  sge0ltfirpmpt2  46408  ovn0  46548  hoidmv1le  46576  hoidmvle  46582  ovnsubadd2lem  46627  ovolval4lem1  46631  vonioolem2  46663  smflimlem3  46755  nsssmfmbf  46761  sinnpoly  46876  axorbtnotaiffb  46888  axorbciffatcxorb  46890  abnotbtaxb  46900  euabsneu  47013  ceilhalf1  47319  sprval  47464  fmtnoinf  47521  1nevenALTV  47676  nfermltl8rev  47727  nfermltl2rev  47728  nnsum3primes4  47773  tgblthelfgott  47800  tgoldbachlt  47801  cycl3grtri  47932  isubgr3stgrlem3  47953  usgrexmpl1lem  48006  usgrexmpl2lem  48011  usgrexmpl2trifr  48022  gpgprismgr4cycllem7  48086  ldepslinc  48495  ackval42  48682  rrx2plordso  48710  vsn  48797  dmtposss  48861  sepfsepc  48913  basresposfo  48963  rescofuf  49079  oppff1  49134  idfth  49144  idsubc  49146  fuco2eld2  49300  fuco22a  49336  setc1onsubc  49588  alimp-no-surprise  49767  aacllem  49787  amgmwlem  49788  amgmlemALT  49789