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  4104  3brtr4d  4114  snelpwi  4296  prelpwi  4299  pwel  4303  ordelon  4473  onin  4476  elelsuc  4499  onsuc  4592  onsucb  4594  onintonm  4608  omsinds  4713  sosng  4791  relssdv  4810  eqbrrdv  4815  eqrelrdv2  4817  relsnopg  4822  breldmg  4928  elrnmptdv  4977  iss  5050  xpimasn  5176  elxp4  5215  elxp5  5216  iotam  5309  funssres  5359  f0rn0  5519  fimadmfo  5556  sefvex  5647  fdmeu  5676  fvun1  5699  eqfnfvd  5734  fvimacnvi  5748  fvimacnv  5749  fvelrn  5765  fmpt3d  5790  fmpt2d  5796  resflem  5798  fmptco  5800  fsn  5806  funopsn  5816  ftpg  5822  fconst2g  5853  funfvima3  5872  elabrexg  5881  foeqcnvco  5913  f1eqcocnv  5914  fliftfun  5919  fliftfund  5920  fliftval  5923  riota5f  5980  f1ofveu  5988  f1ocnvd  6206  f1opw2  6210  off  6229  offval2  6232  ofrfval2  6233  offveq  6237  caofref  6241  caofinvl  6242  elxp6  6313  cnvf1olem  6368  f2ndf  6370  f1od2  6379  tposf12  6413  smores2  6438  tfrlemisucaccv  6469  tfrlemibfn  6472  tfr1onlemsucaccv  6485  tfr1onlembfn  6488  tfrcllemsucaccv  6498  tfrcllembfn  6501  tfrcl  6508  tfri3  6511  frecabcl  6543  nnsucsssuc  6636  ersym  6690  ertr  6693  swoer  6706  erth  6724  riinerm  6753  qliftfund  6763  eroprf  6773  ecopoverg  6781  th3qlem1  6782  elmapssres  6818  mapss  6836  fdiagfn  6837  ixpssmap2g  6872  mapsnf1o  6882  f1oen4g  6901  f1dom4g  6902  f1dom2g  6905  dom3d  6923  en2prd  6968  pw2f1odclem  6991  fopwdom  6993  mapxpen  7005  nndomo  7021  dif1en  7037  findcard2  7047  findcard2s  7048  diffisn  7051  fimax2gtrilemstep  7058  fientri3  7073  tpfidceq  7088  fiintim  7089  opabfi  7096  f1dmvrnfibi  7107  sbthlemi6  7125  elfir  7136  fifo  7143  supelti  7165  supsnti  7168  cnvinfex  7181  ordiso2  7198  updjud  7245  djudom  7256  difinfsn  7263  ctssdc  7276  enumctlemm  7277  enumct  7278  nninfninc  7286  enomnilem  7301  fodjuf  7308  ismkvnex  7318  omnimkv  7319  enmkvlem  7324  enwomnilem  7332  nninfdcinf  7334  nninfwlporlem  7336  isnumi  7350  exmidfodomrlemrALT  7377  finacn  7382  djudoml  7397  djudomr  7398  netap  7436  2omotaplemap  7439  2omotaplemst  7440  exmidapne  7442  cc2lem  7448  cc3  7450  ltsopi  7503  pitri3or  7505  ltdcpi  7506  indpi  7525  enqdc  7544  enqdc1  7545  addcmpblnq  7550  mulcanenq  7568  recrecnq  7577  nqtri3or  7579  ltdcnq  7580  ltsonq  7581  ltaddnq  7590  subhalfnqq  7597  archnqq  7600  prarloclemarch2  7602  enq0tr  7617  nqnq0  7624  addcmpblnq0  7626  mulcanenq0ec  7628  nnnq0lem1  7629  nqpnq0nq  7636  nq0m0r  7639  nq02m  7648  prarloclemlt  7676  prarloclemcalc  7685  addlocpr  7719  nqprl  7734  nqpru  7735  addnqprlemrl  7740  addnqprlemru  7741  prmuloclemcalc  7748  mullocprlem  7753  mulnqprlemrl  7756  mulnqprlemru  7757  1idprl  7773  1idpru  7774  ltaddpr  7780  ltexprlemm  7783  ltexprlemopl  7784  ltexprlemopu  7786  ltexprlemdisj  7789  ltexprlemrl  7793  ltexprlemru  7795  addcanprleml  7797  addcanprlemu  7798  addcanprg  7799  prplnqu  7803  recexprlemloc  7814  recexprlem1ssl  7816  recexprlem1ssu  7817  aptiprleml  7822  aptiprlemu  7823  archpr  7826  cauappcvgprlemm  7828  cauappcvgprlemopl  7829  cauappcvgprlemloc  7835  cauappcvgprlemladdfu  7837  cauappcvgprlemladdfl  7838  cauappcvgprlem1  7842  cauappcvgprlem2  7843  caucvgprlemnkj  7849  caucvgprlemopl  7852  caucvgprlemloc  7858  caucvgprlemladdfu  7860  caucvgprlem2  7863  caucvgprprlemnkltj  7872  caucvgprprlemopl  7880  caucvgprprlemloc  7886  caucvgprprlemexbt  7889  caucvgprprlemaddq  7891  caucvgprprlem2  7893  suplocexprlemmu  7901  suplocexprlemru  7902  suplocexprlemloc  7904  suplocexprlemlub  7907  prsrlem1  7925  0idsr  7950  1idsr  7951  recexgt0sr  7956  archsr  7965  prsradd  7969  caucvgsrlemcau  7976  caucvgsrlembound  7977  caucvgsrlemoffgt1  7982  suplocsrlemb  7989  suplocsrlempr  7990  suplocsrlem  7991  pitonnlem1p1  8029  pitonn  8031  pitoregt0  8032  peano2nnnn  8036  recidpirq  8041  axcaucvglemval  8080  leid  8226  nltled  8263  readdcan  8282  addneintrd  8330  addneintr2d  8331  pncan  8348  subsub2  8370  subsub4  8375  negned  8450  subne0d  8462  subneintrd  8497  subneintr2d  8499  subeq0bd  8521  subdi  8527  gt0add  8716  rimul  8728  rereim  8729  ltmul1a  8734  apreim  8746  apirr  8748  mulap0r  8758  msqge0  8759  mulge0  8762  gt0ap0  8769  ltap  8776  subap0d  8787  recexaplem2  8795  mulap0bad  8802  mulap0bbd  8803  mul0eqap  8813  divrecap  8831  div0ap  8845  div1  8846  recrecap  8852  divdivdivap  8856  ddcanap  8869  rerecclap  8873  div2negap  8878  diveqap1bd  8979  recgt0  8993  prodgt0  8995  lemul1a  9001  recp1lt1  9042  squeeze0  9047  peano2nn  9118  div4p1lem1div2  9361  arch  9362  peano2z  9478  peano2zm  9480  ztri3or  9485  nn0n0n1ge2  9513  zextle  9534  gtndiv  9538  suprzclex  9541  nn0ind-raph  9560  uzid  9732  uzneg  9737  uztric  9740  uz11  9741  eluzp1l  9743  qdivcl  9834  irrmul  9838  irrmulap  9839  rpnegap  9878  negelrpd  9880  ledivge1le  9918  mul2lt0rlt0  9951  mul2lt0rgt0  9952  nn0ledivnn  9959  ltpnf  9972  mnflt  9975  pnfge  9981  mnfle  9984  xrlttr  9987  xrltso  9988  xrlttri3  9989  xrleid  9992  xaddass2  10062  xltadd1  10068  xlt2add  10072  xleaddadd  10079  iccf1o  10196  fztri3or  10231  fznlem  10233  fzn  10234  fzsplit2  10242  fznatpl1  10268  uzsplit  10284  fseq1p1m1  10286  fzm1  10292  fznn0sub2  10320  difelfznle  10327  1fv  10331  fzodcel  10345  fzospliti  10370  fzouzsplit  10373  eluzgtdifelfzo  10398  exfzdc  10441  subfzo0  10443  zsupcllemstep  10444  zsupcl  10446  zssinfcl  10447  infssuzex  10448  infssuzcldc  10450  suprzubdc  10451  nninfdcex  10452  qdcle  10461  exbtwnz  10465  qbtwnrelemcalc  10470  flqlelt  10491  qfraclt1  10495  qfracge0  10496  flqltnz  10502  btwnzge0  10515  flhalf  10517  fldiv4lem1div2uz2  10521  ceiqle  10530  intfracq  10537  mulqmod0  10547  modqge0  10549  modqlt  10550  modqid  10566  modqid0  10567  m1modge3gt1  10588  modqltm1p1mod  10593  q2txmodxeq0  10601  modaddmodlo  10605  modsumfzodifsn  10613  addmodlteq  10615  frecuzrdgtcl  10629  frecuzrdgtclt  10638  uzennn  10653  uzsinds  10661  seqf  10681  seqf2  10685  monoord2  10703  iseqf1olemqk  10724  iseqf1olemjpcl  10725  iseqf1olemqpcl  10726  seq3f1olemqsumkj  10728  seq3f1olemqsum  10730  seq3f1olemstep  10731  seq3f1oleml  10733  seqf1oglem1  10736  ser3le  10754  exp3vallem  10757  exp3val  10758  expp1  10763  expcllem  10767  ltexp2a  10808  leexp2a  10809  nn0ltexp2  10926  faclbnd  10958  faclbnd2  10959  faclbnd3  10960  bcval5  10980  bcpasc  10983  hashennn  10997  fihasheqf1oi  11004  hashsng  11015  fihashfn  11017  hashun  11022  fihashss  11033  fihashssdif  11035  hashfz  11038  hashxp  11043  fimaxq  11044  zfz1isolem1  11057  seq3coll  11059  hashdmprop2dom  11061  wrdf  11072  wrdlenge2n0  11102  fstwrdne0  11106  wrdred1hash  11110  ccatvalfn  11131  ccatsymb  11132  ccatlid  11136  ccatrid  11137  ccatrn  11139  eqs1  11156  ccats1val2  11166  fzowrddc  11174  swrdlen  11179  swrdnd  11186  swrd0g  11187  swrdfv2  11190  swrdwrdsymbg  11191  pfxn0  11215  pfxwrdsymbg  11217  pfxsuff1eqwrdeq  11226  swrdswrd  11232  ccats1pfxeq  11241  ccats1pfxeqrex  11242  wrdind  11249  wrd2ind  11250  swrdccatin1  11252  pfxccatin12lem4  11253  swrdccatin2  11256  pfxccatin12  11260  pfxccat3a  11265  swrdccat3blem  11266  pfxccatid  11268  swrdccatin2d  11271  shftfn  11330  cjth  11352  cjmulrcl  11393  reim0bd  11450  rerebd  11451  cjrebd  11452  caucvgre  11487  cvg1nlemcxze  11488  cvg1nlemcau  11490  cvg1nlemres  11491  recvguniq  11501  resqrexlemover  11516  resqrexlemdec  11517  resqrexlemgt0  11526  resqrexlemoverl  11527  resqrexlemglsq  11528  rersqrtthlem  11536  sqrtgt0  11540  leabs  11580  absexpzap  11586  absle  11595  recvalap  11603  abstri  11610  abs2dif  11612  amgm2  11624  absne0d  11693  maxleim  11711  maxabslemab  11712  maxabslemlub  11713  maxltsup  11724  zmaxcl  11730  fimaxre2  11733  minmax  11736  rpmincl  11744  bdtrilem  11745  bdtri  11746  xrmaxleim  11750  xrmaxiflemcom  11755  xrmaxltsup  11764  xrmaxadd  11767  xrminmax  11771  xrminrpcl  11780  climconst  11796  climuni  11799  2clim  11807  climcn1  11814  climcn2  11815  reccn2ap  11819  climge0  11831  climle  11840  climsqz  11841  climsqz2  11842  serf0  11858  summodclem3  11886  summodclem2a  11887  fsumcl2lem  11904  sumpr  11919  sumtp  11920  fsum0diaglem  11946  mptfzshft  11948  fsumle  11969  fsumlt  11970  divcnv  12003  trireciplem  12006  expcnvap0  12008  expcnv  12010  explecnv  12011  geosergap  12012  cvgratnnlembern  12029  cvgratnnlemabsle  12033  cvgratnnlemsumlt  12034  cvgratz  12038  cvgratgt0  12039  mertenslemi1  12041  mertenslem2  12042  mertensabs  12043  clim2divap  12046  prodmodclem3  12081  prodmodclem2a  12082  fprodseq  12089  fprodmul  12097  fprodfac  12121  fprodconst  12126  fprodap0  12127  fprodap0f  12142  fprodle  12146  eftcl  12160  ef0lem  12166  efsub  12187  eftlub  12196  eflegeo  12207  tanval2ap  12219  sinadd  12242  cos2t  12256  cos2tsin  12257  sin01bnd  12263  cos01bnd  12264  eirraplem  12283  dvdsval2  12296  dvdsdc  12304  dvds0lem  12307  zdvdsdc  12318  dvdscmulr  12326  dvdsmulcr  12327  fsumdvds  12348  dvdslelemd  12349  divconjdvds  12355  dvdsext  12361  fzm1ndvds  12362  dvdsmod  12368  3dvds  12370  oexpneg  12383  2tp1odd  12390  mulsucdiv2z  12391  2teven  12393  zeo5  12394  opeo  12403  omeo  12404  nn0ob  12414  divalglemnqt  12426  bitsdc  12453  bits0o  12456  bitsfzolem  12460  bitsfzo  12461  bitsmod  12462  bitscmp  12464  bitsinv1lem  12467  gcddvds  12479  dvdslegcd  12480  gcdneg  12498  bezoutlemnewy  12512  bezoutlemstep  12513  bezoutlema  12515  bezoutlemb  12516  bezoutlemmo  12522  bezoutlemle  12524  bezoutlemsup  12525  dfgcd3  12526  bezout  12527  dfgcd2  12530  uzwodc  12553  lcmcllem  12584  lcmneg  12591  lcmgcdlem  12594  lcmdvds  12596  lcmid  12597  3lcm2e6woprm  12603  6lcm4e12  12604  ncoprmgcdne1b  12606  mulgcddvds  12611  divgcdcoprmex  12619  cncongr1  12620  cncongr2  12621  isprm2lem  12633  prmind2  12637  dvdsnprmd  12642  prm2orodd  12643  sqnprm  12653  isprm5lem  12658  rpexp  12670  sqrt2irrlem  12678  oddpwdclemdc  12690  sqrt2irraplemnn  12696  qnumdencoprm  12710  qeqnumdivden  12711  nn0gcdsq  12717  nn0sqrtelqelz  12723  nonsq  12724  phicl2  12731  phibnd  12734  hashdvds  12738  phiprmpw  12739  phimullem  12742  eulerthlemrprm  12746  eulerthlema  12747  eulerthlemth  12749  prmdiveq  12753  hashgcdlem  12755  odzdvds  12763  modprminv  12767  nnnn0modprm0  12773  modprmn0modprm0  12774  pythagtriplem10  12787  pythagtriplem19  12800  pythagtrip  12801  pcpre1  12810  pcpremul  12811  pceu  12813  pcmul  12819  pcdiv  12820  pcqmul  12821  pcqdiv  12825  pcexp  12827  pcdvdsb  12838  pcidlem  12841  pcdvdstr  12845  pcgcd1  12846  pc2dvds  12848  pcprmpw2  12851  difsqpwdvds  12856  pcaddlem  12857  pcadd  12858  pcadd2  12859  pcmpt  12861  pcmptdvds  12863  pcprod  12864  fldivp1  12866  pcfaclem  12867  pcfac  12868  pcbc  12869  qexpz  12870  pockthlem  12874  pockthg  12875  1arithlem4  12884  1arith  12885  1arith2  12886  4sqlem6  12901  4sqlem8  12903  4sqlem9  12904  4sqlem10  12905  4sqexercise1  12916  4sqexercise2  12917  4sqlemsdc  12918  4sqlem11  12919  4sqlem12  12920  4sqlem15  12923  4sqlem16  12924  4sqlem17  12925  znnen  12964  ennnfonelemk  12966  ennnfonelemkh  12978  ennnfonelemhf1o  12979  ennnfonelemrnh  12982  ennnfonelemfun  12983  ennnfonelemf1  12984  ennnfonelemrn  12985  ennnfonelemnn0  12988  ctinfomlemom  12993  ctiunctlemudc  13003  unct  13008  omctfn  13009  ssnnctlemct  13012  nninfdclemp1  13016  nninfdc  13019  structfung  13044  setsfun  13062  setsfun0  13063  setscom  13067  strslfv3  13073  setsslid  13078  pwsdiagel  13325  pwssnf1o  13326  imasaddfnlemg  13342  imasaddvallemg  13343  mgmsscl  13389  plusffng  13393  mgmplusf  13394  mgm0  13397  mgm1  13398  opifismgmdc  13399  gsumfzval  13419  gsumprval  13427  sgrp1  13439  issgrpd  13440  prdsplusgsgrpcl  13442  mndpfo  13466  mndfo  13467  prdsplusgcl  13474  prdsidlem  13475  mnd1  13483  0subm  13512  mhmima  13519  grpinvfng  13572  isgrpinv  13582  grpinvid  13588  grpinvf1o  13598  grpinvadd  13606  grpsubf  13607  grpsubsub4  13621  grplactcnv  13630  grp1  13634  grp1inv  13635  prdsinvlem  13636  prdsinvgd  13638  qusgrp2  13645  mulgfng  13656  subginv  13713  resgrpisgrp  13727  subgintm  13730  0subg  13731  0nsg  13746  qusinv  13768  ghminv  13782  ghmrn  13789  ghmeql  13799  ghmnsgima  13800  kerf1ghm  13806  conjnmz  13811  rngass  13897  rngmneg1  13905  rngmneg2  13906  qusrng  13916  srgideu  13930  srgidmlem  13936  srgpcomp  13948  srg1expzeq1  13953  ringcl  13971  ringideu  13975  ringidmlem  13980  ringnegl  14009  ringnegr  14010  ring1  14017  qusring2  14024  opprringbg  14038  dvdsrd  14052  dvdsr01  14062  isunitd  14064  unitinvcl  14081  unitinvinv  14082  unitnegcl  14088  rhmmul  14122  rhmf1o  14126  nzrunit  14146  lringuplu  14154  subrngintm  14170  subrgsubm  14192  subrgintm  14201  aprsym  14242  scaffng  14267  lmodscaf  14268  lsssn0  14328  lss1d  14341  lssintclm  14342  lspval  14348  lspcl  14349  lspsnid  14365  lspprid1  14369  lspsn  14374  sraval  14395  rspcl  14449  rspssid  14450  rspssp  14452  rnglidlmmgm  14454  rnglidlmsgrp  14455  cnfldneg  14531  zringinvg  14562  expghmap  14565  znzrhfo  14606  znf1o  14609  znhash  14614  znidomb  14616  znrrg  14618  psrbagfi  14631  psraddcl  14638  psr0cl  14639  psrnegcl  14641  psrneg  14645  psr1clfi  14646  mplsubgfilemm  14656  mplsubgfilemcl  14657  baspartn  14718  eltg3i  14724  tgclb  14733  topbas  14735  2basgeng  14750  topcld  14777  0cld  14780  uncld  14781  neif  14809  elnei  14820  0nei  14834  restbasg  14836  iscnp4  14886  cnpnei  14887  cnclima  14891  cncnp  14898  cnrest2r  14905  cndis  14909  lmff  14917  lmtopcnp  14918  txbas  14926  txopn  14933  txcnp  14939  upxp  14940  txdis1cn  14946  cnmpt11  14951  cnmpt21  14959  psmetge0  14999  xmetge0  15033  xmettpos  15038  xmetrtri  15044  metrtri  15045  xblpnfps  15066  xblpnf  15067  blfps  15077  blf  15078  ssblps  15093  ssbl  15094  blbas  15101  metss2  15166  xmettxlem  15177  xmettx  15178  qtopbas  15190  divcnap  15233  cncfss  15251  cdivcncfap  15272  expcncf  15277  cnopnap  15279  maxcncf  15283  mincncf  15284  dedekindeulemuub  15285  dedekindeulemlu  15289  dedekindeu  15291  suplociccex  15293  dedekindicclemuub  15294  dedekindicclemlu  15298  dedekindicclemicc  15300  ivthinclemlopn  15304  ivthinclemuopn  15306  ivthinc  15311  ivthreinc  15313  hoverlt1  15317  ellimc3apf  15328  limcimolemlt  15332  limcimo  15333  limcresi  15334  cnplimclemle  15336  reldvg  15347  dvfgg  15356  dvidlemap  15359  dvidrelem  15360  dvidsslem  15361  dvcjbr  15376  dvcj  15377  dvrecap  15381  dveflem  15394  dvef  15395  elply2  15403  elplyr  15408  plycj  15429  plyreres  15432  reeff1oleme  15440  pilem3  15451  sinq34lt0t  15499  cosq14gt0  15500  coseq0q4123  15502  tangtx  15506  sincosq1eq  15507  cosordlem  15517  logdivlti  15549  relogbval  15619  relogbzcl  15620  nnlogbexp  15627  logbgcd1irr  15635  logbgcd1irraplemexp  15636  logbgcd1irraplemap  15637  wilthlem1  15648  mpodvdsmulf1o  15658  mersenne  15665  perfectlem2  15668  perfect  15669  zabsle1  15672  lgslem1  15673  lgsval  15677  lgsfvalg  15678  lgsfcl2  15679  lgsval2lem  15683  lgscl1  15696  lgsmod  15699  lgsdir2lem5  15705  lgsdir2  15706  lgsdilem2  15709  lgsdi  15710  lgsne0  15711  gausslemma2dlem0c  15724  gausslemma2dlem0h  15729  gausslemma2dlem1a  15731  gausslemma2dlem1f1o  15733  gausslemma2dlem3  15736  lgseisenlem1  15743  lgseisenlem2  15744  lgseisenlem3  15745  lgseisenlem4  15746  lgseisen  15747  lgsquadlem1  15750  lgsquadlem2  15751  lgsquadlem3  15752  lgsquad3  15757  2lgslem3b1  15771  2lgslem3c1  15772  2lgs  15777  2lgsoddprmlem2  15779  2lgsoddprm  15786  2sqlem3  15790  2sqlem8  15796  2sqlem10  15798  structgrssvtx  15837  structgrssiedg  15838  ushgruhgr  15874  uhgrun  15880  incistruhgr  15884  upgrop  15898  upgruhgr  15905  umgrupgr  15906  umgrnloopv  15908  umgredgprv  15909  umgr0e  15912  upgr1edc  15915  upgrun  15918  umgrun  15920  umgrislfupgrdom  15923  upgredg  15936  umgrpredgv  15939  usgrop  15958  usgrausgrien  15961  ausgrumgrien  15962  ausgrusgrien  15963  uspgrupgrushgr  15974  usgrumgr  15976  usgrumgruspgr  15977  usgruspgrben  15978  usgrislfuspgrdom  15982  edgssv2en  15991  usgrf1oedg  15997  usgredg4  16007  usgredg2vlem2  16015  usgredg2v  16016  ushgredgedg  16018  ushgredgedgloop  16020  usgrstrrepeen  16023  wlkm  16038  wlkvtxiedgg  16042  fnmptd  16126  bj-sels  16235  bj-nnelon  16280  2omap  16318  pw1map  16320  pwle2  16323  pwf1oexmid  16324  pw1nct  16328  nninfall  16334  nninfsellemdc  16335  nninfself  16338  nnnninfex  16347  nninfnfiinf  16348  refeq  16355  isomninnlem  16357  cvgcmp2nlemabs  16359  trilpolemlt1  16368  trirec0  16371  apdifflemf  16373  apdifflemr  16374  apdiff  16375  iswomninnlem  16376  iswomni0  16378  ismkvnnlem  16379  reap0  16385  cndcap  16386