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  943  mpbi2and  949  bilukdc  1438  equs5or  1876  eqtrd  2262  eleqtrd  2308  neeqtrd  2428  3netr3d  2432  rexlimd2  2646  raleqtrdv  2736  rexeqtrdv  2737  ceqsalt  2826  vtoclgft  2851  vtoclegft  2875  elrab3t  2958  eueq2dc  2976  sbceq1dd  3034  csbiedf  3165  sseqtrd  3262  3sstr3d  3268  ifbothdadc  3636  snssd  3813  dfnfc2  3906  breqdi  4098  breqtrd  4109  3brtr3d  4114  csbexga  4212  reuhypd  4562  reg2exmidlema  4626  elirr  4633  en2lp  4646  onsucuni2  4656  finds  4692  iota4  5298  iota4an  5299  funimaexglem  5404  fneu  5427  fco2  5492  fssres2  5505  fresin  5506  feu  5510  f1orescnv  5590  resdif  5596  funcocnv2  5599  f1oprg  5619  fvelrnb  5683  fimacnv  5766  f1oresrab  5802  fsn2  5811  xpsng  5812  funopsn  5819  fnressn  5829  fsnunf  5843  foeqcnvco  5920  isores1  5944  isoini2  5949  riota5f  5987  riotass2  5989  riotass  5990  ovmpodxf  6136  uchoice  6289  elopabi  6347  cnvf1o  6377  smores3  6445  tfrlemisucaccv  6477  tfr1onlemsucaccv  6493  tfrcllemsucaccv  6506  rdgon  6538  frecabcl  6551  frecsuclem  6558  nnsucsssuc  6646  nnsucuniel  6649  erref  6708  iserd  6714  swoer  6716  swoord1  6717  swoord2  6718  erth  6734  erthi  6736  eroveu  6781  pmresg  6831  mapsn  6845  fndmeng  6971  xpen  7014  phplem4  7024  phplem4on  7037  fidifsnen  7040  dif1en  7049  dif1enen  7050  fisbth  7053  diffisn  7063  ac6sfi  7068  fidcen  7069  fimax2gtri  7072  en2eqpr  7080  unsnfidcex  7093  unsnfidcel  7094  prfidceq  7101  fiintim  7104  fidcenumlemrks  7131  elfi2  7150  elfir  7151  fiuni  7156  fifo  7158  eqsupti  7174  supisoti  7188  ordiso2  7213  casef  7266  difinfsnlem  7277  ctmlemr  7286  ctssdccl  7289  enumct  7293  nninfninc  7301  nnnninfeq  7306  nnnninfeq2  7307  enomnilem  7316  exmidomni  7320  fodjum  7324  fodjuomnilemres  7326  mkvprop  7336  enmkvlem  7339  enwomnilem  7347  nninfdcinf  7349  nninfwlpoimlemdc  7355  nninfinfwlpolem  7356  pr1or2  7378  acfun  7400  2omotaplemap  7454  exmidmotap  7458  ccfunen  7461  cc2lem  7463  dfplpq2  7552  ltanqi  7600  ltmnqi  7601  ltaddnq  7605  subhalfnqq  7612  ltbtwnnqq  7613  archnqq  7615  prarloclemarch2  7617  enq0sym  7630  enq0ref  7631  enq0tr  7632  nqnq0pi  7636  nnnq0lem1  7644  distrnq0  7657  prarloclemlt  7691  prarloclemn  7697  prarloclemcalc  7700  genplt2i  7708  addnqprllem  7725  addnqprulem  7726  addlocprlemgt  7732  appdivnq  7761  prmuloc2  7765  ltexprlemopl  7799  ltexprlemopu  7801  ltexprlemru  7810  prplnqu  7818  cauappcvgprlemopl  7844  cauappcvgprlemlol  7845  cauappcvgprlemladdfu  7852  cauappcvgprlemladdrl  7855  cauappcvgprlem1  7857  archrecnq  7861  archrecpr  7862  caucvgprlemk  7863  caucvgprlemnbj  7865  caucvgprlemm  7866  caucvgprlemopl  7867  caucvgprlemlol  7868  caucvgprlemladdfu  7875  caucvgprlemladdrl  7876  caucvgprlem1  7877  caucvgprprlemk  7881  caucvgprprlemnkeqj  7888  caucvgprprlemnbj  7891  caucvgprprlemml  7892  caucvgprprlemmu  7893  caucvgprprlemopl  7895  caucvgprprlemlol  7896  caucvgprprlemopu  7897  caucvgprprlemexbt  7904  caucvgprprlemexb  7905  caucvgprprlem1  7907  caucvgprprlem2  7908  suplocexprlemru  7917  suplocexprlemdisj  7918  suplocexprlemloc  7919  suplocexprlemub  7921  suplocexprlemlub  7922  prsrlem1  7940  addgt0sr  7973  srpospr  7981  prsrriota  7986  caucvgsrlemgt1  7993  caucvgsrlemoffgt1  7997  caucvgsr  8000  mappsrprg  8002  suplocsrlemb  8004  suplocsrlempr  8005  suplocsrlem  8006  recriota  8088  axsuploc  8230  lelttr  8246  ltletr  8247  ltnsymd  8277  lensymd  8279  cnegexlem3  8334  cnegex2  8336  addcanad  8343  addcan2ad  8344  negcon1ad  8463  negne0d  8466  negrebd  8467  subeq0d  8476  subne0ad  8479  neg11d  8480  subcand  8509  subcan2d  8510  ltadd2  8577  ltadd2dd  8580  add20  8632  ltnegcon1d  8683  ltnegcon2d  8684  lenegcon1d  8685  lenegcon2d  8686  subled  8706  lesubd  8707  ltsub23d  8708  ltsub13d  8709  ltadd1dd  8714  ltsub1dd  8715  ltsub2dd  8716  leadd1dd  8717  leadd2dd  8718  lesub1dd  8719  lesub2dd  8720  recexre  8736  apreap  8745  ltmul1a  8749  reapmul1  8753  cru  8760  apreim  8761  mulge0  8777  leltap  8783  negap0d  8789  ltleap  8790  ltapd  8796  ap0gt0  8798  ap0gt0d  8799  mulcanapad  8821  mulcanap2ad  8822  eqnegad  8892  diveqap0d  8955  diveqap1d  8956  divap1d  8959  rec11apd  8969  div11apd  8989  div2subap  8995  recgt0  9008  prodgt0  9010  lemul1a  9016  lemulge12  9025  lt2msq1  9043  lediv12a  9052  recreclt  9058  nn1suc  9140  nnnlt1  9147  nn2ge  9154  nn1gt1  9155  nnrecl  9378  nn0nlt0  9406  elnn0z  9470  nnnle0  9506  nn0negleid  9526  elz2  9529  nn0n0n1ge2b  9537  nnm1ge0  9544  nn0ge0div  9545  zextle  9549  suprzclex  9556  nn0ind-raph  9575  zindd  9576  uzneg  9753  eluzadd  9763  eluzsub  9764  uzm1  9765  uz3m2nn  9780  supminfex  9804  infregelbex  9805  nn01to3  9824  irrmulap  9855  ltrec1d  9925  lerec2d  9926  ledivdivd  9930  divge1  9931  ltmul1dd  9960  ltmul2dd  9961  ltdiv1dd  9962  lediv1dd  9963  ltdiv23d  9965  lediv23d  9966  nn0ledivnn  9975  addlelt  9976  xrlelttr  10014  xrltletr  10015  xaddass2  10078  xltadd1  10084  xlt2add  10088  ixxdisj  10111  icoshftf1o  10199  icodisj  10200  lincmb01cmp  10211  iccf1o  10212  uzsubsubfz  10255  fzdisj  10260  fzopth  10269  fznatpl1  10284  fzsuc2  10287  fzp1disj  10288  fzrev2i  10294  uzdisj  10301  fseq1p1m1  10302  fzm1  10308  fzneuz  10309  fzp1nel  10312  fzrevral  10313  fznn0sub2  10336  fz0fzdiffz0  10338  difelfzle  10342  difelfznle  10343  nn0disj  10346  fzonnsub  10379  fzodisj  10388  fzouzdisj  10390  fzoun  10391  eluzgtdifelfzo  10415  ubmelfzo  10418  fzonn0p1p1  10431  ubmelm1fzo  10444  fzostep1  10455  exfzdc  10458  subfzo0  10460  zsupcllemstep  10461  infssuzex  10465  zsupssdc  10470  qtri3or  10472  exbtwnzlemex  10481  rebtwn2z  10486  qbtwnrelemcalc  10487  qbtwnre  10488  qavgle  10490  apbtwnz  10506  flid  10516  flqwordi  10520  flqmulnn0  10531  flhalf  10534  flltdivnn0lt  10536  fldiv4p1lem1div2  10537  intfracq  10554  flqdiv  10555  flqpmodeq  10561  modqmulnn  10576  mulqaddmodid  10598  modqmuladdim  10601  modqmuladdnn0  10602  m1modge3gt1  10605  q2submod  10619  modaddmodup  10621  modqsubdir  10627  modqeqmodmin  10628  modfzo0difsn  10629  uzennn  10670  uzsinds  10678  monoord2  10720  ser3mono  10721  iseqf1olemqcl  10733  iseqf1olemnab  10735  iseqf1olemab  10736  iseqf1olemqf1o  10740  iseqf1olemqk  10741  seq3f1olemqsumkj  10745  seq3f1olemqsumk  10746  seq3f1olemqsum  10747  seq3f1olemp  10749  seqf1oglem1  10753  seqf1oglem2  10754  ser3le  10771  exp3val  10775  expnegap0  10781  expgt1  10811  ltexp2a  10825  le2sq2  10849  nnlesq  10877  qsqeqor  10884  bernneq  10894  expnbnd  10897  expnlbnd  10898  expnlbnd2  10899  expeq0d  10903  sq11d  10940  nn0ltexp2  10943  expcand  10951  nn0opthd  10956  facdiv  10972  faclbnd6  10978  facubnd  10979  facavg  10980  bcval4  10986  bcp1nk  10996  bcval5  10997  bcpasc  11000  hashennnuni  11013  isfinite4im  11026  hashnncl  11029  hashunlem  11038  fiprsshashgt1  11052  hashfzp1  11059  zfz1isolemiso  11074  seq3coll  11077  hash2en  11078  iswrdiz  11091  wrdffz  11105  ffz0iswrdnn0  11111  ccatval21sw  11153  ccatass  11156  ccatalpha  11161  swrdf  11203  swrdlend  11206  ccatswrd  11218  swrdccat2  11219  pfxsuffeqwrdeq  11246  ccatpfx  11249  ccats1pfxeq  11262  cats1un  11269  wrdind  11270  wrd2ind  11271  pfxccatin12  11281  swrdccat  11283  s2dmg  11338  seq3shft  11365  cjth  11373  cjdivap  11436  cjne0d  11474  cjap0d  11475  cvg1nlemcxze  11509  cvg1nlemcau  11511  cvg1nlemres  11512  recvguniq  11522  resqrexlemover  11537  resqrexlemdecn  11539  resqrexlemlo  11540  resqrexlemcalc2  11542  resqrexlemcalc3  11543  resqrexlemnmsq  11544  resqrexlemnm  11545  resqrexlemcvg  11546  resqrexlemglsq  11549  resqrexlemga  11550  leabs  11601  absrele  11610  nn0abscl  11612  ltabs  11614  abslt  11615  absle  11616  abstri  11631  amgm2  11645  sqr11d  11700  abs00d  11713  maxabsle  11731  maxabslemlub  11734  maxleastlt  11742  maxltsup  11745  2zsupmax  11753  minmax  11757  2zinfmin  11770  xrmaxleim  11771  xrmaxiflemlub  11775  xrmaxiflemcom  11776  xrmaxiflemval  11777  xrmaxleastlt  11783  xrmaxltsup  11785  xrmaxaddlem  11787  xrmaxadd  11788  xrminmax  11792  xrmin1inf  11794  xrmin2inf  11795  xrmineqinf  11796  climi  11814  reccn2ap  11840  climge0  11852  climle  11861  climserle  11872  climrecvg1n  11875  fz1f1o  11902  summodclem3  11907  summodclem2a  11908  summodc  11910  fisumss  11919  fsum0diaglem  11967  mptfzshft  11969  fsumrev  11970  fisum0diag2  11974  fsumlessfi  11987  fsumle  11990  fsumlt  11991  isumsplit  12018  isumrpcl  12021  expcnvap0  12029  geosergap  12033  pwm1geoserap1  12035  absgtap  12037  geolim  12038  geolim2  12039  georeclim  12040  geoisumr  12045  geoisum1c  12047  cvgratnnlembern  12050  cvgratnnlemseq  12053  cvgratnnlemsumlt  12055  cvgratnnlemfm  12056  cvgratnnlemrate  12057  cvgratnn  12058  cvgratz  12059  mertenslemub  12061  mertenslemi1  12062  mertenslem2  12063  mertensabs  12064  prodmodclem2a  12103  prodmodc  12105  zproddc  12106  fprodntrivap  12111  fprodf1o  12115  fprodssdc  12117  fprodsplitdc  12123  fprodrev  12146  fprodmodd  12168  efcllemp  12185  ege2le3  12198  eftlcvg  12214  eftlub  12217  efltim  12225  eflegeo  12228  tanaddap  12266  sinbnd  12279  cosbnd  12280  sin01bnd  12284  cos01bnd  12285  sinltxirr  12288  sin01gt0  12289  cos01gt0  12290  cos12dec  12295  eirraplem  12304  zdvdsdc  12339  dvdstr  12355  dvdsadd2b  12367  fsumdvds  12369  dvdslelemd  12370  divconjdvds  12376  alzdvds  12381  dvdsext  12382  fzm1ndvds  12383  fzo0dvdseq  12384  3dvds  12391  zeo3  12395  even2n  12401  mod2eq1n2dvds  12406  nn0ehalf  12430  nnehalf  12431  nno  12433  nn0oddm1d2  12436  divalglemnqt  12447  divalglemex  12449  divalglemeuneg  12450  divalg2  12453  divalgmod  12454  flodddiv4t2lthalf  12466  bitsfzolem  12481  bitsfzo  12482  bitsmod  12483  bitsfi  12484  bitscmp  12485  bitsinv1lem  12488  bitsinv1  12489  dvdsbnd  12493  gcdsupex  12494  gcdsupcl  12495  gcddvds  12500  divgcdz  12508  divgcdnn  12512  gcd0id  12516  gcdneg  12519  gcd1  12524  dvdsgcdidd  12531  bezoutlemnewy  12533  bezoutlemstep  12534  bezoutlemmo  12543  bezoutlemsup  12546  dfgcd3  12547  bezout  12548  dfgcd2  12551  mulgcd  12553  sqgcd  12566  dvdssqlem  12567  bezoutr1  12570  uzwodc  12574  nninfctlemfo  12577  lcmval  12601  lcmcllem  12605  dvdslcm  12607  lcmgcdlem  12615  lcmdvds  12617  lcmgcdeq  12621  ncoprmgcdne1b  12627  mulgcddvds  12632  rpmulgcd2  12633  qredeu  12635  rpdvds  12637  prmind2  12658  nprm  12661  dvdsnprmd  12663  isprm5lem  12679  isprm5  12680  divgcdodd  12681  isprm6  12685  prmexpb  12689  pw2dvds  12704  pw2dvdseulemle  12705  oddpwdclemdc  12711  sqne2sq  12715  znege1  12716  sqrt2irraplemnn  12717  divnumden  12734  divdenle  12735  qden1elz  12743  nn0sqrtelqelz  12744  hashdvds  12759  crth  12762  phimullem  12763  eulerthlemfi  12766  eulerthlemh  12769  eulerthlemth  12770  eulerth  12771  prmdiv  12773  prmdiveq  12774  hashgcdlem  12776  dvdsfi  12777  phisum  12779  odzcllem  12781  odzdvds  12784  odzphi  12785  oddprm  12798  pythagtriplem3  12806  pythagtriplem4  12807  pythagtriplem10  12808  pythagtriplem11  12813  pythagtriplem13  12815  pythagtriplem19  12821  pcprendvds  12829  pcprendvds2  12830  pcpre1  12831  pcpremul  12832  pceulem  12833  pceu  12834  pczpre  12836  pcmul  12840  pcdiv  12841  pcqmul  12842  pcqdiv  12846  pcexp  12848  pcidlem  12862  pcneg  12864  pcdvdstr  12866  pcgcd1  12867  pc2dvds  12869  dvdsprmpweq  12874  dvdsprmpweqle  12876  pcaddlem  12878  pcadd  12879  pcadd2  12880  pcmpt  12882  fldivp1  12887  pcfaclem  12888  pcfac  12889  pcbc  12890  qexpz  12891  oddprmdvds  12893  pockthlem  12895  pockthg  12896  infpnlem2  12899  1arith  12906  4sqlem9  12925  4sqlem10  12926  4sqlem11  12940  4sqlem12  12941  4sqlem13m  12942  4sqlem14  12943  4sqlem16  12945  oddennn  12979  ennnfonelemk  12987  ennnfonelemkh  12999  ennnfonelemhf1o  13000  ennnfonelemex  13001  ennnfonelemhom  13002  ennnfonelemrnh  13003  ennnfonelemen  13008  ennnfonelemim  13011  ctinfomlemom  13014  ctiunctlemf  13025  ssnnctlemct  13033  nninfdclemcl  13035  nninfdclemp1  13037  nninfdclemlt  13038  unbendc  13041  prdsbascl  13338  pwselbas  13343  mgmb1mgm1  13417  mgm1  13419  mgmidsssn0  13433  gsumfzval  13440  gsumress  13444  gsum0g  13445  gsumval2  13446  sgrp1  13460  sgrpidmndm  13469  ismndd  13486  prds0g  13498  mhmpropd  13515  resmhm  13536  resmhm2b  13538  gsumwsubmcl  13545  gsumwmhm  13547  isgrpd2e  13569  grpidd2  13590  isgrpinv  13603  grpinvinv  13616  grpidssd  13625  grpinvssd  13626  mulgval  13675  mulgfng  13677  mulgnegnn  13685  subg0  13733  issubg4m  13746  nsgconj  13759  1nsgtrivd  13772  eqgen  13780  eqgcpbl  13781  qus0  13788  ghmid  13802  resghm  13813  ghmnsgpreima  13822  kerf1ghm  13827  conjsubgen  13831  conjnmz  13832  imasabl  13889  rnglz  13924  rngrz  13925  qusrng  13937  issrgid  13960  srg1zr  13966  ringcl  13992  isringid  14004  ringcom  14010  ringpropd  14017  ringlz  14022  ringrz  14023  ring1  14038  opprrng  14056  opprring  14058  dvdsrcld  14077  unitcld  14088  unitmulcl  14093  unitgrp  14096  unitnegcl  14110  rhmmul  14144  isrhm2d  14145  rhmdvdsr  14155  rhmopp  14156  elrhmunit  14157  rhmunitinv  14158  subrgugrp  14220  aprsym  14264  islmodd  14273  lmod0vs  14301  lmodfopne  14306  lmodcom  14313  lssclg  14344  lspsnel5a  14390  lspsneq0b  14407  lsslsp  14409  sraring  14429  sralmod  14430  rspssp  14474  rnglidlmsgrp  14477  2idlcpblrng  14503  gsumfzfsumlem0  14566  zncrng  14625  znzrh2  14626  znzrhfo  14628  znf1o  14631  znfi  14635  znhash  14636  znidom  14637  znidomb  14638  znunit  14639  znrrg  14640  psrbaglesuppg  14652  psrelbas  14655  psrelbasfi  14656  psrgrp  14665  psr0  14666  psr1clfi  14668  mplsubgfilemcl  14679  mplsubgfileminv  14680  ntridm  14816  ntrtop  14818  ntrcls0  14821  ntr0  14824  isopn3i  14825  neiss2  14832  opnneiss  14848  topssnei  14852  cnpf2  14897  icnpimaex  14901  lmcvg  14907  iscnp4  14908  cncnp  14920  cnptopresti  14928  lmfss  14934  lmtopcnp  14940  hmeores  15005  bldisj  15091  xblss2ps  15094  xblss2  15095  blhalf  15098  blssps  15117  blss  15118  ssblex  15121  blpnfctr  15129  xmetresbl  15130  mopni2  15173  bdxmet  15191  bdbl  15193  xmetxpbl  15198  metcnpi  15205  metcnpi2  15206  tgioo  15244  rescncf  15271  mulcncflem  15297  cnopnap  15301  dedekindeulemuub  15307  dedekindeulemloc  15309  dedekindeulemlu  15311  dedekindeu  15313  dedekindicclemuub  15316  dedekindicclemloc  15318  dedekindicclemlu  15320  dedekindicclemicc  15322  dedekindicc  15323  ivthinclemlopn  15326  ivthinclemuopn  15328  ivthdec  15334  ivthreinc  15335  hovergt0  15340  dich0  15342  limcimolemlt  15354  cnplimcim  15357  cnplimclemr  15359  limccnpcntop  15365  limccnp2cntop  15367  limccoap  15368  dvfgg  15378  dvidlemap  15381  dvidrelem  15382  dvidsslem  15383  dvaddxxbr  15391  dvmulxxbr  15392  dvaddxx  15393  dvmulxx  15394  dviaddf  15395  dvimulf  15396  dvcoapbr  15397  dvcjbr  15398  dvcj  15399  dvrecap  15403  dvmptclx  15408  dveflem  15416  elply2  15425  plyf  15427  plyaddlem  15439  plymullem  15440  plycoeid3  15447  plyco  15449  plycj  15451  dvply1  15455  dvply2g  15456  reeff1oleme  15462  eflt  15465  sin0pilem1  15471  pilem3  15473  cosq14gt0  15522  coseq0negpitopi  15526  tangtx  15528  coskpi  15538  cosordlem  15539  cosq34lt1  15540  relogef  15554  logrpap0d  15568  rplogcl  15569  logge0  15570  logdivlti  15571  cxplt3  15610  rpabscxpbnd  15630  dvdsppwf1o  15679  fsumdvdsmul  15681  mersenne  15687  perfect1  15688  perfectlem1  15689  perfectlem2  15690  perfect  15691  lgslem1  15695  lgsval  15699  lgsfvalg  15700  lgsval2lem  15705  lgsvalmod  15714  lgsfcl3  15716  lgsmod  15721  lgsdirprm  15729  lgsdir  15730  lgsdilem2  15731  lgsdi  15732  lgsne0  15733  gausslemma2dlem0i  15752  gausslemma2dlem1a  15753  gausslemma2dlem1f1o  15755  gausslemma2dlem3  15758  gausslemma2dlem4  15759  lgseisenlem1  15765  lgseisenlem2  15766  lgseisenlem3  15767  lgseisenlem4  15768  lgseisen  15769  lgsquadlem1  15772  lgsquadlem2  15773  lgsquadlem3  15774  lgsquad2lem1  15776  lgsquad2lem2  15777  lgsquad3  15779  2lgslem1c  15785  2lgsoddprm  15808  2sqlem3  15812  2sqlem4  15813  2sqlem8  15818  lpvtx  15895  umgrnloopv  15930  umgredgne  15964  ausgrusgrien  15985  wlkcompim  16098  wlkvtxedg  16109  upgr2wlkdc  16121  clwwlkccatlem  16143  clwwlknp  16159  clwwlkext2edg  16164  bj-charfunr  16256  pw1ndom3lem  16440  2omap  16446  pw1map  16448  pwf1oexmid  16452  subctctexmid  16453  domomsubct  16454  pw1nct  16456  nnsf  16459  peano4nninf  16460  nninfsellemeq  16468  nnnninfex  16476  cvgcmp2nlemabs  16488  iooref1o  16490  trilpolemisumle  16494  trilpolemeq1  16496  trilpolemlt1  16497  trirec0  16500  apdifflemf  16502  apdifflemr  16503  apdiff  16504  iswomninnlem  16505  redcwlpo  16511  redc0  16513  reap0  16514  nconstwlpolemgt0  16520  neapmkvlem  16523  ltlenmkv  16526  supfz  16527  inffz  16528