Theorem mpbid 147

Description: A deduction from a biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
mpbid.min	⊢ (𝜑 → 𝜓)
mpbid.maj	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
mpbid	⊢ (𝜑 → 𝜒)

Proof of Theorem mpbid

Step	Hyp	Ref	Expression
1		mpbid.min	. 2 ⊢ (𝜑 → 𝜓)
2		mpbid.maj	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	2	biimpd 144	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 3	mpd 13	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpbii  148  annimdc  945  mpbi2and  951  bilukdc  1440  equs5or  1878  eqtrd  2264  eleqtrd  2310  neeqtrd  2430  3netr3d  2434  rexlimd2  2648  raleqtrdv  2738  rexeqtrdv  2739  ceqsalt  2829  vtoclgft  2854  vtoclegft  2878  elrab3t  2961  eueq2dc  2979  sbceq1dd  3037  csbiedf  3168  sseqtrd  3265  3sstr3d  3271  ifbothdadc  3639  snssd  3818  dfnfc2  3911  breqdi  4103  breqtrd  4114  3brtr3d  4119  csbexga  4217  reuhypd  4568  reg2exmidlema  4632  elirr  4639  en2lp  4652  onsucuni2  4662  finds  4698  iota4  5306  iota4an  5307  funimaexglem  5413  fneu  5436  fco2  5501  fssres2  5514  fresin  5515  feu  5519  f1orescnv  5599  resdif  5605  funcocnv2  5608  f1oprg  5629  fvelrnb  5693  fimacnv  5776  f1oresrab  5812  fsn2  5821  xpsng  5823  funopsn  5830  fnressn  5840  fsnunf  5854  foeqcnvco  5931  isores1  5955  isoini2  5960  riota5f  5998  riotass2  6000  riotass  6001  ovmpodxf  6147  uchoice  6300  elopabi  6360  cnvf1o  6390  smores3  6459  tfrlemisucaccv  6491  tfr1onlemsucaccv  6507  tfrcllemsucaccv  6520  rdgon  6552  frecabcl  6565  frecsuclem  6572  nnsucsssuc  6660  nnsucuniel  6663  erref  6722  iserd  6728  swoer  6730  swoord1  6731  swoord2  6732  erth  6748  erthi  6750  eroveu  6795  pmresg  6845  mapsn  6859  fndmeng  6985  xpen  7031  phplem4  7041  phplem4on  7054  fidifsnen  7057  dif1en  7068  dif1enen  7069  fisbth  7072  diffisn  7082  ac6sfi  7087  fidcen  7088  fimax2gtri  7091  en2eqpr  7099  unsnfidcex  7112  unsnfidcel  7113  prfidceq  7120  fiintim  7123  fidcenumlemrks  7152  elfi2  7171  elfir  7172  fiuni  7177  fifo  7179  eqsupti  7195  supisoti  7209  ordiso2  7234  casef  7287  difinfsnlem  7298  ctmlemr  7307  ctssdccl  7310  enumct  7314  nninfninc  7322  nnnninfeq  7327  nnnninfeq2  7328  enomnilem  7337  exmidomni  7341  fodjum  7345  fodjuomnilemres  7347  mkvprop  7357  enmkvlem  7360  enwomnilem  7368  nninfdcinf  7370  nninfwlpoimlemdc  7376  nninfinfwlpolem  7377  pr1or2  7399  acfun  7422  2omotaplemap  7476  exmidmotap  7480  ccfunen  7483  cc2lem  7485  dfplpq2  7574  ltanqi  7622  ltmnqi  7623  ltaddnq  7627  subhalfnqq  7634  ltbtwnnqq  7635  archnqq  7637  prarloclemarch2  7639  enq0sym  7652  enq0ref  7653  enq0tr  7654  nqnq0pi  7658  nnnq0lem1  7666  distrnq0  7679  prarloclemlt  7713  prarloclemn  7719  prarloclemcalc  7722  genplt2i  7730  addnqprllem  7747  addnqprulem  7748  addlocprlemgt  7754  appdivnq  7783  prmuloc2  7787  ltexprlemopl  7821  ltexprlemopu  7823  ltexprlemru  7832  prplnqu  7840  cauappcvgprlemopl  7866  cauappcvgprlemlol  7867  cauappcvgprlemladdfu  7874  cauappcvgprlemladdrl  7877  cauappcvgprlem1  7879  archrecnq  7883  archrecpr  7884  caucvgprlemk  7885  caucvgprlemnbj  7887  caucvgprlemm  7888  caucvgprlemopl  7889  caucvgprlemlol  7890  caucvgprlemladdfu  7897  caucvgprlemladdrl  7898  caucvgprlem1  7899  caucvgprprlemk  7903  caucvgprprlemnkeqj  7910  caucvgprprlemnbj  7913  caucvgprprlemml  7914  caucvgprprlemmu  7915  caucvgprprlemopl  7917  caucvgprprlemlol  7918  caucvgprprlemopu  7919  caucvgprprlemexbt  7926  caucvgprprlemexb  7927  caucvgprprlem1  7929  caucvgprprlem2  7930  suplocexprlemru  7939  suplocexprlemdisj  7940  suplocexprlemloc  7941  suplocexprlemub  7943  suplocexprlemlub  7944  prsrlem1  7962  addgt0sr  7995  srpospr  8003  prsrriota  8008  caucvgsrlemgt1  8015  caucvgsrlemoffgt1  8019  caucvgsr  8022  mappsrprg  8024  suplocsrlemb  8026  suplocsrlempr  8027  suplocsrlem  8028  recriota  8110  axsuploc  8252  lelttr  8268  ltletr  8269  ltnsymd  8299  lensymd  8301  cnegexlem3  8356  cnegex2  8358  addcanad  8365  addcan2ad  8366  negcon1ad  8485  negne0d  8488  negrebd  8489  subeq0d  8498  subne0ad  8501  neg11d  8502  subcand  8531  subcan2d  8532  ltadd2  8599  ltadd2dd  8602  add20  8654  ltnegcon1d  8705  ltnegcon2d  8706  lenegcon1d  8707  lenegcon2d  8708  subled  8728  lesubd  8729  ltsub23d  8730  ltsub13d  8731  ltadd1dd  8736  ltsub1dd  8737  ltsub2dd  8738  leadd1dd  8739  leadd2dd  8740  lesub1dd  8741  lesub2dd  8742  recexre  8758  apreap  8767  ltmul1a  8771  reapmul1  8775  cru  8782  apreim  8783  mulge0  8799  leltap  8805  negap0d  8811  ltleap  8812  ltapd  8818  ap0gt0  8820  ap0gt0d  8821  mulcanapad  8843  mulcanap2ad  8844  eqnegad  8914  diveqap0d  8977  diveqap1d  8978  divap1d  8981  rec11apd  8991  div11apd  9011  div2subap  9017  recgt0  9030  prodgt0  9032  lemul1a  9038  lemulge12  9047  lt2msq1  9065  lediv12a  9074  recreclt  9080  nn1suc  9162  nnnlt1  9169  nn2ge  9176  nn1gt1  9177  nnrecl  9400  nn0nlt0  9428  elnn0z  9492  nnnle0  9528  nn0negleid  9548  elz2  9551  nn0n0n1ge2b  9559  nnm1ge0  9566  nn0ge0div  9567  zextle  9571  suprzclex  9578  nn0ind-raph  9597  zindd  9598  uzneg  9775  eluzadd  9785  eluzsub  9786  uzm1  9787  uz3m2nn  9807  supminfex  9831  infregelbex  9832  nn01to3  9851  irrmulap  9882  ltrec1d  9952  lerec2d  9953  ledivdivd  9957  divge1  9958  ltmul1dd  9987  ltmul2dd  9988  ltdiv1dd  9989  lediv1dd  9990  ltdiv23d  9992  lediv23d  9993  nn0ledivnn  10002  addlelt  10003  xrlelttr  10041  xrltletr  10042  xaddass2  10105  xltadd1  10111  xlt2add  10115  ixxdisj  10138  icoshftf1o  10226  icodisj  10227  lincmb01cmp  10238  iccf1o  10239  uzsubsubfz  10282  fzdisj  10287  fzopth  10296  fznatpl1  10311  fzsuc2  10314  fzp1disj  10315  fzrev2i  10321  uzdisj  10328  fseq1p1m1  10329  fzm1  10335  fzneuz  10336  fzp1nel  10339  fzrevral  10340  fznn0sub2  10363  fz0fzdiffz0  10365  difelfzle  10369  difelfznle  10370  nn0disj  10373  fzonnsub  10406  fzodisj  10415  fzouzdisj  10417  fzoun  10418  eluzgtdifelfzo  10443  ubmelfzo  10446  fzonn0p1p1  10459  ubmelm1fzo  10472  fzostep1  10484  exfzdc  10487  subfzo0  10489  zsupcllemstep  10490  infssuzex  10494  zsupssdc  10499  qtri3or  10501  exbtwnzlemex  10510  rebtwn2z  10515  qbtwnrelemcalc  10516  qbtwnre  10517  qavgle  10519  apbtwnz  10535  flid  10545  flqwordi  10549  flqmulnn0  10560  flhalf  10563  flltdivnn0lt  10565  fldiv4p1lem1div2  10566  intfracq  10583  flqdiv  10584  flqpmodeq  10590  modqmulnn  10605  mulqaddmodid  10627  modqmuladdim  10630  modqmuladdnn0  10631  m1modge3gt1  10634  q2submod  10648  modaddmodup  10650  modqsubdir  10656  modqeqmodmin  10657  modfzo0difsn  10658  uzennn  10699  uzsinds  10707  monoord2  10749  ser3mono  10750  iseqf1olemqcl  10762  iseqf1olemnab  10764  iseqf1olemab  10765  iseqf1olemqf1o  10769  iseqf1olemqk  10770  seq3f1olemqsumkj  10774  seq3f1olemqsumk  10775  seq3f1olemqsum  10776  seq3f1olemp  10778  seqf1oglem1  10782  seqf1oglem2  10783  ser3le  10800  exp3val  10804  expnegap0  10810  expgt1  10840  ltexp2a  10854  le2sq2  10878  nnlesq  10906  qsqeqor  10913  bernneq  10923  expnbnd  10926  expnlbnd  10927  expnlbnd2  10928  expeq0d  10932  sq11d  10969  nn0ltexp2  10972  expcand  10980  nn0opthd  10985  facdiv  11001  faclbnd6  11007  facubnd  11008  facavg  11009  bcval4  11015  bcp1nk  11025  bcval5  11026  bcpasc  11029  hashennnuni  11042  isfinite4im  11055  hashnncl  11058  hashunlem  11068  fiprsshashgt1  11082  hashfzp1  11089  zfz1isolemiso  11104  seq3coll  11107  hash2en  11108  hashtpgim  11110  hashtpglem  11111  iswrdiz  11124  wrdffz  11138  ffz0iswrdnn0  11144  ccatval21sw  11186  ccatass  11189  ccatalpha  11194  swrdf  11240  swrdlend  11243  ccatswrd  11255  swrdccat2  11256  pfxsuffeqwrdeq  11283  ccatpfx  11286  ccats1pfxeq  11299  cats1un  11306  wrdind  11307  wrd2ind  11308  pfxccatin12  11318  swrdccat  11320  s2dmg  11375  seq3shft  11403  cjth  11411  cjdivap  11474  cjne0d  11512  cjap0d  11513  cvg1nlemcxze  11547  cvg1nlemcau  11549  cvg1nlemres  11550  recvguniq  11560  resqrexlemover  11575  resqrexlemdecn  11577  resqrexlemlo  11578  resqrexlemcalc2  11580  resqrexlemcalc3  11581  resqrexlemnmsq  11582  resqrexlemnm  11583  resqrexlemcvg  11584  resqrexlemglsq  11587  resqrexlemga  11588  leabs  11639  absrele  11648  nn0abscl  11650  ltabs  11652  abslt  11653  absle  11654  abstri  11669  amgm2  11683  sqr11d  11738  abs00d  11751  maxabsle  11769  maxabslemlub  11772  maxleastlt  11780  maxltsup  11783  2zsupmax  11791  minmax  11795  2zinfmin  11808  xrmaxleim  11809  xrmaxiflemlub  11813  xrmaxiflemcom  11814  xrmaxiflemval  11815  xrmaxleastlt  11821  xrmaxltsup  11823  xrmaxaddlem  11825  xrmaxadd  11826  xrminmax  11830  xrmin1inf  11832  xrmin2inf  11833  xrmineqinf  11834  climi  11852  reccn2ap  11878  climge0  11890  climle  11899  climserle  11910  climrecvg1n  11913  fz1f1o  11940  summodclem3  11946  summodclem2a  11947  summodc  11949  fisumss  11958  fsum0diaglem  12006  mptfzshft  12008  fsumrev  12009  fisum0diag2  12013  fsumlessfi  12026  fsumle  12029  fsumlt  12030  isumsplit  12057  isumrpcl  12060  expcnvap0  12068  geosergap  12072  pwm1geoserap1  12074  absgtap  12076  geolim  12077  geolim2  12078  georeclim  12079  geoisumr  12084  geoisum1c  12086  cvgratnnlembern  12089  cvgratnnlemseq  12092  cvgratnnlemsumlt  12094  cvgratnnlemfm  12095  cvgratnnlemrate  12096  cvgratnn  12097  cvgratz  12098  mertenslemub  12100  mertenslemi1  12101  mertenslem2  12102  mertensabs  12103  prodmodclem2a  12142  prodmodc  12144  zproddc  12145  fprodntrivap  12150  fprodf1o  12154  fprodssdc  12156  fprodsplitdc  12162  fprodrev  12185  fprodmodd  12207  efcllemp  12224  ege2le3  12237  eftlcvg  12253  eftlub  12256  efltim  12264  eflegeo  12267  tanaddap  12305  sinbnd  12318  cosbnd  12319  sin01bnd  12323  cos01bnd  12324  sinltxirr  12327  sin01gt0  12328  cos01gt0  12329  cos12dec  12334  eirraplem  12343  zdvdsdc  12378  dvdstr  12394  dvdsadd2b  12406  fsumdvds  12408  dvdslelemd  12409  divconjdvds  12415  alzdvds  12420  dvdsext  12421  fzm1ndvds  12422  fzo0dvdseq  12423  3dvds  12430  zeo3  12434  even2n  12440  mod2eq1n2dvds  12445  nn0ehalf  12469  nnehalf  12470  nno  12472  nn0oddm1d2  12475  divalglemnqt  12486  divalglemex  12488  divalglemeuneg  12489  divalg2  12492  divalgmod  12493  flodddiv4t2lthalf  12505  bitsfzolem  12520  bitsfzo  12521  bitsmod  12522  bitsfi  12523  bitscmp  12524  bitsinv1lem  12527  bitsinv1  12528  dvdsbnd  12532  gcdsupex  12533  gcdsupcl  12534  gcddvds  12539  divgcdz  12547  divgcdnn  12551  gcd0id  12555  gcdneg  12558  gcd1  12563  dvdsgcdidd  12570  bezoutlemnewy  12572  bezoutlemstep  12573  bezoutlemmo  12582  bezoutlemsup  12585  dfgcd3  12586  bezout  12587  dfgcd2  12590  mulgcd  12592  sqgcd  12605  dvdssqlem  12606  bezoutr1  12609  uzwodc  12613  nninfctlemfo  12616  lcmval  12640  lcmcllem  12644  dvdslcm  12646  lcmgcdlem  12654  lcmdvds  12656  lcmgcdeq  12660  ncoprmgcdne1b  12666  mulgcddvds  12671  rpmulgcd2  12672  qredeu  12674  rpdvds  12676  prmind2  12697  nprm  12700  dvdsnprmd  12702  isprm5lem  12718  isprm5  12719  divgcdodd  12720  isprm6  12724  prmexpb  12728  pw2dvds  12743  pw2dvdseulemle  12744  oddpwdclemdc  12750  sqne2sq  12754  znege1  12755  sqrt2irraplemnn  12756  divnumden  12773  divdenle  12774  qden1elz  12782  nn0sqrtelqelz  12783  hashdvds  12798  crth  12801  phimullem  12802  eulerthlemfi  12805  eulerthlemh  12808  eulerthlemth  12809  eulerth  12810  prmdiv  12812  prmdiveq  12813  hashgcdlem  12815  dvdsfi  12816  phisum  12818  odzcllem  12820  odzdvds  12823  odzphi  12824  oddprm  12837  pythagtriplem3  12845  pythagtriplem4  12846  pythagtriplem10  12847  pythagtriplem11  12852  pythagtriplem13  12854  pythagtriplem19  12860  pcprendvds  12868  pcprendvds2  12869  pcpre1  12870  pcpremul  12871  pceulem  12872  pceu  12873  pczpre  12875  pcmul  12879  pcdiv  12880  pcqmul  12881  pcqdiv  12885  pcexp  12887  pcidlem  12901  pcneg  12903  pcdvdstr  12905  pcgcd1  12906  pc2dvds  12908  dvdsprmpweq  12913  dvdsprmpweqle  12915  pcaddlem  12917  pcadd  12918  pcadd2  12919  pcmpt  12921  fldivp1  12926  pcfaclem  12927  pcfac  12928  pcbc  12929  qexpz  12930  oddprmdvds  12932  pockthlem  12934  pockthg  12935  infpnlem2  12938  1arith  12945  4sqlem9  12964  4sqlem10  12965  4sqlem11  12979  4sqlem12  12980  4sqlem13m  12981  4sqlem14  12982  4sqlem16  12984  oddennn  13018  ennnfonelemk  13026  ennnfonelemkh  13038  ennnfonelemhf1o  13039  ennnfonelemex  13040  ennnfonelemhom  13041  ennnfonelemrnh  13042  ennnfonelemen  13047  ennnfonelemim  13050  ctinfomlemom  13053  ctiunctlemf  13064  ssnnctlemct  13072  nninfdclemcl  13074  nninfdclemp1  13076  nninfdclemlt  13077  unbendc  13080  prdsbascl  13377  pwselbas  13382  mgmb1mgm1  13456  mgm1  13458  mgmidsssn0  13472  gsumfzval  13479  gsumress  13483  gsum0g  13484  gsumval2  13485  sgrp1  13499  sgrpidmndm  13508  ismndd  13525  prds0g  13537  mhmpropd  13554  resmhm  13575  resmhm2b  13577  gsumwsubmcl  13584  gsumwmhm  13586  isgrpd2e  13608  grpidd2  13629  isgrpinv  13642  grpinvinv  13655  grpidssd  13664  grpinvssd  13665  mulgval  13714  mulgfng  13716  mulgnegnn  13724  subg0  13772  issubg4m  13785  nsgconj  13798  1nsgtrivd  13811  eqgen  13819  eqgcpbl  13820  qus0  13827  ghmid  13841  resghm  13852  ghmnsgpreima  13861  kerf1ghm  13866  conjsubgen  13870  conjnmz  13871  imasabl  13928  gsumsplit0  13938  rnglz  13964  rngrz  13965  qusrng  13977  issrgid  14000  srg1zr  14006  ringcl  14032  isringid  14044  ringcom  14050  ringpropd  14057  ringlz  14062  ringrz  14063  ring1  14078  opprrng  14096  opprring  14098  dvdsrcld  14117  unitcld  14128  unitmulcl  14133  unitgrp  14136  unitnegcl  14150  rhmmul  14184  isrhm2d  14185  rhmdvdsr  14195  rhmopp  14196  elrhmunit  14197  rhmunitinv  14198  subrgugrp  14260  aprsym  14304  islmodd  14313  lmod0vs  14341  lmodfopne  14346  lmodcom  14353  lssclg  14384  lspsnel5a  14430  lspsneq0b  14447  lsslsp  14449  sraring  14469  sralmod  14470  rspssp  14514  rnglidlmsgrp  14517  2idlcpblrng  14543  gsumfzfsumlem0  14606  zncrng  14665  znzrh2  14666  znzrhfo  14668  znf1o  14671  znfi  14675  znhash  14676  znidom  14677  znidomb  14678  znunit  14679  znrrg  14680  psrbaglesuppg  14692  psrelbas  14695  psrelbasfi  14696  psrgrp  14705  psr0  14706  psr1clfi  14708  mplsubgfilemcl  14719  mplsubgfileminv  14720  ntridm  14856  ntrtop  14858  ntrcls0  14861  ntr0  14864  isopn3i  14865  neiss2  14872  opnneiss  14888  topssnei  14892  cnpf2  14937  icnpimaex  14941  lmcvg  14947  iscnp4  14948  cncnp  14960  cnptopresti  14968  lmfss  14974  lmtopcnp  14980  hmeores  15045  bldisj  15131  xblss2ps  15134  xblss2  15135  blhalf  15138  blssps  15157  blss  15158  ssblex  15161  blpnfctr  15169  xmetresbl  15170  mopni2  15213  bdxmet  15231  bdbl  15233  xmetxpbl  15238  metcnpi  15245  metcnpi2  15246  tgioo  15284  rescncf  15311  mulcncflem  15337  cnopnap  15341  dedekindeulemuub  15347  dedekindeulemloc  15349  dedekindeulemlu  15351  dedekindeu  15353  dedekindicclemuub  15356  dedekindicclemloc  15358  dedekindicclemlu  15360  dedekindicclemicc  15362  dedekindicc  15363  ivthinclemlopn  15366  ivthinclemuopn  15368  ivthdec  15374  ivthreinc  15375  hovergt0  15380  dich0  15382  limcimolemlt  15394  cnplimcim  15397  cnplimclemr  15399  limccnpcntop  15405  limccnp2cntop  15407  limccoap  15408  dvfgg  15418  dvidlemap  15421  dvidrelem  15422  dvidsslem  15423  dvaddxxbr  15431  dvmulxxbr  15432  dvaddxx  15433  dvmulxx  15434  dviaddf  15435  dvimulf  15436  dvcoapbr  15437  dvcjbr  15438  dvcj  15439  dvrecap  15443  dvmptclx  15448  dveflem  15456  elply2  15465  plyf  15467  plyaddlem  15479  plymullem  15480  plycoeid3  15487  plyco  15489  plycj  15491  dvply1  15495  dvply2g  15496  reeff1oleme  15502  eflt  15505  sin0pilem1  15511  pilem3  15513  cosq14gt0  15562  coseq0negpitopi  15566  tangtx  15568  coskpi  15578  cosordlem  15579  cosq34lt1  15580  relogef  15594  logrpap0d  15608  rplogcl  15609  logge0  15610  logdivlti  15611  cxplt3  15650  rpabscxpbnd  15670  dvdsppwf1o  15719  fsumdvdsmul  15721  mersenne  15727  perfect1  15728  perfectlem1  15729  perfectlem2  15730  perfect  15731  lgslem1  15735  lgsval  15739  lgsfvalg  15740  lgsval2lem  15745  lgsvalmod  15754  lgsfcl3  15756  lgsmod  15761  lgsdirprm  15769  lgsdir  15770  lgsdilem2  15771  lgsdi  15772  lgsne0  15773  gausslemma2dlem0i  15792  gausslemma2dlem1a  15793  gausslemma2dlem1f1o  15795  gausslemma2dlem3  15798  gausslemma2dlem4  15799  lgseisenlem1  15805  lgseisenlem2  15806  lgseisenlem3  15807  lgseisenlem4  15808  lgseisen  15809  lgsquadlem1  15812  lgsquadlem2  15813  lgsquadlem3  15814  lgsquad2lem1  15816  lgsquad2lem2  15817  lgsquad3  15819  2lgslem1c  15825  2lgsoddprm  15848  2sqlem3  15852  2sqlem4  15853  2sqlem8  15858  lpvtx  15936  umgrnloopv  15971  umgredgne  16007  ausgrusgrien  16028  uhgr0vusgr  16095  usgr1vr  16105  p1evtxdeqfilem  16168  wlkcompim  16209  wlkvtxedg  16220  upgr2wlkdc  16234  clwwlkccatlem  16257  clwwlknp  16274  clwwlkext2edg  16279  eupth2lem3lem3fi  16327  eulerpathprum  16337  bj-charfunr  16431  pw1ndom3lem  16614  2omap  16620  pw1map  16622  pwf1oexmid  16626  subctctexmid  16627  domomsubct  16628  pw1nct  16630  nnsf  16633  peano4nninf  16634  nninfsellemeq  16642  nnnninfex  16650  cvgcmp2nlemabs  16662  iooref1o  16664  trilpolemisumle  16668  trilpolemeq1  16670  trilpolemlt1  16671  trirec0  16674  apdifflemf  16676  apdifflemr  16677  apdiff  16678  qdiff  16679  iswomninnlem  16680  redcwlpo  16686  redc0  16688  reap0  16689  nconstwlpolemgt0  16695  neapmkvlem  16698  ltlenmkv  16701  supfz  16702  inffz  16703  gfsumval  16707  gsumgfsumlem  16710  gsumgfsum  16711