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  2827  vtoclgft  2852  vtoclegft  2876  elrab3t  2959  eueq2dc  2977  sbceq1dd  3035  csbiedf  3166  sseqtrd  3263  3sstr3d  3269  ifbothdadc  3637  snssd  3816  dfnfc2  3909  breqdi  4101  breqtrd  4112  3brtr3d  4117  csbexga  4215  reuhypd  4566  reg2exmidlema  4630  elirr  4637  en2lp  4650  onsucuni2  4660  finds  4696  iota4  5304  iota4an  5305  funimaexglem  5410  fneu  5433  fco2  5498  fssres2  5511  fresin  5512  feu  5516  f1orescnv  5596  resdif  5602  funcocnv2  5605  f1oprg  5625  fvelrnb  5689  fimacnv  5772  f1oresrab  5808  fsn2  5817  xpsng  5818  funopsn  5825  fnressn  5835  fsnunf  5849  foeqcnvco  5926  isores1  5950  isoini2  5955  riota5f  5993  riotass2  5995  riotass  5996  ovmpodxf  6142  uchoice  6295  elopabi  6355  cnvf1o  6385  smores3  6454  tfrlemisucaccv  6486  tfr1onlemsucaccv  6502  tfrcllemsucaccv  6515  rdgon  6547  frecabcl  6560  frecsuclem  6567  nnsucsssuc  6655  nnsucuniel  6658  erref  6717  iserd  6723  swoer  6725  swoord1  6726  swoord2  6727  erth  6743  erthi  6745  eroveu  6790  pmresg  6840  mapsn  6854  fndmeng  6980  xpen  7026  phplem4  7036  phplem4on  7049  fidifsnen  7052  dif1en  7061  dif1enen  7062  fisbth  7065  diffisn  7075  ac6sfi  7080  fidcen  7081  fimax2gtri  7084  en2eqpr  7092  unsnfidcex  7105  unsnfidcel  7106  prfidceq  7113  fiintim  7116  fidcenumlemrks  7143  elfi2  7162  elfir  7163  fiuni  7168  fifo  7170  eqsupti  7186  supisoti  7200  ordiso2  7225  casef  7278  difinfsnlem  7289  ctmlemr  7298  ctssdccl  7301  enumct  7305  nninfninc  7313  nnnninfeq  7318  nnnninfeq2  7319  enomnilem  7328  exmidomni  7332  fodjum  7336  fodjuomnilemres  7338  mkvprop  7348  enmkvlem  7351  enwomnilem  7359  nninfdcinf  7361  nninfwlpoimlemdc  7367  nninfinfwlpolem  7368  pr1or2  7390  acfun  7412  2omotaplemap  7466  exmidmotap  7470  ccfunen  7473  cc2lem  7475  dfplpq2  7564  ltanqi  7612  ltmnqi  7613  ltaddnq  7617  subhalfnqq  7624  ltbtwnnqq  7625  archnqq  7627  prarloclemarch2  7629  enq0sym  7642  enq0ref  7643  enq0tr  7644  nqnq0pi  7648  nnnq0lem1  7656  distrnq0  7669  prarloclemlt  7703  prarloclemn  7709  prarloclemcalc  7712  genplt2i  7720  addnqprllem  7737  addnqprulem  7738  addlocprlemgt  7744  appdivnq  7773  prmuloc2  7777  ltexprlemopl  7811  ltexprlemopu  7813  ltexprlemru  7822  prplnqu  7830  cauappcvgprlemopl  7856  cauappcvgprlemlol  7857  cauappcvgprlemladdfu  7864  cauappcvgprlemladdrl  7867  cauappcvgprlem1  7869  archrecnq  7873  archrecpr  7874  caucvgprlemk  7875  caucvgprlemnbj  7877  caucvgprlemm  7878  caucvgprlemopl  7879  caucvgprlemlol  7880  caucvgprlemladdfu  7887  caucvgprlemladdrl  7888  caucvgprlem1  7889  caucvgprprlemk  7893  caucvgprprlemnkeqj  7900  caucvgprprlemnbj  7903  caucvgprprlemml  7904  caucvgprprlemmu  7905  caucvgprprlemopl  7907  caucvgprprlemlol  7908  caucvgprprlemopu  7909  caucvgprprlemexbt  7916  caucvgprprlemexb  7917  caucvgprprlem1  7919  caucvgprprlem2  7920  suplocexprlemru  7929  suplocexprlemdisj  7930  suplocexprlemloc  7931  suplocexprlemub  7933  suplocexprlemlub  7934  prsrlem1  7952  addgt0sr  7985  srpospr  7993  prsrriota  7998  caucvgsrlemgt1  8005  caucvgsrlemoffgt1  8009  caucvgsr  8012  mappsrprg  8014  suplocsrlemb  8016  suplocsrlempr  8017  suplocsrlem  8018  recriota  8100  axsuploc  8242  lelttr  8258  ltletr  8259  ltnsymd  8289  lensymd  8291  cnegexlem3  8346  cnegex2  8348  addcanad  8355  addcan2ad  8356  negcon1ad  8475  negne0d  8478  negrebd  8479  subeq0d  8488  subne0ad  8491  neg11d  8492  subcand  8521  subcan2d  8522  ltadd2  8589  ltadd2dd  8592  add20  8644  ltnegcon1d  8695  ltnegcon2d  8696  lenegcon1d  8697  lenegcon2d  8698  subled  8718  lesubd  8719  ltsub23d  8720  ltsub13d  8721  ltadd1dd  8726  ltsub1dd  8727  ltsub2dd  8728  leadd1dd  8729  leadd2dd  8730  lesub1dd  8731  lesub2dd  8732  recexre  8748  apreap  8757  ltmul1a  8761  reapmul1  8765  cru  8772  apreim  8773  mulge0  8789  leltap  8795  negap0d  8801  ltleap  8802  ltapd  8808  ap0gt0  8810  ap0gt0d  8811  mulcanapad  8833  mulcanap2ad  8834  eqnegad  8904  diveqap0d  8967  diveqap1d  8968  divap1d  8971  rec11apd  8981  div11apd  9001  div2subap  9007  recgt0  9020  prodgt0  9022  lemul1a  9028  lemulge12  9037  lt2msq1  9055  lediv12a  9064  recreclt  9070  nn1suc  9152  nnnlt1  9159  nn2ge  9166  nn1gt1  9167  nnrecl  9390  nn0nlt0  9418  elnn0z  9482  nnnle0  9518  nn0negleid  9538  elz2  9541  nn0n0n1ge2b  9549  nnm1ge0  9556  nn0ge0div  9557  zextle  9561  suprzclex  9568  nn0ind-raph  9587  zindd  9588  uzneg  9765  eluzadd  9775  eluzsub  9776  uzm1  9777  uz3m2nn  9797  supminfex  9821  infregelbex  9822  nn01to3  9841  irrmulap  9872  ltrec1d  9942  lerec2d  9943  ledivdivd  9947  divge1  9948  ltmul1dd  9977  ltmul2dd  9978  ltdiv1dd  9979  lediv1dd  9980  ltdiv23d  9982  lediv23d  9983  nn0ledivnn  9992  addlelt  9993  xrlelttr  10031  xrltletr  10032  xaddass2  10095  xltadd1  10101  xlt2add  10105  ixxdisj  10128  icoshftf1o  10216  icodisj  10217  lincmb01cmp  10228  iccf1o  10229  uzsubsubfz  10272  fzdisj  10277  fzopth  10286  fznatpl1  10301  fzsuc2  10304  fzp1disj  10305  fzrev2i  10311  uzdisj  10318  fseq1p1m1  10319  fzm1  10325  fzneuz  10326  fzp1nel  10329  fzrevral  10330  fznn0sub2  10353  fz0fzdiffz0  10355  difelfzle  10359  difelfznle  10360  nn0disj  10363  fzonnsub  10396  fzodisj  10405  fzouzdisj  10407  fzoun  10408  eluzgtdifelfzo  10432  ubmelfzo  10435  fzonn0p1p1  10448  ubmelm1fzo  10461  fzostep1  10473  exfzdc  10476  subfzo0  10478  zsupcllemstep  10479  infssuzex  10483  zsupssdc  10488  qtri3or  10490  exbtwnzlemex  10499  rebtwn2z  10504  qbtwnrelemcalc  10505  qbtwnre  10506  qavgle  10508  apbtwnz  10524  flid  10534  flqwordi  10538  flqmulnn0  10549  flhalf  10552  flltdivnn0lt  10554  fldiv4p1lem1div2  10555  intfracq  10572  flqdiv  10573  flqpmodeq  10579  modqmulnn  10594  mulqaddmodid  10616  modqmuladdim  10619  modqmuladdnn0  10620  m1modge3gt1  10623  q2submod  10637  modaddmodup  10639  modqsubdir  10645  modqeqmodmin  10646  modfzo0difsn  10647  uzennn  10688  uzsinds  10696  monoord2  10738  ser3mono  10739  iseqf1olemqcl  10751  iseqf1olemnab  10753  iseqf1olemab  10754  iseqf1olemqf1o  10758  iseqf1olemqk  10759  seq3f1olemqsumkj  10763  seq3f1olemqsumk  10764  seq3f1olemqsum  10765  seq3f1olemp  10767  seqf1oglem1  10771  seqf1oglem2  10772  ser3le  10789  exp3val  10793  expnegap0  10799  expgt1  10829  ltexp2a  10843  le2sq2  10867  nnlesq  10895  qsqeqor  10902  bernneq  10912  expnbnd  10915  expnlbnd  10916  expnlbnd2  10917  expeq0d  10921  sq11d  10958  nn0ltexp2  10961  expcand  10969  nn0opthd  10974  facdiv  10990  faclbnd6  10996  facubnd  10997  facavg  10998  bcval4  11004  bcp1nk  11014  bcval5  11015  bcpasc  11018  hashennnuni  11031  isfinite4im  11044  hashnncl  11047  hashunlem  11057  fiprsshashgt1  11071  hashfzp1  11078  zfz1isolemiso  11093  seq3coll  11096  hash2en  11097  iswrdiz  11110  wrdffz  11124  ffz0iswrdnn0  11130  ccatval21sw  11172  ccatass  11175  ccatalpha  11180  swrdf  11226  swrdlend  11229  ccatswrd  11241  swrdccat2  11242  pfxsuffeqwrdeq  11269  ccatpfx  11272  ccats1pfxeq  11285  cats1un  11292  wrdind  11293  wrd2ind  11294  pfxccatin12  11304  swrdccat  11306  s2dmg  11361  seq3shft  11389  cjth  11397  cjdivap  11460  cjne0d  11498  cjap0d  11499  cvg1nlemcxze  11533  cvg1nlemcau  11535  cvg1nlemres  11536  recvguniq  11546  resqrexlemover  11561  resqrexlemdecn  11563  resqrexlemlo  11564  resqrexlemcalc2  11566  resqrexlemcalc3  11567  resqrexlemnmsq  11568  resqrexlemnm  11569  resqrexlemcvg  11570  resqrexlemglsq  11573  resqrexlemga  11574  leabs  11625  absrele  11634  nn0abscl  11636  ltabs  11638  abslt  11639  absle  11640  abstri  11655  amgm2  11669  sqr11d  11724  abs00d  11737  maxabsle  11755  maxabslemlub  11758  maxleastlt  11766  maxltsup  11769  2zsupmax  11777  minmax  11781  2zinfmin  11794  xrmaxleim  11795  xrmaxiflemlub  11799  xrmaxiflemcom  11800  xrmaxiflemval  11801  xrmaxleastlt  11807  xrmaxltsup  11809  xrmaxaddlem  11811  xrmaxadd  11812  xrminmax  11816  xrmin1inf  11818  xrmin2inf  11819  xrmineqinf  11820  climi  11838  reccn2ap  11864  climge0  11876  climle  11885  climserle  11896  climrecvg1n  11899  fz1f1o  11926  summodclem3  11931  summodclem2a  11932  summodc  11934  fisumss  11943  fsum0diaglem  11991  mptfzshft  11993  fsumrev  11994  fisum0diag2  11998  fsumlessfi  12011  fsumle  12014  fsumlt  12015  isumsplit  12042  isumrpcl  12045  expcnvap0  12053  geosergap  12057  pwm1geoserap1  12059  absgtap  12061  geolim  12062  geolim2  12063  georeclim  12064  geoisumr  12069  geoisum1c  12071  cvgratnnlembern  12074  cvgratnnlemseq  12077  cvgratnnlemsumlt  12079  cvgratnnlemfm  12080  cvgratnnlemrate  12081  cvgratnn  12082  cvgratz  12083  mertenslemub  12085  mertenslemi1  12086  mertenslem2  12087  mertensabs  12088  prodmodclem2a  12127  prodmodc  12129  zproddc  12130  fprodntrivap  12135  fprodf1o  12139  fprodssdc  12141  fprodsplitdc  12147  fprodrev  12170  fprodmodd  12192  efcllemp  12209  ege2le3  12222  eftlcvg  12238  eftlub  12241  efltim  12249  eflegeo  12252  tanaddap  12290  sinbnd  12303  cosbnd  12304  sin01bnd  12308  cos01bnd  12309  sinltxirr  12312  sin01gt0  12313  cos01gt0  12314  cos12dec  12319  eirraplem  12328  zdvdsdc  12363  dvdstr  12379  dvdsadd2b  12391  fsumdvds  12393  dvdslelemd  12394  divconjdvds  12400  alzdvds  12405  dvdsext  12406  fzm1ndvds  12407  fzo0dvdseq  12408  3dvds  12415  zeo3  12419  even2n  12425  mod2eq1n2dvds  12430  nn0ehalf  12454  nnehalf  12455  nno  12457  nn0oddm1d2  12460  divalglemnqt  12471  divalglemex  12473  divalglemeuneg  12474  divalg2  12477  divalgmod  12478  flodddiv4t2lthalf  12490  bitsfzolem  12505  bitsfzo  12506  bitsmod  12507  bitsfi  12508  bitscmp  12509  bitsinv1lem  12512  bitsinv1  12513  dvdsbnd  12517  gcdsupex  12518  gcdsupcl  12519  gcddvds  12524  divgcdz  12532  divgcdnn  12536  gcd0id  12540  gcdneg  12543  gcd1  12548  dvdsgcdidd  12555  bezoutlemnewy  12557  bezoutlemstep  12558  bezoutlemmo  12567  bezoutlemsup  12570  dfgcd3  12571  bezout  12572  dfgcd2  12575  mulgcd  12577  sqgcd  12590  dvdssqlem  12591  bezoutr1  12594  uzwodc  12598  nninfctlemfo  12601  lcmval  12625  lcmcllem  12629  dvdslcm  12631  lcmgcdlem  12639  lcmdvds  12641  lcmgcdeq  12645  ncoprmgcdne1b  12651  mulgcddvds  12656  rpmulgcd2  12657  qredeu  12659  rpdvds  12661  prmind2  12682  nprm  12685  dvdsnprmd  12687  isprm5lem  12703  isprm5  12704  divgcdodd  12705  isprm6  12709  prmexpb  12713  pw2dvds  12728  pw2dvdseulemle  12729  oddpwdclemdc  12735  sqne2sq  12739  znege1  12740  sqrt2irraplemnn  12741  divnumden  12758  divdenle  12759  qden1elz  12767  nn0sqrtelqelz  12768  hashdvds  12783  crth  12786  phimullem  12787  eulerthlemfi  12790  eulerthlemh  12793  eulerthlemth  12794  eulerth  12795  prmdiv  12797  prmdiveq  12798  hashgcdlem  12800  dvdsfi  12801  phisum  12803  odzcllem  12805  odzdvds  12808  odzphi  12809  oddprm  12822  pythagtriplem3  12830  pythagtriplem4  12831  pythagtriplem10  12832  pythagtriplem11  12837  pythagtriplem13  12839  pythagtriplem19  12845  pcprendvds  12853  pcprendvds2  12854  pcpre1  12855  pcpremul  12856  pceulem  12857  pceu  12858  pczpre  12860  pcmul  12864  pcdiv  12865  pcqmul  12866  pcqdiv  12870  pcexp  12872  pcidlem  12886  pcneg  12888  pcdvdstr  12890  pcgcd1  12891  pc2dvds  12893  dvdsprmpweq  12898  dvdsprmpweqle  12900  pcaddlem  12902  pcadd  12903  pcadd2  12904  pcmpt  12906  fldivp1  12911  pcfaclem  12912  pcfac  12913  pcbc  12914  qexpz  12915  oddprmdvds  12917  pockthlem  12919  pockthg  12920  infpnlem2  12923  1arith  12930  4sqlem9  12949  4sqlem10  12950  4sqlem11  12964  4sqlem12  12965  4sqlem13m  12966  4sqlem14  12967  4sqlem16  12969  oddennn  13003  ennnfonelemk  13011  ennnfonelemkh  13023  ennnfonelemhf1o  13024  ennnfonelemex  13025  ennnfonelemhom  13026  ennnfonelemrnh  13027  ennnfonelemen  13032  ennnfonelemim  13035  ctinfomlemom  13038  ctiunctlemf  13049  ssnnctlemct  13057  nninfdclemcl  13059  nninfdclemp1  13061  nninfdclemlt  13062  unbendc  13065  prdsbascl  13362  pwselbas  13367  mgmb1mgm1  13441  mgm1  13443  mgmidsssn0  13457  gsumfzval  13464  gsumress  13468  gsum0g  13469  gsumval2  13470  sgrp1  13484  sgrpidmndm  13493  ismndd  13510  prds0g  13522  mhmpropd  13539  resmhm  13560  resmhm2b  13562  gsumwsubmcl  13569  gsumwmhm  13571  isgrpd2e  13593  grpidd2  13614  isgrpinv  13627  grpinvinv  13640  grpidssd  13649  grpinvssd  13650  mulgval  13699  mulgfng  13701  mulgnegnn  13709  subg0  13757  issubg4m  13770  nsgconj  13783  1nsgtrivd  13796  eqgen  13804  eqgcpbl  13805  qus0  13812  ghmid  13826  resghm  13837  ghmnsgpreima  13846  kerf1ghm  13851  conjsubgen  13855  conjnmz  13856  imasabl  13913  rnglz  13948  rngrz  13949  qusrng  13961  issrgid  13984  srg1zr  13990  ringcl  14016  isringid  14028  ringcom  14034  ringpropd  14041  ringlz  14046  ringrz  14047  ring1  14062  opprrng  14080  opprring  14082  dvdsrcld  14101  unitcld  14112  unitmulcl  14117  unitgrp  14120  unitnegcl  14134  rhmmul  14168  isrhm2d  14169  rhmdvdsr  14179  rhmopp  14180  elrhmunit  14181  rhmunitinv  14182  subrgugrp  14244  aprsym  14288  islmodd  14297  lmod0vs  14325  lmodfopne  14330  lmodcom  14337  lssclg  14368  lspsnel5a  14414  lspsneq0b  14431  lsslsp  14433  sraring  14453  sralmod  14454  rspssp  14498  rnglidlmsgrp  14501  2idlcpblrng  14527  gsumfzfsumlem0  14590  zncrng  14649  znzrh2  14650  znzrhfo  14652  znf1o  14655  znfi  14659  znhash  14660  znidom  14661  znidomb  14662  znunit  14663  znrrg  14664  psrbaglesuppg  14676  psrelbas  14679  psrelbasfi  14680  psrgrp  14689  psr0  14690  psr1clfi  14692  mplsubgfilemcl  14703  mplsubgfileminv  14704  ntridm  14840  ntrtop  14842  ntrcls0  14845  ntr0  14848  isopn3i  14849  neiss2  14856  opnneiss  14872  topssnei  14876  cnpf2  14921  icnpimaex  14925  lmcvg  14931  iscnp4  14932  cncnp  14944  cnptopresti  14952  lmfss  14958  lmtopcnp  14964  hmeores  15029  bldisj  15115  xblss2ps  15118  xblss2  15119  blhalf  15122  blssps  15141  blss  15142  ssblex  15145  blpnfctr  15153  xmetresbl  15154  mopni2  15197  bdxmet  15215  bdbl  15217  xmetxpbl  15222  metcnpi  15229  metcnpi2  15230  tgioo  15268  rescncf  15295  mulcncflem  15321  cnopnap  15325  dedekindeulemuub  15331  dedekindeulemloc  15333  dedekindeulemlu  15335  dedekindeu  15337  dedekindicclemuub  15340  dedekindicclemloc  15342  dedekindicclemlu  15344  dedekindicclemicc  15346  dedekindicc  15347  ivthinclemlopn  15350  ivthinclemuopn  15352  ivthdec  15358  ivthreinc  15359  hovergt0  15364  dich0  15366  limcimolemlt  15378  cnplimcim  15381  cnplimclemr  15383  limccnpcntop  15389  limccnp2cntop  15391  limccoap  15392  dvfgg  15402  dvidlemap  15405  dvidrelem  15406  dvidsslem  15407  dvaddxxbr  15415  dvmulxxbr  15416  dvaddxx  15417  dvmulxx  15418  dviaddf  15419  dvimulf  15420  dvcoapbr  15421  dvcjbr  15422  dvcj  15423  dvrecap  15427  dvmptclx  15432  dveflem  15440  elply2  15449  plyf  15451  plyaddlem  15463  plymullem  15464  plycoeid3  15471  plyco  15473  plycj  15475  dvply1  15479  dvply2g  15480  reeff1oleme  15486  eflt  15489  sin0pilem1  15495  pilem3  15497  cosq14gt0  15546  coseq0negpitopi  15550  tangtx  15552  coskpi  15562  cosordlem  15563  cosq34lt1  15564  relogef  15578  logrpap0d  15592  rplogcl  15593  logge0  15594  logdivlti  15595  cxplt3  15634  rpabscxpbnd  15654  dvdsppwf1o  15703  fsumdvdsmul  15705  mersenne  15711  perfect1  15712  perfectlem1  15713  perfectlem2  15714  perfect  15715  lgslem1  15719  lgsval  15723  lgsfvalg  15724  lgsval2lem  15729  lgsvalmod  15738  lgsfcl3  15740  lgsmod  15745  lgsdirprm  15753  lgsdir  15754  lgsdilem2  15755  lgsdi  15756  lgsne0  15757  gausslemma2dlem0i  15776  gausslemma2dlem1a  15777  gausslemma2dlem1f1o  15779  gausslemma2dlem3  15782  gausslemma2dlem4  15783  lgseisenlem1  15789  lgseisenlem2  15790  lgseisenlem3  15791  lgseisenlem4  15792  lgseisen  15793  lgsquadlem1  15796  lgsquadlem2  15797  lgsquadlem3  15798  lgsquad2lem1  15800  lgsquad2lem2  15801  lgsquad3  15803  2lgslem1c  15809  2lgsoddprm  15832  2sqlem3  15836  2sqlem4  15837  2sqlem8  15842  lpvtx  15920  umgrnloopv  15955  umgredgne  15989  ausgrusgrien  16010  uhgr0vusgr  16077  usgr1vr  16087  wlkcompim  16149  wlkvtxedg  16160  upgr2wlkdc  16172  clwwlkccatlem  16195  clwwlknp  16212  clwwlkext2edg  16217  bj-charfunr  16341  pw1ndom3lem  16524  2omap  16530  pw1map  16532  pwf1oexmid  16536  subctctexmid  16537  domomsubct  16538  pw1nct  16540  nnsf  16543  peano4nninf  16544  nninfsellemeq  16552  nnnninfex  16560  cvgcmp2nlemabs  16572  iooref1o  16574  trilpolemisumle  16578  trilpolemeq1  16580  trilpolemlt1  16581  trirec0  16584  apdifflemf  16586  apdifflemr  16587  apdiff  16588  iswomninnlem  16589  redcwlpo  16595  redc0  16597  reap0  16598  nconstwlpolemgt0  16604  neapmkvlem  16607  ltlenmkv  16610  supfz  16611  inffz  16612