Theorem mpbird 167

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

Hypotheses

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

Assertion

Ref	Expression
mpbird	|- ( ph -> ps )

Proof of Theorem mpbird

Step	Hyp	Ref	Expression
1		mpbird.min	. 2 |- ( ph -> ch )
2		mpbird.maj	. . 3 |- ( ph -> ( ps <-> ch ) )
3	2	biimprd 158	. 2 |- ( ph -> ( ch -> ps ) )
4	1, 3	mpd 13	1 |- ( ph -> ps )

Syntax hints:   -> wi 4   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpbiri  168  pm5.19  711  pm4.55dc  944  mpbir2and  950  pm3.12dc  964  mpbir3and  1204  pm5.15dc  1431  eqeltrd  2306  eqnetrd  2424  3netr4d  2433  r19.30dc  2678  raleqtrrdv  2738  rexeqtrrdv  2739  sbcne12g  3142  eqsstrd  3260  3sstr4d  3269  eqbrtrd  4105  3brtr4d  4115  snelpwi  4297  prelpwi  4300  pwel  4304  ordelon  4474  onin  4477  elelsuc  4500  onsuc  4593  onsucb  4595  onintonm  4609  omsinds  4714  sosng  4792  relssdv  4811  eqbrrdv  4816  eqrelrdv2  4818  relsnopg  4823  breldmg  4929  elrnmptdv  4978  iss  5051  xpimasn  5177  elxp4  5216  elxp5  5217  iotam  5310  funssres  5360  f0rn0  5520  fimadmfo  5557  sefvex  5648  fdmeu  5677  fvun1  5700  eqfnfvd  5735  fvimacnvi  5749  fvimacnv  5750  fvelrn  5766  fmpt3d  5791  fmpt2d  5797  resflem  5799  fmptco  5801  fsn  5807  funopsn  5817  ftpg  5823  fconst2g  5854  funfvima3  5873  elabrexg  5882  foeqcnvco  5914  f1eqcocnv  5915  fliftfun  5920  fliftfund  5921  fliftval  5924  riota5f  5981  f1ofveu  5989  f1ocnvd  6208  f1opw2  6212  off  6231  offval2  6234  ofrfval2  6235  offveq  6239  caofref  6243  caofinvl  6244  elxp6  6315  cnvf1olem  6370  f2ndf  6372  f1od2  6381  tposf12  6415  smores2  6440  tfrlemisucaccv  6471  tfrlemibfn  6474  tfr1onlemsucaccv  6487  tfr1onlembfn  6490  tfrcllemsucaccv  6500  tfrcllembfn  6503  tfrcl  6510  tfri3  6513  frecabcl  6545  nnsucsssuc  6638  ersym  6692  ertr  6695  swoer  6708  erth  6726  riinerm  6755  qliftfund  6765  eroprf  6775  ecopoverg  6783  th3qlem1  6784  elmapssres  6820  mapss  6838  fdiagfn  6839  ixpssmap2g  6874  mapsnf1o  6884  f1oen4g  6903  f1dom4g  6904  f1dom2g  6907  dom3d  6925  en2prd  6970  dom1oi  6978  pw2f1odclem  6995  fopwdom  6997  mapxpen  7009  nndomo  7025  dif1en  7041  findcard2  7051  findcard2s  7052  diffisn  7055  fimax2gtrilemstep  7062  fientri3  7077  tpfidceq  7092  fiintim  7093  opabfi  7100  f1dmvrnfibi  7111  sbthlemi6  7129  elfir  7140  fifo  7147  supelti  7169  supsnti  7172  cnvinfex  7185  ordiso2  7202  updjud  7249  djudom  7260  difinfsn  7267  ctssdc  7280  enumctlemm  7281  enumct  7282  nninfninc  7290  enomnilem  7305  fodjuf  7312  ismkvnex  7322  omnimkv  7323  enmkvlem  7328  enwomnilem  7336  nninfdcinf  7338  nninfwlporlem  7340  isnumi  7354  exmidfodomrlemrALT  7381  finacn  7386  djudoml  7401  djudomr  7402  netap  7440  2omotaplemap  7443  2omotaplemst  7444  exmidapne  7446  cc2lem  7452  cc3  7454  ltsopi  7507  pitri3or  7509  ltdcpi  7510  indpi  7529  enqdc  7548  enqdc1  7549  addcmpblnq  7554  mulcanenq  7572  recrecnq  7581  nqtri3or  7583  ltdcnq  7584  ltsonq  7585  ltaddnq  7594  subhalfnqq  7601  archnqq  7604  prarloclemarch2  7606  enq0tr  7621  nqnq0  7628  addcmpblnq0  7630  mulcanenq0ec  7632  nnnq0lem1  7633  nqpnq0nq  7640  nq0m0r  7643  nq02m  7652  prarloclemlt  7680  prarloclemcalc  7689  addlocpr  7723  nqprl  7738  nqpru  7739  addnqprlemrl  7744  addnqprlemru  7745  prmuloclemcalc  7752  mullocprlem  7757  mulnqprlemrl  7760  mulnqprlemru  7761  1idprl  7777  1idpru  7778  ltaddpr  7784  ltexprlemm  7787  ltexprlemopl  7788  ltexprlemopu  7790  ltexprlemdisj  7793  ltexprlemrl  7797  ltexprlemru  7799  addcanprleml  7801  addcanprlemu  7802  addcanprg  7803  prplnqu  7807  recexprlemloc  7818  recexprlem1ssl  7820  recexprlem1ssu  7821  aptiprleml  7826  aptiprlemu  7827  archpr  7830  cauappcvgprlemm  7832  cauappcvgprlemopl  7833  cauappcvgprlemloc  7839  cauappcvgprlemladdfu  7841  cauappcvgprlemladdfl  7842  cauappcvgprlem1  7846  cauappcvgprlem2  7847  caucvgprlemnkj  7853  caucvgprlemopl  7856  caucvgprlemloc  7862  caucvgprlemladdfu  7864  caucvgprlem2  7867  caucvgprprlemnkltj  7876  caucvgprprlemopl  7884  caucvgprprlemloc  7890  caucvgprprlemexbt  7893  caucvgprprlemaddq  7895  caucvgprprlem2  7897  suplocexprlemmu  7905  suplocexprlemru  7906  suplocexprlemloc  7908  suplocexprlemlub  7911  prsrlem1  7929  0idsr  7954  1idsr  7955  recexgt0sr  7960  archsr  7969  prsradd  7973  caucvgsrlemcau  7980  caucvgsrlembound  7981  caucvgsrlemoffgt1  7986  suplocsrlemb  7993  suplocsrlempr  7994  suplocsrlem  7995  pitonnlem1p1  8033  pitonn  8035  pitoregt0  8036  peano2nnnn  8040  recidpirq  8045  axcaucvglemval  8084  leid  8230  nltled  8267  readdcan  8286  addneintrd  8334  addneintr2d  8335  pncan  8352  subsub2  8374  subsub4  8379  negned  8454  subne0d  8466  subneintrd  8501  subneintr2d  8503  subeq0bd  8525  subdi  8531  gt0add  8720  rimul  8732  rereim  8733  ltmul1a  8738  apreim  8750  apirr  8752  mulap0r  8762  msqge0  8763  mulge0  8766  gt0ap0  8773  ltap  8780  subap0d  8791  recexaplem2  8799  mulap0bad  8806  mulap0bbd  8807  mul0eqap  8817  divrecap  8835  div0ap  8849  div1  8850  recrecap  8856  divdivdivap  8860  ddcanap  8873  rerecclap  8877  div2negap  8882  diveqap1bd  8983  recgt0  8997  prodgt0  8999  lemul1a  9005  recp1lt1  9046  squeeze0  9051  peano2nn  9122  div4p1lem1div2  9365  arch  9366  peano2z  9482  peano2zm  9484  ztri3or  9489  nn0n0n1ge2  9517  zextle  9538  gtndiv  9542  suprzclex  9545  nn0ind-raph  9564  uzid  9736  uzneg  9741  uztric  9744  uz11  9745  eluzp1l  9747  qdivcl  9838  irrmul  9842  irrmulap  9843  rpnegap  9882  negelrpd  9884  ledivge1le  9922  mul2lt0rlt0  9955  mul2lt0rgt0  9956  nn0ledivnn  9963  ltpnf  9976  mnflt  9979  pnfge  9985  mnfle  9988  xrlttr  9991  xrltso  9992  xrlttri3  9993  xrleid  9996  xaddass2  10066  xltadd1  10072  xlt2add  10076  xleaddadd  10083  iccf1o  10200  fztri3or  10235  fznlem  10237  fzn  10238  fzsplit2  10246  fznatpl1  10272  uzsplit  10288  fseq1p1m1  10290  fzm1  10296  fznn0sub2  10324  difelfznle  10331  1fv  10335  fzodcel  10349  fzospliti  10374  fzouzsplit  10377  eluzgtdifelfzo  10403  exfzdc  10446  subfzo0  10448  zsupcllemstep  10449  zsupcl  10451  zssinfcl  10452  infssuzex  10453  infssuzcldc  10455  suprzubdc  10456  nninfdcex  10457  qdcle  10466  exbtwnz  10470  qbtwnrelemcalc  10475  flqlelt  10496  qfraclt1  10500  qfracge0  10501  flqltnz  10507  btwnzge0  10520  flhalf  10522  fldiv4lem1div2uz2  10526  ceiqle  10535  intfracq  10542  mulqmod0  10552  modqge0  10554  modqlt  10555  modqid  10571  modqid0  10572  m1modge3gt1  10593  modqltm1p1mod  10598  q2txmodxeq0  10606  modaddmodlo  10610  modsumfzodifsn  10618  addmodlteq  10620  frecuzrdgtcl  10634  frecuzrdgtclt  10643  uzennn  10658  uzsinds  10666  seqf  10686  seqf2  10690  monoord2  10708  iseqf1olemqk  10729  iseqf1olemjpcl  10730  iseqf1olemqpcl  10731  seq3f1olemqsumkj  10733  seq3f1olemqsum  10735  seq3f1olemstep  10736  seq3f1oleml  10738  seqf1oglem1  10741  ser3le  10759  exp3vallem  10762  exp3val  10763  expp1  10768  expcllem  10772  ltexp2a  10813  leexp2a  10814  nn0ltexp2  10931  faclbnd  10963  faclbnd2  10964  faclbnd3  10965  bcval5  10985  bcpasc  10988  hashennn  11002  fihasheqf1oi  11009  hashsng  11020  fihashfn  11022  hashun  11027  fihashss  11038  fihashssdif  11040  hashfz  11043  hashxp  11048  fimaxq  11049  zfz1isolem1  11062  seq3coll  11064  hashdmprop2dom  11066  wrdf  11077  wrdlenge2n0  11107  fstwrdne0  11111  wrdred1hash  11115  ccatvalfn  11136  ccatsymb  11137  ccatlid  11141  ccatrid  11142  ccatrn  11144  eqs1  11161  ccats1val2  11171  fzowrddc  11179  swrdlen  11184  swrdnd  11191  swrd0g  11192  swrdfv2  11195  swrdwrdsymbg  11196  pfxn0  11220  pfxwrdsymbg  11222  pfxsuff1eqwrdeq  11231  swrdswrd  11237  ccats1pfxeq  11246  ccats1pfxeqrex  11247  wrdind  11254  wrd2ind  11255  swrdccatin1  11257  pfxccatin12lem4  11258  swrdccatin2  11261  pfxccatin12  11265  pfxccat3a  11270  swrdccat3blem  11271  pfxccatid  11273  swrdccatin2d  11276  shftfn  11335  cjth  11357  cjmulrcl  11398  reim0bd  11455  rerebd  11456  cjrebd  11457  caucvgre  11492  cvg1nlemcxze  11493  cvg1nlemcau  11495  cvg1nlemres  11496  recvguniq  11506  resqrexlemover  11521  resqrexlemdec  11522  resqrexlemgt0  11531  resqrexlemoverl  11532  resqrexlemglsq  11533  rersqrtthlem  11541  sqrtgt0  11545  leabs  11585  absexpzap  11591  absle  11600  recvalap  11608  abstri  11615  abs2dif  11617  amgm2  11629  absne0d  11698  maxleim  11716  maxabslemab  11717  maxabslemlub  11718  maxltsup  11729  zmaxcl  11735  fimaxre2  11738  minmax  11741  rpmincl  11749  bdtrilem  11750  bdtri  11751  xrmaxleim  11755  xrmaxiflemcom  11760  xrmaxltsup  11769  xrmaxadd  11772  xrminmax  11776  xrminrpcl  11785  climconst  11801  climuni  11804  2clim  11812  climcn1  11819  climcn2  11820  reccn2ap  11824  climge0  11836  climle  11845  climsqz  11846  climsqz2  11847  serf0  11863  summodclem3  11891  summodclem2a  11892  fsumcl2lem  11909  sumpr  11924  sumtp  11925  fsum0diaglem  11951  mptfzshft  11953  fsumle  11974  fsumlt  11975  divcnv  12008  trireciplem  12011  expcnvap0  12013  expcnv  12015  explecnv  12016  geosergap  12017  cvgratnnlembern  12034  cvgratnnlemabsle  12038  cvgratnnlemsumlt  12039  cvgratz  12043  cvgratgt0  12044  mertenslemi1  12046  mertenslem2  12047  mertensabs  12048  clim2divap  12051  prodmodclem3  12086  prodmodclem2a  12087  fprodseq  12094  fprodmul  12102  fprodfac  12126  fprodconst  12131  fprodap0  12132  fprodap0f  12147  fprodle  12151  eftcl  12165  ef0lem  12171  efsub  12192  eftlub  12201  eflegeo  12212  tanval2ap  12224  sinadd  12247  cos2t  12261  cos2tsin  12262  sin01bnd  12268  cos01bnd  12269  eirraplem  12288  dvdsval2  12301  dvdsdc  12309  dvds0lem  12312  zdvdsdc  12323  dvdscmulr  12331  dvdsmulcr  12332  fsumdvds  12353  dvdslelemd  12354  divconjdvds  12360  dvdsext  12366  fzm1ndvds  12367  dvdsmod  12373  3dvds  12375  oexpneg  12388  2tp1odd  12395  mulsucdiv2z  12396  2teven  12398  zeo5  12399  opeo  12408  omeo  12409  nn0ob  12419  divalglemnqt  12431  bitsdc  12458  bits0o  12461  bitsfzolem  12465  bitsfzo  12466  bitsmod  12467  bitscmp  12469  bitsinv1lem  12472  gcddvds  12484  dvdslegcd  12485  gcdneg  12503  bezoutlemnewy  12517  bezoutlemstep  12518  bezoutlema  12520  bezoutlemb  12521  bezoutlemmo  12527  bezoutlemle  12529  bezoutlemsup  12530  dfgcd3  12531  bezout  12532  dfgcd2  12535  uzwodc  12558  lcmcllem  12589  lcmneg  12596  lcmgcdlem  12599  lcmdvds  12601  lcmid  12602  3lcm2e6woprm  12608  6lcm4e12  12609  ncoprmgcdne1b  12611  mulgcddvds  12616  divgcdcoprmex  12624  cncongr1  12625  cncongr2  12626  isprm2lem  12638  prmind2  12642  dvdsnprmd  12647  prm2orodd  12648  sqnprm  12658  isprm5lem  12663  rpexp  12675  sqrt2irrlem  12683  oddpwdclemdc  12695  sqrt2irraplemnn  12701  qnumdencoprm  12715  qeqnumdivden  12716  nn0gcdsq  12722  nn0sqrtelqelz  12728  nonsq  12729  phicl2  12736  phibnd  12739  hashdvds  12743  phiprmpw  12744  phimullem  12747  eulerthlemrprm  12751  eulerthlema  12752  eulerthlemth  12754  prmdiveq  12758  hashgcdlem  12760  odzdvds  12768  modprminv  12772  nnnn0modprm0  12778  modprmn0modprm0  12779  pythagtriplem10  12792  pythagtriplem19  12805  pythagtrip  12806  pcpre1  12815  pcpremul  12816  pceu  12818  pcmul  12824  pcdiv  12825  pcqmul  12826  pcqdiv  12830  pcexp  12832  pcdvdsb  12843  pcidlem  12846  pcdvdstr  12850  pcgcd1  12851  pc2dvds  12853  pcprmpw2  12856  difsqpwdvds  12861  pcaddlem  12862  pcadd  12863  pcadd2  12864  pcmpt  12866  pcmptdvds  12868  pcprod  12869  fldivp1  12871  pcfaclem  12872  pcfac  12873  pcbc  12874  qexpz  12875  pockthlem  12879  pockthg  12880  1arithlem4  12889  1arith  12890  1arith2  12891  4sqlem6  12906  4sqlem8  12908  4sqlem9  12909  4sqlem10  12910  4sqexercise1  12921  4sqexercise2  12922  4sqlemsdc  12923  4sqlem11  12924  4sqlem12  12925  4sqlem15  12928  4sqlem16  12929  4sqlem17  12930  znnen  12969  ennnfonelemk  12971  ennnfonelemkh  12983  ennnfonelemhf1o  12984  ennnfonelemrnh  12987  ennnfonelemfun  12988  ennnfonelemf1  12989  ennnfonelemrn  12990  ennnfonelemnn0  12993  ctinfomlemom  12998  ctiunctlemudc  13008  unct  13013  omctfn  13014  ssnnctlemct  13017  nninfdclemp1  13021  nninfdc  13024  structfung  13049  setsfun  13067  setsfun0  13068  setscom  13072  strslfv3  13078  setsslid  13083  pwsdiagel  13330  pwssnf1o  13331  imasaddfnlemg  13347  imasaddvallemg  13348  mgmsscl  13394  plusffng  13398  mgmplusf  13399  mgm0  13402  mgm1  13403  opifismgmdc  13404  gsumfzval  13424  gsumprval  13432  sgrp1  13444  issgrpd  13445  prdsplusgsgrpcl  13447  mndpfo  13471  mndfo  13472  prdsplusgcl  13479  prdsidlem  13480  mnd1  13488  0subm  13517  mhmima  13524  grpinvfng  13577  isgrpinv  13587  grpinvid  13593  grpinvf1o  13603  grpinvadd  13611  grpsubf  13612  grpsubsub4  13626  grplactcnv  13635  grp1  13639  grp1inv  13640  prdsinvlem  13641  prdsinvgd  13643  qusgrp2  13650  mulgfng  13661  subginv  13718  resgrpisgrp  13732  subgintm  13735  0subg  13736  0nsg  13751  qusinv  13773  ghminv  13787  ghmrn  13794  ghmeql  13804  ghmnsgima  13805  kerf1ghm  13811  conjnmz  13816  rngass  13902  rngmneg1  13910  rngmneg2  13911  qusrng  13921  srgideu  13935  srgidmlem  13941  srgpcomp  13953  srg1expzeq1  13958  ringcl  13976  ringideu  13980  ringidmlem  13985  ringnegl  14014  ringnegr  14015  ring1  14022  qusring2  14029  opprringbg  14043  dvdsrd  14058  dvdsr01  14068  isunitd  14070  unitinvcl  14087  unitinvinv  14088  unitnegcl  14094  rhmmul  14128  rhmf1o  14132  nzrunit  14152  lringuplu  14160  subrngintm  14176  subrgsubm  14198  subrgintm  14207  aprsym  14248  scaffng  14273  lmodscaf  14274  lsssn0  14334  lss1d  14347  lssintclm  14348  lspval  14354  lspcl  14355  lspsnid  14371  lspprid1  14375  lspsn  14380  sraval  14401  rspcl  14455  rspssid  14456  rspssp  14458  rnglidlmmgm  14460  rnglidlmsgrp  14461  cnfldneg  14537  zringinvg  14568  expghmap  14571  znzrhfo  14612  znf1o  14615  znhash  14620  znidomb  14622  znrrg  14624  psrbagfi  14637  psraddcl  14644  psr0cl  14645  psrnegcl  14647  psrneg  14651  psr1clfi  14652  mplsubgfilemm  14662  mplsubgfilemcl  14663  baspartn  14724  eltg3i  14730  tgclb  14739  topbas  14741  2basgeng  14756  topcld  14783  0cld  14786  uncld  14787  neif  14815  elnei  14826  0nei  14840  restbasg  14842  iscnp4  14892  cnpnei  14893  cnclima  14897  cncnp  14904  cnrest2r  14911  cndis  14915  lmff  14923  lmtopcnp  14924  txbas  14932  txopn  14939  txcnp  14945  upxp  14946  txdis1cn  14952  cnmpt11  14957  cnmpt21  14965  psmetge0  15005  xmetge0  15039  xmettpos  15044  xmetrtri  15050  metrtri  15051  xblpnfps  15072  xblpnf  15073  blfps  15083  blf  15084  ssblps  15099  ssbl  15100  blbas  15107  metss2  15172  xmettxlem  15183  xmettx  15184  qtopbas  15196  divcnap  15239  cncfss  15257  cdivcncfap  15278  expcncf  15283  cnopnap  15285  maxcncf  15289  mincncf  15290  dedekindeulemuub  15291  dedekindeulemlu  15295  dedekindeu  15297  suplociccex  15299  dedekindicclemuub  15300  dedekindicclemlu  15304  dedekindicclemicc  15306  ivthinclemlopn  15310  ivthinclemuopn  15312  ivthinc  15317  ivthreinc  15319  hoverlt1  15323  ellimc3apf  15334  limcimolemlt  15338  limcimo  15339  limcresi  15340  cnplimclemle  15342  reldvg  15353  dvfgg  15362  dvidlemap  15365  dvidrelem  15366  dvidsslem  15367  dvcjbr  15382  dvcj  15383  dvrecap  15387  dveflem  15400  dvef  15401  elply2  15409  elplyr  15414  plycj  15435  plyreres  15438  reeff1oleme  15446  pilem3  15457  sinq34lt0t  15505  cosq14gt0  15506  coseq0q4123  15508  tangtx  15512  sincosq1eq  15513  cosordlem  15523  logdivlti  15555  relogbval  15625  relogbzcl  15626  nnlogbexp  15633  logbgcd1irr  15641  logbgcd1irraplemexp  15642  logbgcd1irraplemap  15643  wilthlem1  15654  mpodvdsmulf1o  15664  mersenne  15671  perfectlem2  15674  perfect  15675  zabsle1  15678  lgslem1  15679  lgsval  15683  lgsfvalg  15684  lgsfcl2  15685  lgsval2lem  15689  lgscl1  15702  lgsmod  15705  lgsdir2lem5  15711  lgsdir2  15712  lgsdilem2  15715  lgsdi  15716  lgsne0  15717  gausslemma2dlem0c  15730  gausslemma2dlem0h  15735  gausslemma2dlem1a  15737  gausslemma2dlem1f1o  15739  gausslemma2dlem3  15742  lgseisenlem1  15749  lgseisenlem2  15750  lgseisenlem3  15751  lgseisenlem4  15752  lgseisen  15753  lgsquadlem1  15756  lgsquadlem2  15757  lgsquadlem3  15758  lgsquad3  15763  2lgslem3b1  15777  2lgslem3c1  15778  2lgs  15783  2lgsoddprmlem2  15785  2lgsoddprm  15792  2sqlem3  15796  2sqlem8  15802  2sqlem10  15804  structgrssvtx  15843  structgrssiedg  15844  ushgruhgr  15880  uhgrun  15886  incistruhgr  15890  upgrop  15904  upgruhgr  15911  umgrupgr  15912  umgrnloopv  15914  umgredgprv  15915  umgr0e  15918  upgr1edc  15921  upgrun  15924  umgrun  15926  umgrislfupgrdom  15929  upgredg  15942  umgrpredgv  15945  usgrop  15964  usgrausgrien  15967  ausgrumgrien  15968  ausgrusgrien  15969  uspgrupgrushgr  15980  usgrumgr  15982  usgrumgruspgr  15983  usgruspgrben  15984  usgrislfuspgrdom  15988  edgssv2en  15997  usgrf1oedg  16003  usgredg4  16013  usgredg2vlem2  16021  usgredg2v  16022  ushgredgedg  16024  ushgredgedgloop  16026  usgrstrrepeen  16029  wlkm  16051  wlkvtxiedg  16056  wlkvtxiedgg  16057  wlkeq  16065  wlk1walkdom  16070  uspgr2wlkeq  16076  uspgr2wlkeqi  16078  fnmptd  16168  bj-sels  16277  bj-nnelon  16322  2omap  16359  pw1map  16361  pwle2  16364  pwf1oexmid  16365  pw1nct  16369  nninfall  16375  nninfsellemdc  16376  nninfself  16379  nnnninfex  16388  nninfnfiinf  16389  refeq  16396  isomninnlem  16398  cvgcmp2nlemabs  16400  trilpolemlt1  16409  trirec0  16412  apdifflemf  16414  apdifflemr  16415  apdiff  16416  iswomninnlem  16417  iswomni0  16419  ismkvnnlem  16420  reap0  16426  cndcap  16427