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  5822  funopsn  5829  fnressn  5839  fsnunf  5853  foeqcnvco  5930  isores1  5954  isoini2  5959  riota5f  5997  riotass2  5999  riotass  6000  ovmpodxf  6146  uchoice  6299  elopabi  6359  cnvf1o  6389  smores3  6458  tfrlemisucaccv  6490  tfr1onlemsucaccv  6506  tfrcllemsucaccv  6519  rdgon  6551  frecabcl  6564  frecsuclem  6571  nnsucsssuc  6659  nnsucuniel  6662  erref  6721  iserd  6727  swoer  6729  swoord1  6730  swoord2  6731  erth  6747  erthi  6749  eroveu  6794  pmresg  6844  mapsn  6858  fndmeng  6984  xpen  7030  phplem4  7040  phplem4on  7053  fidifsnen  7056  dif1en  7067  dif1enen  7068  fisbth  7071  diffisn  7081  ac6sfi  7086  fidcen  7087  fimax2gtri  7090  en2eqpr  7098  unsnfidcex  7111  unsnfidcel  7112  prfidceq  7119  fiintim  7122  fidcenumlemrks  7151  elfi2  7170  elfir  7171  fiuni  7176  fifo  7178  eqsupti  7194  supisoti  7208  ordiso2  7233  casef  7286  difinfsnlem  7297  ctmlemr  7306  ctssdccl  7309  enumct  7313  nninfninc  7321  nnnninfeq  7326  nnnninfeq2  7327  enomnilem  7336  exmidomni  7340  fodjum  7344  fodjuomnilemres  7346  mkvprop  7356  enmkvlem  7359  enwomnilem  7367  nninfdcinf  7369  nninfwlpoimlemdc  7375  nninfinfwlpolem  7376  pr1or2  7398  acfun  7421  2omotaplemap  7475  exmidmotap  7479  ccfunen  7482  cc2lem  7484  dfplpq2  7573  ltanqi  7621  ltmnqi  7622  ltaddnq  7626  subhalfnqq  7633  ltbtwnnqq  7634  archnqq  7636  prarloclemarch2  7638  enq0sym  7651  enq0ref  7652  enq0tr  7653  nqnq0pi  7657  nnnq0lem1  7665  distrnq0  7678  prarloclemlt  7712  prarloclemn  7718  prarloclemcalc  7721  genplt2i  7729  addnqprllem  7746  addnqprulem  7747  addlocprlemgt  7753  appdivnq  7782  prmuloc2  7786  ltexprlemopl  7820  ltexprlemopu  7822  ltexprlemru  7831  prplnqu  7839  cauappcvgprlemopl  7865  cauappcvgprlemlol  7866  cauappcvgprlemladdfu  7873  cauappcvgprlemladdrl  7876  cauappcvgprlem1  7878  archrecnq  7882  archrecpr  7883  caucvgprlemk  7884  caucvgprlemnbj  7886  caucvgprlemm  7887  caucvgprlemopl  7888  caucvgprlemlol  7889  caucvgprlemladdfu  7896  caucvgprlemladdrl  7897  caucvgprlem1  7898  caucvgprprlemk  7902  caucvgprprlemnkeqj  7909  caucvgprprlemnbj  7912  caucvgprprlemml  7913  caucvgprprlemmu  7914  caucvgprprlemopl  7916  caucvgprprlemlol  7917  caucvgprprlemopu  7918  caucvgprprlemexbt  7925  caucvgprprlemexb  7926  caucvgprprlem1  7928  caucvgprprlem2  7929  suplocexprlemru  7938  suplocexprlemdisj  7939  suplocexprlemloc  7940  suplocexprlemub  7942  suplocexprlemlub  7943  prsrlem1  7961  addgt0sr  7994  srpospr  8002  prsrriota  8007  caucvgsrlemgt1  8014  caucvgsrlemoffgt1  8018  caucvgsr  8021  mappsrprg  8023  suplocsrlemb  8025  suplocsrlempr  8026  suplocsrlem  8027  recriota  8109  axsuploc  8251  lelttr  8267  ltletr  8268  ltnsymd  8298  lensymd  8300  cnegexlem3  8355  cnegex2  8357  addcanad  8364  addcan2ad  8365  negcon1ad  8484  negne0d  8487  negrebd  8488  subeq0d  8497  subne0ad  8500  neg11d  8501  subcand  8530  subcan2d  8531  ltadd2  8598  ltadd2dd  8601  add20  8653  ltnegcon1d  8704  ltnegcon2d  8705  lenegcon1d  8706  lenegcon2d  8707  subled  8727  lesubd  8728  ltsub23d  8729  ltsub13d  8730  ltadd1dd  8735  ltsub1dd  8736  ltsub2dd  8737  leadd1dd  8738  leadd2dd  8739  lesub1dd  8740  lesub2dd  8741  recexre  8757  apreap  8766  ltmul1a  8770  reapmul1  8774  cru  8781  apreim  8782  mulge0  8798  leltap  8804  negap0d  8810  ltleap  8811  ltapd  8817  ap0gt0  8819  ap0gt0d  8820  mulcanapad  8842  mulcanap2ad  8843  eqnegad  8913  diveqap0d  8976  diveqap1d  8977  divap1d  8980  rec11apd  8990  div11apd  9010  div2subap  9016  recgt0  9029  prodgt0  9031  lemul1a  9037  lemulge12  9046  lt2msq1  9064  lediv12a  9073  recreclt  9079  nn1suc  9161  nnnlt1  9168  nn2ge  9175  nn1gt1  9176  nnrecl  9399  nn0nlt0  9427  elnn0z  9491  nnnle0  9527  nn0negleid  9547  elz2  9550  nn0n0n1ge2b  9558  nnm1ge0  9565  nn0ge0div  9566  zextle  9570  suprzclex  9577  nn0ind-raph  9596  zindd  9597  uzneg  9774  eluzadd  9784  eluzsub  9785  uzm1  9786  uz3m2nn  9806  supminfex  9830  infregelbex  9831  nn01to3  9850  irrmulap  9881  ltrec1d  9951  lerec2d  9952  ledivdivd  9956  divge1  9957  ltmul1dd  9986  ltmul2dd  9987  ltdiv1dd  9988  lediv1dd  9989  ltdiv23d  9991  lediv23d  9992  nn0ledivnn  10001  addlelt  10002  xrlelttr  10040  xrltletr  10041  xaddass2  10104  xltadd1  10110  xlt2add  10114  ixxdisj  10137  icoshftf1o  10225  icodisj  10226  lincmb01cmp  10237  iccf1o  10238  uzsubsubfz  10281  fzdisj  10286  fzopth  10295  fznatpl1  10310  fzsuc2  10313  fzp1disj  10314  fzrev2i  10320  uzdisj  10327  fseq1p1m1  10328  fzm1  10334  fzneuz  10335  fzp1nel  10338  fzrevral  10339  fznn0sub2  10362  fz0fzdiffz0  10364  difelfzle  10368  difelfznle  10369  nn0disj  10372  fzonnsub  10405  fzodisj  10414  fzouzdisj  10416  fzoun  10417  eluzgtdifelfzo  10441  ubmelfzo  10444  fzonn0p1p1  10457  ubmelm1fzo  10470  fzostep1  10482  exfzdc  10485  subfzo0  10487  zsupcllemstep  10488  infssuzex  10492  zsupssdc  10497  qtri3or  10499  exbtwnzlemex  10508  rebtwn2z  10513  qbtwnrelemcalc  10514  qbtwnre  10515  qavgle  10517  apbtwnz  10533  flid  10543  flqwordi  10547  flqmulnn0  10558  flhalf  10561  flltdivnn0lt  10563  fldiv4p1lem1div2  10564  intfracq  10581  flqdiv  10582  flqpmodeq  10588  modqmulnn  10603  mulqaddmodid  10625  modqmuladdim  10628  modqmuladdnn0  10629  m1modge3gt1  10632  q2submod  10646  modaddmodup  10648  modqsubdir  10654  modqeqmodmin  10655  modfzo0difsn  10656  uzennn  10697  uzsinds  10705  monoord2  10747  ser3mono  10748  iseqf1olemqcl  10760  iseqf1olemnab  10762  iseqf1olemab  10763  iseqf1olemqf1o  10767  iseqf1olemqk  10768  seq3f1olemqsumkj  10772  seq3f1olemqsumk  10773  seq3f1olemqsum  10774  seq3f1olemp  10776  seqf1oglem1  10780  seqf1oglem2  10781  ser3le  10798  exp3val  10802  expnegap0  10808  expgt1  10838  ltexp2a  10852  le2sq2  10876  nnlesq  10904  qsqeqor  10911  bernneq  10921  expnbnd  10924  expnlbnd  10925  expnlbnd2  10926  expeq0d  10930  sq11d  10967  nn0ltexp2  10970  expcand  10978  nn0opthd  10983  facdiv  10999  faclbnd6  11005  facubnd  11006  facavg  11007  bcval4  11013  bcp1nk  11023  bcval5  11024  bcpasc  11027  hashennnuni  11040  isfinite4im  11053  hashnncl  11056  hashunlem  11066  fiprsshashgt1  11080  hashfzp1  11087  zfz1isolemiso  11102  seq3coll  11105  hash2en  11106  iswrdiz  11119  wrdffz  11133  ffz0iswrdnn0  11139  ccatval21sw  11181  ccatass  11184  ccatalpha  11189  swrdf  11235  swrdlend  11238  ccatswrd  11250  swrdccat2  11251  pfxsuffeqwrdeq  11278  ccatpfx  11281  ccats1pfxeq  11294  cats1un  11301  wrdind  11302  wrd2ind  11303  pfxccatin12  11313  swrdccat  11315  s2dmg  11370  seq3shft  11398  cjth  11406  cjdivap  11469  cjne0d  11507  cjap0d  11508  cvg1nlemcxze  11542  cvg1nlemcau  11544  cvg1nlemres  11545  recvguniq  11555  resqrexlemover  11570  resqrexlemdecn  11572  resqrexlemlo  11573  resqrexlemcalc2  11575  resqrexlemcalc3  11576  resqrexlemnmsq  11577  resqrexlemnm  11578  resqrexlemcvg  11579  resqrexlemglsq  11582  resqrexlemga  11583  leabs  11634  absrele  11643  nn0abscl  11645  ltabs  11647  abslt  11648  absle  11649  abstri  11664  amgm2  11678  sqr11d  11733  abs00d  11746  maxabsle  11764  maxabslemlub  11767  maxleastlt  11775  maxltsup  11778  2zsupmax  11786  minmax  11790  2zinfmin  11803  xrmaxleim  11804  xrmaxiflemlub  11808  xrmaxiflemcom  11809  xrmaxiflemval  11810  xrmaxleastlt  11816  xrmaxltsup  11818  xrmaxaddlem  11820  xrmaxadd  11821  xrminmax  11825  xrmin1inf  11827  xrmin2inf  11828  xrmineqinf  11829  climi  11847  reccn2ap  11873  climge0  11885  climle  11894  climserle  11905  climrecvg1n  11908  fz1f1o  11935  summodclem3  11940  summodclem2a  11941  summodc  11943  fisumss  11952  fsum0diaglem  12000  mptfzshft  12002  fsumrev  12003  fisum0diag2  12007  fsumlessfi  12020  fsumle  12023  fsumlt  12024  isumsplit  12051  isumrpcl  12054  expcnvap0  12062  geosergap  12066  pwm1geoserap1  12068  absgtap  12070  geolim  12071  geolim2  12072  georeclim  12073  geoisumr  12078  geoisum1c  12080  cvgratnnlembern  12083  cvgratnnlemseq  12086  cvgratnnlemsumlt  12088  cvgratnnlemfm  12089  cvgratnnlemrate  12090  cvgratnn  12091  cvgratz  12092  mertenslemub  12094  mertenslemi1  12095  mertenslem2  12096  mertensabs  12097  prodmodclem2a  12136  prodmodc  12138  zproddc  12139  fprodntrivap  12144  fprodf1o  12148  fprodssdc  12150  fprodsplitdc  12156  fprodrev  12179  fprodmodd  12201  efcllemp  12218  ege2le3  12231  eftlcvg  12247  eftlub  12250  efltim  12258  eflegeo  12261  tanaddap  12299  sinbnd  12312  cosbnd  12313  sin01bnd  12317  cos01bnd  12318  sinltxirr  12321  sin01gt0  12322  cos01gt0  12323  cos12dec  12328  eirraplem  12337  zdvdsdc  12372  dvdstr  12388  dvdsadd2b  12400  fsumdvds  12402  dvdslelemd  12403  divconjdvds  12409  alzdvds  12414  dvdsext  12415  fzm1ndvds  12416  fzo0dvdseq  12417  3dvds  12424  zeo3  12428  even2n  12434  mod2eq1n2dvds  12439  nn0ehalf  12463  nnehalf  12464  nno  12466  nn0oddm1d2  12469  divalglemnqt  12480  divalglemex  12482  divalglemeuneg  12483  divalg2  12486  divalgmod  12487  flodddiv4t2lthalf  12499  bitsfzolem  12514  bitsfzo  12515  bitsmod  12516  bitsfi  12517  bitscmp  12518  bitsinv1lem  12521  bitsinv1  12522  dvdsbnd  12526  gcdsupex  12527  gcdsupcl  12528  gcddvds  12533  divgcdz  12541  divgcdnn  12545  gcd0id  12549  gcdneg  12552  gcd1  12557  dvdsgcdidd  12564  bezoutlemnewy  12566  bezoutlemstep  12567  bezoutlemmo  12576  bezoutlemsup  12579  dfgcd3  12580  bezout  12581  dfgcd2  12584  mulgcd  12586  sqgcd  12599  dvdssqlem  12600  bezoutr1  12603  uzwodc  12607  nninfctlemfo  12610  lcmval  12634  lcmcllem  12638  dvdslcm  12640  lcmgcdlem  12648  lcmdvds  12650  lcmgcdeq  12654  ncoprmgcdne1b  12660  mulgcddvds  12665  rpmulgcd2  12666  qredeu  12668  rpdvds  12670  prmind2  12691  nprm  12694  dvdsnprmd  12696  isprm5lem  12712  isprm5  12713  divgcdodd  12714  isprm6  12718  prmexpb  12722  pw2dvds  12737  pw2dvdseulemle  12738  oddpwdclemdc  12744  sqne2sq  12748  znege1  12749  sqrt2irraplemnn  12750  divnumden  12767  divdenle  12768  qden1elz  12776  nn0sqrtelqelz  12777  hashdvds  12792  crth  12795  phimullem  12796  eulerthlemfi  12799  eulerthlemh  12802  eulerthlemth  12803  eulerth  12804  prmdiv  12806  prmdiveq  12807  hashgcdlem  12809  dvdsfi  12810  phisum  12812  odzcllem  12814  odzdvds  12817  odzphi  12818  oddprm  12831  pythagtriplem3  12839  pythagtriplem4  12840  pythagtriplem10  12841  pythagtriplem11  12846  pythagtriplem13  12848  pythagtriplem19  12854  pcprendvds  12862  pcprendvds2  12863  pcpre1  12864  pcpremul  12865  pceulem  12866  pceu  12867  pczpre  12869  pcmul  12873  pcdiv  12874  pcqmul  12875  pcqdiv  12879  pcexp  12881  pcidlem  12895  pcneg  12897  pcdvdstr  12899  pcgcd1  12900  pc2dvds  12902  dvdsprmpweq  12907  dvdsprmpweqle  12909  pcaddlem  12911  pcadd  12912  pcadd2  12913  pcmpt  12915  fldivp1  12920  pcfaclem  12921  pcfac  12922  pcbc  12923  qexpz  12924  oddprmdvds  12926  pockthlem  12928  pockthg  12929  infpnlem2  12932  1arith  12939  4sqlem9  12958  4sqlem10  12959  4sqlem11  12973  4sqlem12  12974  4sqlem13m  12975  4sqlem14  12976  4sqlem16  12978  oddennn  13012  ennnfonelemk  13020  ennnfonelemkh  13032  ennnfonelemhf1o  13033  ennnfonelemex  13034  ennnfonelemhom  13035  ennnfonelemrnh  13036  ennnfonelemen  13041  ennnfonelemim  13044  ctinfomlemom  13047  ctiunctlemf  13058  ssnnctlemct  13066  nninfdclemcl  13068  nninfdclemp1  13070  nninfdclemlt  13071  unbendc  13074  prdsbascl  13371  pwselbas  13376  mgmb1mgm1  13450  mgm1  13452  mgmidsssn0  13466  gsumfzval  13473  gsumress  13477  gsum0g  13478  gsumval2  13479  sgrp1  13493  sgrpidmndm  13502  ismndd  13519  prds0g  13531  mhmpropd  13548  resmhm  13569  resmhm2b  13571  gsumwsubmcl  13578  gsumwmhm  13580  isgrpd2e  13602  grpidd2  13623  isgrpinv  13636  grpinvinv  13649  grpidssd  13658  grpinvssd  13659  mulgval  13708  mulgfng  13710  mulgnegnn  13718  subg0  13766  issubg4m  13779  nsgconj  13792  1nsgtrivd  13805  eqgen  13813  eqgcpbl  13814  qus0  13821  ghmid  13835  resghm  13846  ghmnsgpreima  13855  kerf1ghm  13860  conjsubgen  13864  conjnmz  13865  imasabl  13922  rnglz  13957  rngrz  13958  qusrng  13970  issrgid  13993  srg1zr  13999  ringcl  14025  isringid  14037  ringcom  14043  ringpropd  14050  ringlz  14055  ringrz  14056  ring1  14071  opprrng  14089  opprring  14091  dvdsrcld  14110  unitcld  14121  unitmulcl  14126  unitgrp  14129  unitnegcl  14143  rhmmul  14177  isrhm2d  14178  rhmdvdsr  14188  rhmopp  14189  elrhmunit  14190  rhmunitinv  14191  subrgugrp  14253  aprsym  14297  islmodd  14306  lmod0vs  14334  lmodfopne  14339  lmodcom  14346  lssclg  14377  lspsnel5a  14423  lspsneq0b  14440  lsslsp  14442  sraring  14462  sralmod  14463  rspssp  14507  rnglidlmsgrp  14510  2idlcpblrng  14536  gsumfzfsumlem0  14599  zncrng  14658  znzrh2  14659  znzrhfo  14661  znf1o  14664  znfi  14668  znhash  14669  znidom  14670  znidomb  14671  znunit  14672  znrrg  14673  psrbaglesuppg  14685  psrelbas  14688  psrelbasfi  14689  psrgrp  14698  psr0  14699  psr1clfi  14701  mplsubgfilemcl  14712  mplsubgfileminv  14713  ntridm  14849  ntrtop  14851  ntrcls0  14854  ntr0  14857  isopn3i  14858  neiss2  14865  opnneiss  14881  topssnei  14885  cnpf2  14930  icnpimaex  14934  lmcvg  14940  iscnp4  14941  cncnp  14953  cnptopresti  14961  lmfss  14967  lmtopcnp  14973  hmeores  15038  bldisj  15124  xblss2ps  15127  xblss2  15128  blhalf  15131  blssps  15150  blss  15151  ssblex  15154  blpnfctr  15162  xmetresbl  15163  mopni2  15206  bdxmet  15224  bdbl  15226  xmetxpbl  15231  metcnpi  15238  metcnpi2  15239  tgioo  15277  rescncf  15304  mulcncflem  15330  cnopnap  15334  dedekindeulemuub  15340  dedekindeulemloc  15342  dedekindeulemlu  15344  dedekindeu  15346  dedekindicclemuub  15349  dedekindicclemloc  15351  dedekindicclemlu  15353  dedekindicclemicc  15355  dedekindicc  15356  ivthinclemlopn  15359  ivthinclemuopn  15361  ivthdec  15367  ivthreinc  15368  hovergt0  15373  dich0  15375  limcimolemlt  15387  cnplimcim  15390  cnplimclemr  15392  limccnpcntop  15398  limccnp2cntop  15400  limccoap  15401  dvfgg  15411  dvidlemap  15414  dvidrelem  15415  dvidsslem  15416  dvaddxxbr  15424  dvmulxxbr  15425  dvaddxx  15426  dvmulxx  15427  dviaddf  15428  dvimulf  15429  dvcoapbr  15430  dvcjbr  15431  dvcj  15432  dvrecap  15436  dvmptclx  15441  dveflem  15449  elply2  15458  plyf  15460  plyaddlem  15472  plymullem  15473  plycoeid3  15480  plyco  15482  plycj  15484  dvply1  15488  dvply2g  15489  reeff1oleme  15495  eflt  15498  sin0pilem1  15504  pilem3  15506  cosq14gt0  15555  coseq0negpitopi  15559  tangtx  15561  coskpi  15571  cosordlem  15572  cosq34lt1  15573  relogef  15587  logrpap0d  15601  rplogcl  15602  logge0  15603  logdivlti  15604  cxplt3  15643  rpabscxpbnd  15663  dvdsppwf1o  15712  fsumdvdsmul  15714  mersenne  15720  perfect1  15721  perfectlem1  15722  perfectlem2  15723  perfect  15724  lgslem1  15728  lgsval  15732  lgsfvalg  15733  lgsval2lem  15738  lgsvalmod  15747  lgsfcl3  15749  lgsmod  15754  lgsdirprm  15762  lgsdir  15763  lgsdilem2  15764  lgsdi  15765  lgsne0  15766  gausslemma2dlem0i  15785  gausslemma2dlem1a  15786  gausslemma2dlem1f1o  15788  gausslemma2dlem3  15791  gausslemma2dlem4  15792  lgseisenlem1  15798  lgseisenlem2  15799  lgseisenlem3  15800  lgseisenlem4  15801  lgseisen  15802  lgsquadlem1  15805  lgsquadlem2  15806  lgsquadlem3  15807  lgsquad2lem1  15809  lgsquad2lem2  15810  lgsquad3  15812  2lgslem1c  15818  2lgsoddprm  15841  2sqlem3  15845  2sqlem4  15846  2sqlem8  15851  lpvtx  15929  umgrnloopv  15964  umgredgne  16000  ausgrusgrien  16021  uhgr0vusgr  16088  usgr1vr  16098  p1evtxdeqfilem  16161  wlkcompim  16202  wlkvtxedg  16213  upgr2wlkdc  16227  clwwlkccatlem  16250  clwwlknp  16267  clwwlkext2edg  16272  bj-charfunr  16405  pw1ndom3lem  16588  2omap  16594  pw1map  16596  pwf1oexmid  16600  subctctexmid  16601  domomsubct  16602  pw1nct  16604  nnsf  16607  peano4nninf  16608  nninfsellemeq  16616  nnnninfex  16624  cvgcmp2nlemabs  16636  iooref1o  16638  trilpolemisumle  16642  trilpolemeq1  16644  trilpolemlt1  16645  trirec0  16648  apdifflemf  16650  apdifflemr  16651  apdiff  16652  iswomninnlem  16653  redcwlpo  16659  redc0  16661  reap0  16662  nconstwlpolemgt0  16668  neapmkvlem  16671  ltlenmkv  16674  supfz  16675  inffz  16676  gfsumval  16680  gsumgfsumlem  16683  gsumgfsum  16684