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  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  11202  swrdlend  11205  ccatswrd  11217  swrdccat2  11218  pfxsuffeqwrdeq  11245  ccatpfx  11248  ccats1pfxeq  11261  cats1un  11268  wrdind  11269  wrd2ind  11270  pfxccatin12  11280  swrdccat  11282  s2dmg  11337  seq3shft  11364  cjth  11372  cjdivap  11435  cjne0d  11473  cjap0d  11474  cvg1nlemcxze  11508  cvg1nlemcau  11510  cvg1nlemres  11511  recvguniq  11521  resqrexlemover  11536  resqrexlemdecn  11538  resqrexlemlo  11539  resqrexlemcalc2  11541  resqrexlemcalc3  11542  resqrexlemnmsq  11543  resqrexlemnm  11544  resqrexlemcvg  11545  resqrexlemglsq  11548  resqrexlemga  11549  leabs  11600  absrele  11609  nn0abscl  11611  ltabs  11613  abslt  11614  absle  11615  abstri  11630  amgm2  11644  sqr11d  11699  abs00d  11712  maxabsle  11730  maxabslemlub  11733  maxleastlt  11741  maxltsup  11744  2zsupmax  11752  minmax  11756  2zinfmin  11769  xrmaxleim  11770  xrmaxiflemlub  11774  xrmaxiflemcom  11775  xrmaxiflemval  11776  xrmaxleastlt  11782  xrmaxltsup  11784  xrmaxaddlem  11786  xrmaxadd  11787  xrminmax  11791  xrmin1inf  11793  xrmin2inf  11794  xrmineqinf  11795  climi  11813  reccn2ap  11839  climge0  11851  climle  11860  climserle  11871  climrecvg1n  11874  fz1f1o  11901  summodclem3  11906  summodclem2a  11907  summodc  11909  fisumss  11918  fsum0diaglem  11966  mptfzshft  11968  fsumrev  11969  fisum0diag2  11973  fsumlessfi  11986  fsumle  11989  fsumlt  11990  isumsplit  12017  isumrpcl  12020  expcnvap0  12028  geosergap  12032  pwm1geoserap1  12034  absgtap  12036  geolim  12037  geolim2  12038  georeclim  12039  geoisumr  12044  geoisum1c  12046  cvgratnnlembern  12049  cvgratnnlemseq  12052  cvgratnnlemsumlt  12054  cvgratnnlemfm  12055  cvgratnnlemrate  12056  cvgratnn  12057  cvgratz  12058  mertenslemub  12060  mertenslemi1  12061  mertenslem2  12062  mertensabs  12063  prodmodclem2a  12102  prodmodc  12104  zproddc  12105  fprodntrivap  12110  fprodf1o  12114  fprodssdc  12116  fprodsplitdc  12122  fprodrev  12145  fprodmodd  12167  efcllemp  12184  ege2le3  12197  eftlcvg  12213  eftlub  12216  efltim  12224  eflegeo  12227  tanaddap  12265  sinbnd  12278  cosbnd  12279  sin01bnd  12283  cos01bnd  12284  sinltxirr  12287  sin01gt0  12288  cos01gt0  12289  cos12dec  12294  eirraplem  12303  zdvdsdc  12338  dvdstr  12354  dvdsadd2b  12366  fsumdvds  12368  dvdslelemd  12369  divconjdvds  12375  alzdvds  12380  dvdsext  12381  fzm1ndvds  12382  fzo0dvdseq  12383  3dvds  12390  zeo3  12394  even2n  12400  mod2eq1n2dvds  12405  nn0ehalf  12429  nnehalf  12430  nno  12432  nn0oddm1d2  12435  divalglemnqt  12446  divalglemex  12448  divalglemeuneg  12449  divalg2  12452  divalgmod  12453  flodddiv4t2lthalf  12465  bitsfzolem  12480  bitsfzo  12481  bitsmod  12482  bitsfi  12483  bitscmp  12484  bitsinv1lem  12487  bitsinv1  12488  dvdsbnd  12492  gcdsupex  12493  gcdsupcl  12494  gcddvds  12499  divgcdz  12507  divgcdnn  12511  gcd0id  12515  gcdneg  12518  gcd1  12523  dvdsgcdidd  12530  bezoutlemnewy  12532  bezoutlemstep  12533  bezoutlemmo  12542  bezoutlemsup  12545  dfgcd3  12546  bezout  12547  dfgcd2  12550  mulgcd  12552  sqgcd  12565  dvdssqlem  12566  bezoutr1  12569  uzwodc  12573  nninfctlemfo  12576  lcmval  12600  lcmcllem  12604  dvdslcm  12606  lcmgcdlem  12614  lcmdvds  12616  lcmgcdeq  12620  ncoprmgcdne1b  12626  mulgcddvds  12631  rpmulgcd2  12632  qredeu  12634  rpdvds  12636  prmind2  12657  nprm  12660  dvdsnprmd  12662  isprm5lem  12678  isprm5  12679  divgcdodd  12680  isprm6  12684  prmexpb  12688  pw2dvds  12703  pw2dvdseulemle  12704  oddpwdclemdc  12710  sqne2sq  12714  znege1  12715  sqrt2irraplemnn  12716  divnumden  12733  divdenle  12734  qden1elz  12742  nn0sqrtelqelz  12743  hashdvds  12758  crth  12761  phimullem  12762  eulerthlemfi  12765  eulerthlemh  12768  eulerthlemth  12769  eulerth  12770  prmdiv  12772  prmdiveq  12773  hashgcdlem  12775  dvdsfi  12776  phisum  12778  odzcllem  12780  odzdvds  12783  odzphi  12784  oddprm  12797  pythagtriplem3  12805  pythagtriplem4  12806  pythagtriplem10  12807  pythagtriplem11  12812  pythagtriplem13  12814  pythagtriplem19  12820  pcprendvds  12828  pcprendvds2  12829  pcpre1  12830  pcpremul  12831  pceulem  12832  pceu  12833  pczpre  12835  pcmul  12839  pcdiv  12840  pcqmul  12841  pcqdiv  12845  pcexp  12847  pcidlem  12861  pcneg  12863  pcdvdstr  12865  pcgcd1  12866  pc2dvds  12868  dvdsprmpweq  12873  dvdsprmpweqle  12875  pcaddlem  12877  pcadd  12878  pcadd2  12879  pcmpt  12881  fldivp1  12886  pcfaclem  12887  pcfac  12888  pcbc  12889  qexpz  12890  oddprmdvds  12892  pockthlem  12894  pockthg  12895  infpnlem2  12898  1arith  12905  4sqlem9  12924  4sqlem10  12925  4sqlem11  12939  4sqlem12  12940  4sqlem13m  12941  4sqlem14  12942  4sqlem16  12944  oddennn  12978  ennnfonelemk  12986  ennnfonelemkh  12998  ennnfonelemhf1o  12999  ennnfonelemex  13000  ennnfonelemhom  13001  ennnfonelemrnh  13002  ennnfonelemen  13007  ennnfonelemim  13010  ctinfomlemom  13013  ctiunctlemf  13024  ssnnctlemct  13032  nninfdclemcl  13034  nninfdclemp1  13036  nninfdclemlt  13037  unbendc  13040  prdsbascl  13337  pwselbas  13342  mgmb1mgm1  13416  mgm1  13418  mgmidsssn0  13432  gsumfzval  13439  gsumress  13443  gsum0g  13444  gsumval2  13445  sgrp1  13459  sgrpidmndm  13468  ismndd  13485  prds0g  13497  mhmpropd  13514  resmhm  13535  resmhm2b  13537  gsumwsubmcl  13544  gsumwmhm  13546  isgrpd2e  13568  grpidd2  13589  isgrpinv  13602  grpinvinv  13615  grpidssd  13624  grpinvssd  13625  mulgval  13674  mulgfng  13676  mulgnegnn  13684  subg0  13732  issubg4m  13745  nsgconj  13758  1nsgtrivd  13771  eqgen  13779  eqgcpbl  13780  qus0  13787  ghmid  13801  resghm  13812  ghmnsgpreima  13821  kerf1ghm  13826  conjsubgen  13830  conjnmz  13831  imasabl  13888  rnglz  13923  rngrz  13924  qusrng  13936  issrgid  13959  srg1zr  13965  ringcl  13991  isringid  14003  ringcom  14009  ringpropd  14016  ringlz  14021  ringrz  14022  ring1  14037  opprrng  14055  opprring  14057  dvdsrcld  14076  unitcld  14087  unitmulcl  14092  unitgrp  14095  unitnegcl  14109  rhmmul  14143  isrhm2d  14144  rhmdvdsr  14154  rhmopp  14155  elrhmunit  14156  rhmunitinv  14157  subrgugrp  14219  aprsym  14263  islmodd  14272  lmod0vs  14300  lmodfopne  14305  lmodcom  14312  lssclg  14343  lspsnel5a  14389  lspsneq0b  14406  lsslsp  14408  sraring  14428  sralmod  14429  rspssp  14473  rnglidlmsgrp  14476  2idlcpblrng  14502  gsumfzfsumlem0  14565  zncrng  14624  znzrh2  14625  znzrhfo  14627  znf1o  14630  znfi  14634  znhash  14635  znidom  14636  znidomb  14637  znunit  14638  znrrg  14639  psrbaglesuppg  14651  psrelbas  14654  psrelbasfi  14655  psrgrp  14664  psr0  14665  psr1clfi  14667  mplsubgfilemcl  14678  mplsubgfileminv  14679  ntridm  14815  ntrtop  14817  ntrcls0  14820  ntr0  14823  isopn3i  14824  neiss2  14831  opnneiss  14847  topssnei  14851  cnpf2  14896  icnpimaex  14900  lmcvg  14906  iscnp4  14907  cncnp  14919  cnptopresti  14927  lmfss  14933  lmtopcnp  14939  hmeores  15004  bldisj  15090  xblss2ps  15093  xblss2  15094  blhalf  15097  blssps  15116  blss  15117  ssblex  15120  blpnfctr  15128  xmetresbl  15129  mopni2  15172  bdxmet  15190  bdbl  15192  xmetxpbl  15197  metcnpi  15204  metcnpi2  15205  tgioo  15243  rescncf  15270  mulcncflem  15296  cnopnap  15300  dedekindeulemuub  15306  dedekindeulemloc  15308  dedekindeulemlu  15310  dedekindeu  15312  dedekindicclemuub  15315  dedekindicclemloc  15317  dedekindicclemlu  15319  dedekindicclemicc  15321  dedekindicc  15322  ivthinclemlopn  15325  ivthinclemuopn  15327  ivthdec  15333  ivthreinc  15334  hovergt0  15339  dich0  15341  limcimolemlt  15353  cnplimcim  15356  cnplimclemr  15358  limccnpcntop  15364  limccnp2cntop  15366  limccoap  15367  dvfgg  15377  dvidlemap  15380  dvidrelem  15381  dvidsslem  15382  dvaddxxbr  15390  dvmulxxbr  15391  dvaddxx  15392  dvmulxx  15393  dviaddf  15394  dvimulf  15395  dvcoapbr  15396  dvcjbr  15397  dvcj  15398  dvrecap  15402  dvmptclx  15407  dveflem  15415  elply2  15424  plyf  15426  plyaddlem  15438  plymullem  15439  plycoeid3  15446  plyco  15448  plycj  15450  dvply1  15454  dvply2g  15455  reeff1oleme  15461  eflt  15464  sin0pilem1  15470  pilem3  15472  cosq14gt0  15521  coseq0negpitopi  15525  tangtx  15527  coskpi  15537  cosordlem  15538  cosq34lt1  15539  relogef  15553  logrpap0d  15567  rplogcl  15568  logge0  15569  logdivlti  15570  cxplt3  15609  rpabscxpbnd  15629  dvdsppwf1o  15678  fsumdvdsmul  15680  mersenne  15686  perfect1  15687  perfectlem1  15688  perfectlem2  15689  perfect  15690  lgslem1  15694  lgsval  15698  lgsfvalg  15699  lgsval2lem  15704  lgsvalmod  15713  lgsfcl3  15715  lgsmod  15720  lgsdirprm  15728  lgsdir  15729  lgsdilem2  15730  lgsdi  15731  lgsne0  15732  gausslemma2dlem0i  15751  gausslemma2dlem1a  15752  gausslemma2dlem1f1o  15754  gausslemma2dlem3  15757  gausslemma2dlem4  15758  lgseisenlem1  15764  lgseisenlem2  15765  lgseisenlem3  15766  lgseisenlem4  15767  lgseisen  15768  lgsquadlem1  15771  lgsquadlem2  15772  lgsquadlem3  15773  lgsquad2lem1  15775  lgsquad2lem2  15776  lgsquad3  15778  2lgslem1c  15784  2lgsoddprm  15807  2sqlem3  15811  2sqlem4  15812  2sqlem8  15817  lpvtx  15894  umgrnloopv  15929  umgredgne  15963  ausgrusgrien  15984  wlkcompim  16093  wlkvtxedg  16104  upgr2wlkdc  16116  clwwlkccatlem  16137  bj-charfunr  16228  pw1ndom3lem  16412  2omap  16418  pw1map  16420  pwf1oexmid  16424  subctctexmid  16425  domomsubct  16426  pw1nct  16428  nnsf  16431  peano4nninf  16432  nninfsellemeq  16440  nnnninfex  16448  cvgcmp2nlemabs  16460  iooref1o  16462  trilpolemisumle  16466  trilpolemeq1  16468  trilpolemlt1  16469  trirec0  16472  apdifflemf  16474  apdifflemr  16475  apdiff  16476  iswomninnlem  16477  redcwlpo  16483  redc0  16485  reap0  16486  nconstwlpolemgt0  16492  neapmkvlem  16495  ltlenmkv  16498  supfz  16499  inffz  16500