Theorem mpbird 167

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

Hypotheses

Ref	Expression
mpbird.min	⊢ (𝜑 → 𝜒)
mpbird.maj	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
mpbird	⊢ (𝜑 → 𝜓)

Proof of Theorem mpbird

Step	Hyp	Ref	Expression
1		mpbird.min	. 2 ⊢ (𝜑 → 𝜒)
2		mpbird.maj	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	2	biimprd 158	. 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  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpbiri  168  pm5.19  710  pm4.55dc  943  mpbir2and  949  pm3.12dc  963  mpbir3and  1185  pm5.15dc  1411  eqeltrd  2286  eqnetrd  2404  3netr4d  2413  r19.30dc  2658  raleqtrrdv  2718  rexeqtrrdv  2719  sbcne12g  3122  eqsstrd  3240  3sstr4d  3249  eqbrtrd  4084  3brtr4d  4094  snelpwi  4276  prelpwi  4279  pwel  4283  ordelon  4451  onin  4454  elelsuc  4477  onsuc  4570  onsucb  4572  onintonm  4586  omsinds  4691  sosng  4769  relssdv  4788  eqbrrdv  4793  eqrelrdv2  4795  relsnopg  4800  breldmg  4906  elrnmptdv  4954  iss  5027  xpimasn  5153  elxp4  5192  elxp5  5193  iotam  5286  funssres  5336  f0rn0  5496  fimadmfo  5533  sefvex  5624  fdmeu  5650  fvun1  5673  eqfnfvd  5708  fvimacnvi  5722  fvimacnv  5723  fvelrn  5739  fmpt3d  5764  fmpt2d  5770  resflem  5772  fmptco  5774  fsn  5780  funopsn  5790  ftpg  5796  fconst2g  5827  funfvima3  5846  elabrexg  5855  foeqcnvco  5887  f1eqcocnv  5888  fliftfun  5893  fliftfund  5894  fliftval  5897  riota5f  5954  f1ofveu  5962  f1ocnvd  6178  f1opw2  6182  off  6201  offval2  6204  ofrfval2  6205  offveq  6209  caofref  6213  caofinvl  6214  elxp6  6285  cnvf1olem  6340  f2ndf  6342  f1od2  6351  tposf12  6385  smores2  6410  tfrlemisucaccv  6441  tfrlemibfn  6444  tfr1onlemsucaccv  6457  tfr1onlembfn  6460  tfrcllemsucaccv  6470  tfrcllembfn  6473  tfrcl  6480  tfri3  6483  frecabcl  6515  nnsucsssuc  6608  ersym  6662  ertr  6665  swoer  6678  erth  6696  riinerm  6725  qliftfund  6735  eroprf  6745  ecopoverg  6753  th3qlem1  6754  elmapssres  6790  mapss  6808  fdiagfn  6809  ixpssmap2g  6844  mapsnf1o  6854  f1oen4g  6873  f1dom4g  6874  f1dom2g  6877  dom3d  6895  en2prd  6940  pw2f1odclem  6963  fopwdom  6965  mapxpen  6977  nndomo  6993  dif1en  7009  findcard2  7019  findcard2s  7020  diffisn  7023  fimax2gtrilemstep  7030  fientri3  7045  tpfidceq  7060  fiintim  7061  opabfi  7068  f1dmvrnfibi  7079  sbthlemi6  7097  elfir  7108  fifo  7115  supelti  7137  supsnti  7140  cnvinfex  7153  ordiso2  7170  updjud  7217  djudom  7228  difinfsn  7235  ctssdc  7248  enumctlemm  7249  enumct  7250  nninfninc  7258  enomnilem  7273  fodjuf  7280  ismkvnex  7290  omnimkv  7291  enmkvlem  7296  enwomnilem  7304  nninfdcinf  7306  nninfwlporlem  7308  isnumi  7322  exmidfodomrlemrALT  7349  finacn  7354  djudoml  7369  djudomr  7370  netap  7408  2omotaplemap  7411  2omotaplemst  7412  exmidapne  7414  cc2lem  7420  cc3  7422  ltsopi  7475  pitri3or  7477  ltdcpi  7478  indpi  7497  enqdc  7516  enqdc1  7517  addcmpblnq  7522  mulcanenq  7540  recrecnq  7549  nqtri3or  7551  ltdcnq  7552  ltsonq  7553  ltaddnq  7562  subhalfnqq  7569  archnqq  7572  prarloclemarch2  7574  enq0tr  7589  nqnq0  7596  addcmpblnq0  7598  mulcanenq0ec  7600  nnnq0lem1  7601  nqpnq0nq  7608  nq0m0r  7611  nq02m  7620  prarloclemlt  7648  prarloclemcalc  7657  addlocpr  7691  nqprl  7706  nqpru  7707  addnqprlemrl  7712  addnqprlemru  7713  prmuloclemcalc  7720  mullocprlem  7725  mulnqprlemrl  7728  mulnqprlemru  7729  1idprl  7745  1idpru  7746  ltaddpr  7752  ltexprlemm  7755  ltexprlemopl  7756  ltexprlemopu  7758  ltexprlemdisj  7761  ltexprlemrl  7765  ltexprlemru  7767  addcanprleml  7769  addcanprlemu  7770  addcanprg  7771  prplnqu  7775  recexprlemloc  7786  recexprlem1ssl  7788  recexprlem1ssu  7789  aptiprleml  7794  aptiprlemu  7795  archpr  7798  cauappcvgprlemm  7800  cauappcvgprlemopl  7801  cauappcvgprlemloc  7807  cauappcvgprlemladdfu  7809  cauappcvgprlemladdfl  7810  cauappcvgprlem1  7814  cauappcvgprlem2  7815  caucvgprlemnkj  7821  caucvgprlemopl  7824  caucvgprlemloc  7830  caucvgprlemladdfu  7832  caucvgprlem2  7835  caucvgprprlemnkltj  7844  caucvgprprlemopl  7852  caucvgprprlemloc  7858  caucvgprprlemexbt  7861  caucvgprprlemaddq  7863  caucvgprprlem2  7865  suplocexprlemmu  7873  suplocexprlemru  7874  suplocexprlemloc  7876  suplocexprlemlub  7879  prsrlem1  7897  0idsr  7922  1idsr  7923  recexgt0sr  7928  archsr  7937  prsradd  7941  caucvgsrlemcau  7948  caucvgsrlembound  7949  caucvgsrlemoffgt1  7954  suplocsrlemb  7961  suplocsrlempr  7962  suplocsrlem  7963  pitonnlem1p1  8001  pitonn  8003  pitoregt0  8004  peano2nnnn  8008  recidpirq  8013  axcaucvglemval  8052  leid  8198  nltled  8235  readdcan  8254  addneintrd  8302  addneintr2d  8303  pncan  8320  subsub2  8342  subsub4  8347  negned  8422  subne0d  8434  subneintrd  8469  subneintr2d  8471  subeq0bd  8493  subdi  8499  gt0add  8688  rimul  8700  rereim  8701  ltmul1a  8706  apreim  8718  apirr  8720  mulap0r  8730  msqge0  8731  mulge0  8734  gt0ap0  8741  ltap  8748  subap0d  8759  recexaplem2  8767  mulap0bad  8774  mulap0bbd  8775  mul0eqap  8785  divrecap  8803  div0ap  8817  div1  8818  recrecap  8824  divdivdivap  8828  ddcanap  8841  rerecclap  8845  div2negap  8850  diveqap1bd  8951  recgt0  8965  prodgt0  8967  lemul1a  8973  recp1lt1  9014  squeeze0  9019  peano2nn  9090  div4p1lem1div2  9333  arch  9334  peano2z  9450  peano2zm  9452  ztri3or  9457  nn0n0n1ge2  9485  zextle  9506  gtndiv  9510  suprzclex  9513  nn0ind-raph  9532  uzid  9704  uzneg  9709  uztric  9712  uz11  9713  eluzp1l  9715  qdivcl  9806  irrmul  9810  irrmulap  9811  rpnegap  9850  negelrpd  9852  ledivge1le  9890  mul2lt0rlt0  9923  mul2lt0rgt0  9924  nn0ledivnn  9931  ltpnf  9944  mnflt  9947  pnfge  9953  mnfle  9956  xrlttr  9959  xrltso  9960  xrlttri3  9961  xrleid  9964  xaddass2  10034  xltadd1  10040  xlt2add  10044  xleaddadd  10051  iccf1o  10168  fztri3or  10203  fznlem  10205  fzn  10206  fzsplit2  10214  fznatpl1  10240  uzsplit  10256  fseq1p1m1  10258  fzm1  10264  fznn0sub2  10292  difelfznle  10299  1fv  10303  fzodcel  10317  fzospliti  10342  fzouzsplit  10345  eluzgtdifelfzo  10370  exfzdc  10413  subfzo0  10415  zsupcllemstep  10416  zsupcl  10418  zssinfcl  10419  infssuzex  10420  infssuzcldc  10422  suprzubdc  10423  nninfdcex  10424  qdcle  10433  exbtwnz  10437  qbtwnrelemcalc  10442  flqlelt  10463  qfraclt1  10467  qfracge0  10468  flqltnz  10474  btwnzge0  10487  flhalf  10489  fldiv4lem1div2uz2  10493  ceiqle  10502  intfracq  10509  mulqmod0  10519  modqge0  10521  modqlt  10522  modqid  10538  modqid0  10539  m1modge3gt1  10560  modqltm1p1mod  10565  q2txmodxeq0  10573  modaddmodlo  10577  modsumfzodifsn  10585  addmodlteq  10587  frecuzrdgtcl  10601  frecuzrdgtclt  10610  uzennn  10625  uzsinds  10633  seqf  10653  seqf2  10657  monoord2  10675  iseqf1olemqk  10696  iseqf1olemjpcl  10697  iseqf1olemqpcl  10698  seq3f1olemqsumkj  10700  seq3f1olemqsum  10702  seq3f1olemstep  10703  seq3f1oleml  10705  seqf1oglem1  10708  ser3le  10726  exp3vallem  10729  exp3val  10730  expp1  10735  expcllem  10739  ltexp2a  10780  leexp2a  10781  nn0ltexp2  10898  faclbnd  10930  faclbnd2  10931  faclbnd3  10932  bcval5  10952  bcpasc  10955  hashennn  10969  fihasheqf1oi  10976  hashsng  10987  fihashfn  10989  hashun  10994  fihashss  11005  fihashssdif  11007  hashfz  11010  hashxp  11015  fimaxq  11016  zfz1isolem1  11029  seq3coll  11031  hashdmprop2dom  11033  wrdf  11044  wrdlenge2n0  11073  fstwrdne0  11077  wrdred1hash  11081  ccatvalfn  11102  ccatsymb  11103  ccatlid  11107  ccatrid  11108  ccatrn  11110  eqs1  11127  ccats1val2  11137  fzowrddc  11145  swrdlen  11150  swrdnd  11157  swrd0g  11158  swrdfv2  11161  swrdwrdsymbg  11162  pfxn0  11186  pfxwrdsymbg  11188  pfxsuff1eqwrdeq  11197  swrdswrd  11203  ccats1pfxeq  11212  ccats1pfxeqrex  11213  wrdind  11220  wrd2ind  11221  swrdccatin1  11223  pfxccatin12lem4  11224  swrdccatin2  11227  pfxccatin12  11231  pfxccat3a  11236  swrdccat3blem  11237  pfxccatid  11239  swrdccatin2d  11242  shftfn  11301  cjth  11323  cjmulrcl  11364  reim0bd  11421  rerebd  11422  cjrebd  11423  caucvgre  11458  cvg1nlemcxze  11459  cvg1nlemcau  11461  cvg1nlemres  11462  recvguniq  11472  resqrexlemover  11487  resqrexlemdec  11488  resqrexlemgt0  11497  resqrexlemoverl  11498  resqrexlemglsq  11499  rersqrtthlem  11507  sqrtgt0  11511  leabs  11551  absexpzap  11557  absle  11566  recvalap  11574  abstri  11581  abs2dif  11583  amgm2  11595  absne0d  11664  maxleim  11682  maxabslemab  11683  maxabslemlub  11684  maxltsup  11695  zmaxcl  11701  fimaxre2  11704  minmax  11707  rpmincl  11715  bdtrilem  11716  bdtri  11717  xrmaxleim  11721  xrmaxiflemcom  11726  xrmaxltsup  11735  xrmaxadd  11738  xrminmax  11742  xrminrpcl  11751  climconst  11767  climuni  11770  2clim  11778  climcn1  11785  climcn2  11786  reccn2ap  11790  climge0  11802  climle  11811  climsqz  11812  climsqz2  11813  serf0  11829  summodclem3  11857  summodclem2a  11858  fsumcl2lem  11875  sumpr  11890  sumtp  11891  fsum0diaglem  11917  mptfzshft  11919  fsumle  11940  fsumlt  11941  divcnv  11974  trireciplem  11977  expcnvap0  11979  expcnv  11981  explecnv  11982  geosergap  11983  cvgratnnlembern  12000  cvgratnnlemabsle  12004  cvgratnnlemsumlt  12005  cvgratz  12009  cvgratgt0  12010  mertenslemi1  12012  mertenslem2  12013  mertensabs  12014  clim2divap  12017  prodmodclem3  12052  prodmodclem2a  12053  fprodseq  12060  fprodmul  12068  fprodfac  12092  fprodconst  12097  fprodap0  12098  fprodap0f  12113  fprodle  12117  eftcl  12131  ef0lem  12137  efsub  12158  eftlub  12167  eflegeo  12178  tanval2ap  12190  sinadd  12213  cos2t  12227  cos2tsin  12228  sin01bnd  12234  cos01bnd  12235  eirraplem  12254  dvdsval2  12267  dvdsdc  12275  dvds0lem  12278  zdvdsdc  12289  dvdscmulr  12297  dvdsmulcr  12298  fsumdvds  12319  dvdslelemd  12320  divconjdvds  12326  dvdsext  12332  fzm1ndvds  12333  dvdsmod  12339  3dvds  12341  oexpneg  12354  2tp1odd  12361  mulsucdiv2z  12362  2teven  12364  zeo5  12365  opeo  12374  omeo  12375  nn0ob  12385  divalglemnqt  12397  bitsdc  12424  bits0o  12427  bitsfzolem  12431  bitsfzo  12432  bitsmod  12433  bitscmp  12435  bitsinv1lem  12438  gcddvds  12450  dvdslegcd  12451  gcdneg  12469  bezoutlemnewy  12483  bezoutlemstep  12484  bezoutlema  12486  bezoutlemb  12487  bezoutlemmo  12493  bezoutlemle  12495  bezoutlemsup  12496  dfgcd3  12497  bezout  12498  dfgcd2  12501  uzwodc  12524  lcmcllem  12555  lcmneg  12562  lcmgcdlem  12565  lcmdvds  12567  lcmid  12568  3lcm2e6woprm  12574  6lcm4e12  12575  ncoprmgcdne1b  12577  mulgcddvds  12582  divgcdcoprmex  12590  cncongr1  12591  cncongr2  12592  isprm2lem  12604  prmind2  12608  dvdsnprmd  12613  prm2orodd  12614  sqnprm  12624  isprm5lem  12629  rpexp  12641  sqrt2irrlem  12649  oddpwdclemdc  12661  sqrt2irraplemnn  12667  qnumdencoprm  12681  qeqnumdivden  12682  nn0gcdsq  12688  nn0sqrtelqelz  12694  nonsq  12695  phicl2  12702  phibnd  12705  hashdvds  12709  phiprmpw  12710  phimullem  12713  eulerthlemrprm  12717  eulerthlema  12718  eulerthlemth  12720  prmdiveq  12724  hashgcdlem  12726  odzdvds  12734  modprminv  12738  nnnn0modprm0  12744  modprmn0modprm0  12745  pythagtriplem10  12758  pythagtriplem19  12771  pythagtrip  12772  pcpre1  12781  pcpremul  12782  pceu  12784  pcmul  12790  pcdiv  12791  pcqmul  12792  pcqdiv  12796  pcexp  12798  pcdvdsb  12809  pcidlem  12812  pcdvdstr  12816  pcgcd1  12817  pc2dvds  12819  pcprmpw2  12822  difsqpwdvds  12827  pcaddlem  12828  pcadd  12829  pcadd2  12830  pcmpt  12832  pcmptdvds  12834  pcprod  12835  fldivp1  12837  pcfaclem  12838  pcfac  12839  pcbc  12840  qexpz  12841  pockthlem  12845  pockthg  12846  1arithlem4  12855  1arith  12856  1arith2  12857  4sqlem6  12872  4sqlem8  12874  4sqlem9  12875  4sqlem10  12876  4sqexercise1  12887  4sqexercise2  12888  4sqlemsdc  12889  4sqlem11  12890  4sqlem12  12891  4sqlem15  12894  4sqlem16  12895  4sqlem17  12896  znnen  12935  ennnfonelemk  12937  ennnfonelemkh  12949  ennnfonelemhf1o  12950  ennnfonelemrnh  12953  ennnfonelemfun  12954  ennnfonelemf1  12955  ennnfonelemrn  12956  ennnfonelemnn0  12959  ctinfomlemom  12964  ctiunctlemudc  12974  unct  12979  omctfn  12980  ssnnctlemct  12983  nninfdclemp1  12987  nninfdc  12990  structfung  13015  setsfun  13033  setsfun0  13034  setscom  13038  strslfv3  13044  setsslid  13049  pwsdiagel  13296  pwssnf1o  13297  imasaddfnlemg  13313  imasaddvallemg  13314  mgmsscl  13360  plusffng  13364  mgmplusf  13365  mgm0  13368  mgm1  13369  opifismgmdc  13370  gsumfzval  13390  gsumprval  13398  sgrp1  13410  issgrpd  13411  prdsplusgsgrpcl  13413  mndpfo  13437  mndfo  13438  prdsplusgcl  13445  prdsidlem  13446  mnd1  13454  0subm  13483  mhmima  13490  grpinvfng  13543  isgrpinv  13553  grpinvid  13559  grpinvf1o  13569  grpinvadd  13577  grpsubf  13578  grpsubsub4  13592  grplactcnv  13601  grp1  13605  grp1inv  13606  prdsinvlem  13607  prdsinvgd  13609  qusgrp2  13616  mulgfng  13627  subginv  13684  resgrpisgrp  13698  subgintm  13701  0subg  13702  0nsg  13717  qusinv  13739  ghminv  13753  ghmrn  13760  ghmeql  13770  ghmnsgima  13771  kerf1ghm  13777  conjnmz  13782  rngass  13868  rngmneg1  13876  rngmneg2  13877  qusrng  13887  srgideu  13901  srgidmlem  13907  srgpcomp  13919  srg1expzeq1  13924  ringcl  13942  ringideu  13946  ringidmlem  13951  ringnegl  13980  ringnegr  13981  ring1  13988  qusring2  13995  opprringbg  14009  dvdsrd  14023  dvdsr01  14033  isunitd  14035  unitinvcl  14052  unitinvinv  14053  unitnegcl  14059  rhmmul  14093  rhmf1o  14097  nzrunit  14117  lringuplu  14125  subrngintm  14141  subrgsubm  14163  subrgintm  14172  aprsym  14213  scaffng  14238  lmodscaf  14239  lsssn0  14299  lss1d  14312  lssintclm  14313  lspval  14319  lspcl  14320  lspsnid  14336  lspprid1  14340  lspsn  14345  sraval  14366  rspcl  14420  rspssid  14421  rspssp  14423  rnglidlmmgm  14425  rnglidlmsgrp  14426  cnfldneg  14502  zringinvg  14533  expghmap  14536  znzrhfo  14577  znf1o  14580  znhash  14585  znidomb  14587  znrrg  14589  psrbagfi  14602  psraddcl  14609  psr0cl  14610  psrnegcl  14612  psrneg  14616  psr1clfi  14617  mplsubgfilemm  14627  mplsubgfilemcl  14628  baspartn  14689  eltg3i  14695  tgclb  14704  topbas  14706  2basgeng  14721  topcld  14748  0cld  14751  uncld  14752  neif  14780  elnei  14791  0nei  14805  restbasg  14807  iscnp4  14857  cnpnei  14858  cnclima  14862  cncnp  14869  cnrest2r  14876  cndis  14880  lmff  14888  lmtopcnp  14889  txbas  14897  txopn  14904  txcnp  14910  upxp  14911  txdis1cn  14917  cnmpt11  14922  cnmpt21  14930  psmetge0  14970  xmetge0  15004  xmettpos  15009  xmetrtri  15015  metrtri  15016  xblpnfps  15037  xblpnf  15038  blfps  15048  blf  15049  ssblps  15064  ssbl  15065  blbas  15072  metss2  15137  xmettxlem  15148  xmettx  15149  qtopbas  15161  divcnap  15204  cncfss  15222  cdivcncfap  15243  expcncf  15248  cnopnap  15250  maxcncf  15254  mincncf  15255  dedekindeulemuub  15256  dedekindeulemlu  15260  dedekindeu  15262  suplociccex  15264  dedekindicclemuub  15265  dedekindicclemlu  15269  dedekindicclemicc  15271  ivthinclemlopn  15275  ivthinclemuopn  15277  ivthinc  15282  ivthreinc  15284  hoverlt1  15288  ellimc3apf  15299  limcimolemlt  15303  limcimo  15304  limcresi  15305  cnplimclemle  15307  reldvg  15318  dvfgg  15327  dvidlemap  15330  dvidrelem  15331  dvidsslem  15332  dvcjbr  15347  dvcj  15348  dvrecap  15352  dveflem  15365  dvef  15366  elply2  15374  elplyr  15379  plycj  15400  plyreres  15403  reeff1oleme  15411  pilem3  15422  sinq34lt0t  15470  cosq14gt0  15471  coseq0q4123  15473  tangtx  15477  sincosq1eq  15478  cosordlem  15488  logdivlti  15520  relogbval  15590  relogbzcl  15591  nnlogbexp  15598  logbgcd1irr  15606  logbgcd1irraplemexp  15607  logbgcd1irraplemap  15608  wilthlem1  15619  mpodvdsmulf1o  15629  mersenne  15636  perfectlem2  15639  perfect  15640  zabsle1  15643  lgslem1  15644  lgsval  15648  lgsfvalg  15649  lgsfcl2  15650  lgsval2lem  15654  lgscl1  15667  lgsmod  15670  lgsdir2lem5  15676  lgsdir2  15677  lgsdilem2  15680  lgsdi  15681  lgsne0  15682  gausslemma2dlem0c  15695  gausslemma2dlem0h  15700  gausslemma2dlem1a  15702  gausslemma2dlem1f1o  15704  gausslemma2dlem3  15707  lgseisenlem1  15714  lgseisenlem2  15715  lgseisenlem3  15716  lgseisenlem4  15717  lgseisen  15718  lgsquadlem1  15721  lgsquadlem2  15722  lgsquadlem3  15723  lgsquad3  15728  2lgslem3b1  15742  2lgslem3c1  15743  2lgs  15748  2lgsoddprmlem2  15750  2lgsoddprm  15757  2sqlem3  15761  2sqlem8  15767  2sqlem10  15769  structgrssvtx  15808  structgrssiedg  15809  ushgruhgr  15845  uhgrun  15851  incistruhgr  15855  upgrop  15869  upgruhgr  15876  umgrupgr  15877  umgrnloopv  15879  umgredgprv  15880  umgr0e  15883  upgr1edc  15886  upgrun  15889  umgrun  15891  umgrislfupgrdom  15894  upgredg  15907  umgrpredgv  15910  usgrop  15929  usgrausgrien  15932  ausgrumgrien  15933  ausgrusgrien  15934  uspgrupgrushgr  15945  usgrumgr  15947  usgrumgruspgr  15948  usgruspgrben  15949  usgrislfuspgrdom  15953  edgssv2en  15962  usgrf1oedg  15968  usgredg4  15978  usgredg2vlem2  15986  usgredg2v  15987  ushgredgedg  15989  ushgredgedgloop  15991  usgrstrrepeen  15994  fnmptd  16078  bj-sels  16187  bj-nnelon  16232  2omap  16270  pw1map  16272  pwle2  16275  pwf1oexmid  16276  pw1nct  16280  nninfall  16286  nninfsellemdc  16287  nninfself  16290  nnnninfex  16299  nninfnfiinf  16300  refeq  16307  isomninnlem  16309  cvgcmp2nlemabs  16311  trilpolemlt1  16320  trirec0  16323  apdifflemf  16325  apdifflemr  16326  apdiff  16327  iswomninnlem  16328  iswomni0  16330  ismkvnnlem  16331  reap0  16337  cndcap  16338