Theorem mpbid 147

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

Hypotheses

Ref	Expression
mpbid.min	|- ( ph -> ps )
mpbid.maj	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
mpbid	|- ( ph -> ch )

Proof of Theorem mpbid

Step	Hyp	Ref	Expression
1		mpbid.min	. 2 |- ( ph -> ps )
2		mpbid.maj	. . 3 |- ( ph -> ( ps <-> ch ) )
3	2	biimpd 144	. 2 |- ( ph -> ( ps -> ch ) )
4	1, 3	mpd 13	1 |- ( ph -> ch )

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  11416  cjth  11424  cjdivap  11487  cjne0d  11525  cjap0d  11526  cvg1nlemcxze  11560  cvg1nlemcau  11562  cvg1nlemres  11563  recvguniq  11573  resqrexlemover  11588  resqrexlemdecn  11590  resqrexlemlo  11591  resqrexlemcalc2  11593  resqrexlemcalc3  11594  resqrexlemnmsq  11595  resqrexlemnm  11596  resqrexlemcvg  11597  resqrexlemglsq  11600  resqrexlemga  11601  leabs  11652  absrele  11661  nn0abscl  11663  ltabs  11665  abslt  11666  absle  11667  abstri  11682  amgm2  11696  sqr11d  11751  abs00d  11764  maxabsle  11782  maxabslemlub  11785  maxleastlt  11793  maxltsup  11796  2zsupmax  11804  minmax  11808  2zinfmin  11821  xrmaxleim  11822  xrmaxiflemlub  11826  xrmaxiflemcom  11827  xrmaxiflemval  11828  xrmaxleastlt  11834  xrmaxltsup  11836  xrmaxaddlem  11838  xrmaxadd  11839  xrminmax  11843  xrmin1inf  11845  xrmin2inf  11846  xrmineqinf  11847  climi  11865  reccn2ap  11891  climge0  11903  climle  11912  climserle  11923  climrecvg1n  11926  fz1f1o  11953  summodclem3  11959  summodclem2a  11960  summodc  11962  fisumss  11971  fsum0diaglem  12019  mptfzshft  12021  fsumrev  12022  fisum0diag2  12026  fsumlessfi  12039  fsumle  12042  fsumlt  12043  isumsplit  12070  isumrpcl  12073  expcnvap0  12081  geosergap  12085  pwm1geoserap1  12087  absgtap  12089  geolim  12090  geolim2  12091  georeclim  12092  geoisumr  12097  geoisum1c  12099  cvgratnnlembern  12102  cvgratnnlemseq  12105  cvgratnnlemsumlt  12107  cvgratnnlemfm  12108  cvgratnnlemrate  12109  cvgratnn  12110  cvgratz  12111  mertenslemub  12113  mertenslemi1  12114  mertenslem2  12115  mertensabs  12116  prodmodclem2a  12155  prodmodc  12157  zproddc  12158  fprodntrivap  12163  fprodf1o  12167  fprodssdc  12169  fprodsplitdc  12175  fprodrev  12198  fprodmodd  12220  efcllemp  12237  ege2le3  12250  eftlcvg  12266  eftlub  12269  efltim  12277  eflegeo  12280  tanaddap  12318  sinbnd  12331  cosbnd  12332  sin01bnd  12336  cos01bnd  12337  sinltxirr  12340  sin01gt0  12341  cos01gt0  12342  cos12dec  12347  eirraplem  12356  zdvdsdc  12391  dvdstr  12407  dvdsadd2b  12419  fsumdvds  12421  dvdslelemd  12422  divconjdvds  12428  alzdvds  12433  dvdsext  12434  fzm1ndvds  12435  fzo0dvdseq  12436  3dvds  12443  zeo3  12447  even2n  12453  mod2eq1n2dvds  12458  nn0ehalf  12482  nnehalf  12483  nno  12485  nn0oddm1d2  12488  divalglemnqt  12499  divalglemex  12501  divalglemeuneg  12502  divalg2  12505  divalgmod  12506  flodddiv4t2lthalf  12518  bitsfzolem  12533  bitsfzo  12534  bitsmod  12535  bitsfi  12536  bitscmp  12537  bitsinv1lem  12540  bitsinv1  12541  dvdsbnd  12545  gcdsupex  12546  gcdsupcl  12547  gcddvds  12552  divgcdz  12560  divgcdnn  12564  gcd0id  12568  gcdneg  12571  gcd1  12576  dvdsgcdidd  12583  bezoutlemnewy  12585  bezoutlemstep  12586  bezoutlemmo  12595  bezoutlemsup  12598  dfgcd3  12599  bezout  12600  dfgcd2  12603  mulgcd  12605  sqgcd  12618  dvdssqlem  12619  bezoutr1  12622  uzwodc  12626  nninfctlemfo  12629  lcmval  12653  lcmcllem  12657  dvdslcm  12659  lcmgcdlem  12667  lcmdvds  12669  lcmgcdeq  12673  ncoprmgcdne1b  12679  mulgcddvds  12684  rpmulgcd2  12685  qredeu  12687  rpdvds  12689  prmind2  12710  nprm  12713  dvdsnprmd  12715  isprm5lem  12731  isprm5  12732  divgcdodd  12733  isprm6  12737  prmexpb  12741  pw2dvds  12756  pw2dvdseulemle  12757  oddpwdclemdc  12763  sqne2sq  12767  znege1  12768  sqrt2irraplemnn  12769  divnumden  12786  divdenle  12787  qden1elz  12795  nn0sqrtelqelz  12796  hashdvds  12811  crth  12814  phimullem  12815  eulerthlemfi  12818  eulerthlemh  12821  eulerthlemth  12822  eulerth  12823  prmdiv  12825  prmdiveq  12826  hashgcdlem  12828  dvdsfi  12829  phisum  12831  odzcllem  12833  odzdvds  12836  odzphi  12837  oddprm  12850  pythagtriplem3  12858  pythagtriplem4  12859  pythagtriplem10  12860  pythagtriplem11  12865  pythagtriplem13  12867  pythagtriplem19  12873  pcprendvds  12881  pcprendvds2  12882  pcpre1  12883  pcpremul  12884  pceulem  12885  pceu  12886  pczpre  12888  pcmul  12892  pcdiv  12893  pcqmul  12894  pcqdiv  12898  pcexp  12900  pcidlem  12914  pcneg  12916  pcdvdstr  12918  pcgcd1  12919  pc2dvds  12921  dvdsprmpweq  12926  dvdsprmpweqle  12928  pcaddlem  12930  pcadd  12931  pcadd2  12932  pcmpt  12934  fldivp1  12939  pcfaclem  12940  pcfac  12941  pcbc  12942  qexpz  12943  oddprmdvds  12945  pockthlem  12947  pockthg  12948  infpnlem2  12951  1arith  12958  4sqlem9  12977  4sqlem10  12978  4sqlem11  12992  4sqlem12  12993  4sqlem13m  12994  4sqlem14  12995  4sqlem16  12997  oddennn  13031  ennnfonelemk  13039  ennnfonelemkh  13051  ennnfonelemhf1o  13052  ennnfonelemex  13053  ennnfonelemhom  13054  ennnfonelemrnh  13055  ennnfonelemen  13060  ennnfonelemim  13063  ctinfomlemom  13066  ctiunctlemf  13077  ssnnctlemct  13085  nninfdclemcl  13087  nninfdclemp1  13089  nninfdclemlt  13090  unbendc  13093  prdsbascl  13390  pwselbas  13395  mgmb1mgm1  13469  mgm1  13471  mgmidsssn0  13485  gsumfzval  13492  gsumress  13496  gsum0g  13497  gsumval2  13498  sgrp1  13512  sgrpidmndm  13521  ismndd  13538  prds0g  13550  mhmpropd  13567  resmhm  13588  resmhm2b  13590  gsumwsubmcl  13597  gsumwmhm  13599  isgrpd2e  13621  grpidd2  13642  isgrpinv  13655  grpinvinv  13668  grpidssd  13677  grpinvssd  13678  mulgval  13727  mulgfng  13729  mulgnegnn  13737  subg0  13785  issubg4m  13798  nsgconj  13811  1nsgtrivd  13824  eqgen  13832  eqgcpbl  13833  qus0  13840  ghmid  13854  resghm  13865  ghmnsgpreima  13874  kerf1ghm  13879  conjsubgen  13883  conjnmz  13884  imasabl  13941  gsumsplit0  13951  rnglz  13977  rngrz  13978  qusrng  13990  issrgid  14013  srg1zr  14019  ringcl  14045  isringid  14057  ringcom  14063  ringpropd  14070  ringlz  14075  ringrz  14076  ring1  14091  opprrng  14109  opprring  14111  dvdsrcld  14130  unitcld  14141  unitmulcl  14146  unitgrp  14149  unitnegcl  14163  rhmmul  14197  isrhm2d  14198  rhmdvdsr  14208  rhmopp  14209  elrhmunit  14210  rhmunitinv  14211  subrgugrp  14273  aprsym  14317  islmodd  14326  lmod0vs  14354  lmodfopne  14359  lmodcom  14366  lssclg  14397  lspsnel5a  14443  lspsneq0b  14460  lsslsp  14462  sraring  14482  sralmod  14483  rspssp  14527  rnglidlmsgrp  14530  2idlcpblrng  14556  gsumfzfsumlem0  14619  zncrng  14678  znzrh2  14679  znzrhfo  14681  znf1o  14684  znfi  14688  znhash  14689  znidom  14690  znidomb  14691  znunit  14692  znrrg  14693  psrbaglesuppg  14705  psrelbas  14708  psrelbasfi  14709  psrgrp  14718  psr0  14719  psr1clfi  14721  mplsubgfilemcl  14732  mplsubgfileminv  14733  ntridm  14869  ntrtop  14871  ntrcls0  14874  ntr0  14877  isopn3i  14878  neiss2  14885  opnneiss  14901  topssnei  14905  cnpf2  14950  icnpimaex  14954  lmcvg  14960  iscnp4  14961  cncnp  14973  cnptopresti  14981  lmfss  14987  lmtopcnp  14993  hmeores  15058  bldisj  15144  xblss2ps  15147  xblss2  15148  blhalf  15151  blssps  15170  blss  15171  ssblex  15174  blpnfctr  15182  xmetresbl  15183  mopni2  15226  bdxmet  15244  bdbl  15246  xmetxpbl  15251  metcnpi  15258  metcnpi2  15259  tgioo  15297  rescncf  15324  mulcncflem  15350  cnopnap  15354  dedekindeulemuub  15360  dedekindeulemloc  15362  dedekindeulemlu  15364  dedekindeu  15366  dedekindicclemuub  15369  dedekindicclemloc  15371  dedekindicclemlu  15373  dedekindicclemicc  15375  dedekindicc  15376  ivthinclemlopn  15379  ivthinclemuopn  15381  ivthdec  15387  ivthreinc  15388  hovergt0  15393  dich0  15395  limcimolemlt  15407  cnplimcim  15410  cnplimclemr  15412  limccnpcntop  15418  limccnp2cntop  15420  limccoap  15421  dvfgg  15431  dvidlemap  15434  dvidrelem  15435  dvidsslem  15436  dvaddxxbr  15444  dvmulxxbr  15445  dvaddxx  15446  dvmulxx  15447  dviaddf  15448  dvimulf  15449  dvcoapbr  15450  dvcjbr  15451  dvcj  15452  dvrecap  15456  dvmptclx  15461  dveflem  15469  elply2  15478  plyf  15480  plyaddlem  15492  plymullem  15493  plycoeid3  15500  plyco  15502  plycj  15504  dvply1  15508  dvply2g  15509  reeff1oleme  15515  eflt  15518  sin0pilem1  15524  pilem3  15526  cosq14gt0  15575  coseq0negpitopi  15579  tangtx  15581  coskpi  15591  cosordlem  15592  cosq34lt1  15593  relogef  15607  logrpap0d  15621  rplogcl  15622  logge0  15623  logdivlti  15624  cxplt3  15663  rpabscxpbnd  15683  dvdsppwf1o  15732  fsumdvdsmul  15734  mersenne  15740  perfect1  15741  perfectlem1  15742  perfectlem2  15743  perfect  15744  lgslem1  15748  lgsval  15752  lgsfvalg  15753  lgsval2lem  15758  lgsvalmod  15767  lgsfcl3  15769  lgsmod  15774  lgsdirprm  15782  lgsdir  15783  lgsdilem2  15784  lgsdi  15785  lgsne0  15786  gausslemma2dlem0i  15805  gausslemma2dlem1a  15806  gausslemma2dlem1f1o  15808  gausslemma2dlem3  15811  gausslemma2dlem4  15812  lgseisenlem1  15818  lgseisenlem2  15819  lgseisenlem3  15820  lgseisenlem4  15821  lgseisen  15822  lgsquadlem1  15825  lgsquadlem2  15826  lgsquadlem3  15827  lgsquad2lem1  15829  lgsquad2lem2  15830  lgsquad3  15832  2lgslem1c  15838  2lgsoddprm  15861  2sqlem3  15865  2sqlem4  15866  2sqlem8  15871  lpvtx  15949  umgrnloopv  15984  umgredgne  16020  ausgrusgrien  16041  uhgr0vusgr  16108  usgr1vr  16118  p1evtxdeqfilem  16181  wlkcompim  16222  wlkvtxedg  16233  upgr2wlkdc  16247  clwwlkccatlem  16270  clwwlknp  16287  clwwlkext2edg  16292  eupth2lem3lem3fi  16340  eulerpathprum  16350  bj-charfunr  16456  pw1ndom3lem  16639  2omap  16645  pw1map  16647  pwf1oexmid  16651  subctctexmid  16652  domomsubct  16653  pw1nct  16655  nnsf  16658  peano4nninf  16659  nninfsellemeq  16667  nnnninfex  16675  cvgcmp2nlemabs  16687  iooref1o  16689  trilpolemisumle  16693  trilpolemeq1  16695  trilpolemlt1  16696  trirec0  16699  apdifflemf  16701  apdifflemr  16702  apdiff  16703  qdiff  16704  iswomninnlem  16705  redcwlpo  16711  redc0  16713  reap0  16714  nconstwlpolemgt0  16720  neapmkvlem  16723  ltlenmkv  16726  supfz  16727  inffz  16728  gfsumval  16732  gsumgfsumlem  16735  gsumgfsum  16736