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  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  5522  fimadmfo  5559  sefvex  5650  fdmeu  5679  fvun1  5702  eqfnfvd  5737  fvimacnvi  5751  fvimacnv  5752  fvelrn  5768  fmpt3d  5793  fmpt2d  5799  resflem  5801  fmptco  5803  fsn  5809  funopsn  5819  fncofn  5821  ftpg  5827  fconst2g  5858  funfvima3  5877  elabrexg  5888  foeqcnvco  5920  f1eqcocnv  5921  fliftfun  5926  fliftfund  5927  fliftval  5930  riota5f  5987  f1ofveu  5995  f1ocnvd  6214  f1opw2  6218  off  6237  offval2  6240  ofrfval2  6241  offveq  6245  caofref  6249  caofinvl  6250  elxp6  6321  cnvf1olem  6376  f2ndf  6378  f1od2  6387  tposf12  6421  smores2  6446  tfrlemisucaccv  6477  tfrlemibfn  6480  tfr1onlemsucaccv  6493  tfr1onlembfn  6496  tfrcllemsucaccv  6506  tfrcllembfn  6509  tfrcl  6516  tfri3  6519  frecabcl  6551  nnsucsssuc  6646  ersym  6700  ertr  6703  swoer  6716  erth  6734  riinerm  6763  qliftfund  6773  eroprf  6783  ecopoverg  6791  th3qlem1  6792  elmapssres  6828  mapss  6846  fdiagfn  6847  ixpssmap2g  6882  mapsnf1o  6892  f1oen4g  6911  f1dom4g  6912  f1dom2g  6915  dom3d  6933  en2prd  6978  dom1oi  6986  pw2f1odclem  7003  fopwdom  7005  mapxpen  7017  nndomo  7033  dif1en  7049  findcard2  7059  findcard2s  7060  diffisn  7063  fimax2gtrilemstep  7070  fientri3  7085  tpfidceq  7100  fiintim  7101  opabfi  7108  f1dmvrnfibi  7119  sbthlemi6  7137  elfir  7148  fifo  7155  supelti  7177  supsnti  7180  cnvinfex  7193  ordiso2  7210  updjud  7257  djudom  7268  difinfsn  7275  ctssdc  7288  enumctlemm  7289  enumct  7290  nninfninc  7298  enomnilem  7313  fodjuf  7320  ismkvnex  7330  omnimkv  7331  enmkvlem  7336  enwomnilem  7344  nninfdcinf  7346  nninfwlporlem  7348  isnumi  7362  exmidfodomrlemrALT  7389  finacn  7394  djudoml  7409  djudomr  7410  netap  7448  2omotaplemap  7451  2omotaplemst  7452  exmidapne  7454  cc2lem  7460  cc3  7462  ltsopi  7515  pitri3or  7517  ltdcpi  7518  indpi  7537  enqdc  7556  enqdc1  7557  addcmpblnq  7562  mulcanenq  7580  recrecnq  7589  nqtri3or  7591  ltdcnq  7592  ltsonq  7593  ltaddnq  7602  subhalfnqq  7609  archnqq  7612  prarloclemarch2  7614  enq0tr  7629  nqnq0  7636  addcmpblnq0  7638  mulcanenq0ec  7640  nnnq0lem1  7641  nqpnq0nq  7648  nq0m0r  7651  nq02m  7660  prarloclemlt  7688  prarloclemcalc  7697  addlocpr  7731  nqprl  7746  nqpru  7747  addnqprlemrl  7752  addnqprlemru  7753  prmuloclemcalc  7760  mullocprlem  7765  mulnqprlemrl  7768  mulnqprlemru  7769  1idprl  7785  1idpru  7786  ltaddpr  7792  ltexprlemm  7795  ltexprlemopl  7796  ltexprlemopu  7798  ltexprlemdisj  7801  ltexprlemrl  7805  ltexprlemru  7807  addcanprleml  7809  addcanprlemu  7810  addcanprg  7811  prplnqu  7815  recexprlemloc  7826  recexprlem1ssl  7828  recexprlem1ssu  7829  aptiprleml  7834  aptiprlemu  7835  archpr  7838  cauappcvgprlemm  7840  cauappcvgprlemopl  7841  cauappcvgprlemloc  7847  cauappcvgprlemladdfu  7849  cauappcvgprlemladdfl  7850  cauappcvgprlem1  7854  cauappcvgprlem2  7855  caucvgprlemnkj  7861  caucvgprlemopl  7864  caucvgprlemloc  7870  caucvgprlemladdfu  7872  caucvgprlem2  7875  caucvgprprlemnkltj  7884  caucvgprprlemopl  7892  caucvgprprlemloc  7898  caucvgprprlemexbt  7901  caucvgprprlemaddq  7903  caucvgprprlem2  7905  suplocexprlemmu  7913  suplocexprlemru  7914  suplocexprlemloc  7916  suplocexprlemlub  7919  prsrlem1  7937  0idsr  7962  1idsr  7963  recexgt0sr  7968  archsr  7977  prsradd  7981  caucvgsrlemcau  7988  caucvgsrlembound  7989  caucvgsrlemoffgt1  7994  suplocsrlemb  8001  suplocsrlempr  8002  suplocsrlem  8003  pitonnlem1p1  8041  pitonn  8043  pitoregt0  8044  peano2nnnn  8048  recidpirq  8053  axcaucvglemval  8092  leid  8238  nltled  8275  readdcan  8294  addneintrd  8342  addneintr2d  8343  pncan  8360  subsub2  8382  subsub4  8387  negned  8462  subne0d  8474  subneintrd  8509  subneintr2d  8511  subeq0bd  8533  subdi  8539  gt0add  8728  rimul  8740  rereim  8741  ltmul1a  8746  apreim  8758  apirr  8760  mulap0r  8770  msqge0  8771  mulge0  8774  gt0ap0  8781  ltap  8788  subap0d  8799  recexaplem2  8807  mulap0bad  8814  mulap0bbd  8815  mul0eqap  8825  divrecap  8843  div0ap  8857  div1  8858  recrecap  8864  divdivdivap  8868  ddcanap  8881  rerecclap  8885  div2negap  8890  diveqap1bd  8991  recgt0  9005  prodgt0  9007  lemul1a  9013  recp1lt1  9054  squeeze0  9059  peano2nn  9130  div4p1lem1div2  9373  arch  9374  peano2z  9490  peano2zm  9492  ztri3or  9497  nn0n0n1ge2  9525  zextle  9546  gtndiv  9550  suprzclex  9553  nn0ind-raph  9572  uzid  9744  uzneg  9749  uztric  9752  uz11  9753  eluzp1l  9755  qdivcl  9846  irrmul  9850  irrmulap  9851  rpnegap  9890  negelrpd  9892  ledivge1le  9930  mul2lt0rlt0  9963  mul2lt0rgt0  9964  nn0ledivnn  9971  ltpnf  9984  mnflt  9987  pnfge  9993  mnfle  9996  xrlttr  9999  xrltso  10000  xrlttri3  10001  xrleid  10004  xaddass2  10074  xltadd1  10080  xlt2add  10084  xleaddadd  10091  iccf1o  10208  fztri3or  10243  fznlem  10245  fzn  10246  fzsplit2  10254  fznatpl1  10280  uzsplit  10296  fseq1p1m1  10298  fzm1  10304  fznn0sub2  10332  difelfznle  10339  1fv  10343  fzodcel  10357  fzospliti  10382  fzouzsplit  10385  eluzgtdifelfzo  10411  exfzdc  10454  subfzo0  10456  zsupcllemstep  10457  zsupcl  10459  zssinfcl  10460  infssuzex  10461  infssuzcldc  10463  suprzubdc  10464  nninfdcex  10465  qdcle  10474  exbtwnz  10478  qbtwnrelemcalc  10483  flqlelt  10504  qfraclt1  10508  qfracge0  10509  flqltnz  10515  btwnzge0  10528  flhalf  10530  fldiv4lem1div2uz2  10534  ceiqle  10543  intfracq  10550  mulqmod0  10560  modqge0  10562  modqlt  10563  modqid  10579  modqid0  10580  m1modge3gt1  10601  modqltm1p1mod  10606  q2txmodxeq0  10614  modaddmodlo  10618  modsumfzodifsn  10626  addmodlteq  10628  frecuzrdgtcl  10642  frecuzrdgtclt  10651  uzennn  10666  uzsinds  10674  seqf  10694  seqf2  10698  monoord2  10716  iseqf1olemqk  10737  iseqf1olemjpcl  10738  iseqf1olemqpcl  10739  seq3f1olemqsumkj  10741  seq3f1olemqsum  10743  seq3f1olemstep  10744  seq3f1oleml  10746  seqf1oglem1  10749  ser3le  10767  exp3vallem  10770  exp3val  10771  expp1  10776  expcllem  10780  ltexp2a  10821  leexp2a  10822  nn0ltexp2  10939  faclbnd  10971  faclbnd2  10972  faclbnd3  10973  bcval5  10993  bcpasc  10996  hashennn  11010  fihasheqf1oi  11017  hashsng  11028  fihashfn  11030  hashun  11035  fihashss  11046  fihashssdif  11048  hashfz  11051  hashxp  11056  fimaxq  11057  zfz1isolem1  11070  seq3coll  11072  hashdmprop2dom  11074  wrdf  11085  wrdlenge2n0  11115  fstwrdne0  11119  wrdred1hash  11123  ccatvalfn  11144  ccatsymb  11145  ccatlid  11149  ccatrid  11150  ccatrn  11152  eqs1  11169  ccats1val2  11179  fzowrddc  11187  swrdlen  11192  swrdnd  11199  swrd0g  11200  swrdfv2  11203  swrdwrdsymbg  11204  pfxn0  11228  pfxwrdsymbg  11230  pfxsuff1eqwrdeq  11239  swrdswrd  11245  ccats1pfxeq  11254  ccats1pfxeqrex  11255  wrdind  11262  wrd2ind  11263  swrdccatin1  11265  pfxccatin12lem4  11266  swrdccatin2  11269  pfxccatin12  11273  pfxccat3a  11278  swrdccat3blem  11279  pfxccatid  11281  swrdccatin2d  11284  shftfn  11343  cjth  11365  cjmulrcl  11406  reim0bd  11463  rerebd  11464  cjrebd  11465  caucvgre  11500  cvg1nlemcxze  11501  cvg1nlemcau  11503  cvg1nlemres  11504  recvguniq  11514  resqrexlemover  11529  resqrexlemdec  11530  resqrexlemgt0  11539  resqrexlemoverl  11540  resqrexlemglsq  11541  rersqrtthlem  11549  sqrtgt0  11553  leabs  11593  absexpzap  11599  absle  11608  recvalap  11616  abstri  11623  abs2dif  11625  amgm2  11637  absne0d  11706  maxleim  11724  maxabslemab  11725  maxabslemlub  11726  maxltsup  11737  zmaxcl  11743  fimaxre2  11746  minmax  11749  rpmincl  11757  bdtrilem  11758  bdtri  11759  xrmaxleim  11763  xrmaxiflemcom  11768  xrmaxltsup  11777  xrmaxadd  11780  xrminmax  11784  xrminrpcl  11793  climconst  11809  climuni  11812  2clim  11820  climcn1  11827  climcn2  11828  reccn2ap  11832  climge0  11844  climle  11853  climsqz  11854  climsqz2  11855  serf0  11871  summodclem3  11899  summodclem2a  11900  fsumcl2lem  11917  sumpr  11932  sumtp  11933  fsum0diaglem  11959  mptfzshft  11961  fsumle  11982  fsumlt  11983  divcnv  12016  trireciplem  12019  expcnvap0  12021  expcnv  12023  explecnv  12024  geosergap  12025  cvgratnnlembern  12042  cvgratnnlemabsle  12046  cvgratnnlemsumlt  12047  cvgratz  12051  cvgratgt0  12052  mertenslemi1  12054  mertenslem2  12055  mertensabs  12056  clim2divap  12059  prodmodclem3  12094  prodmodclem2a  12095  fprodseq  12102  fprodmul  12110  fprodfac  12134  fprodconst  12139  fprodap0  12140  fprodap0f  12155  fprodle  12159  eftcl  12173  ef0lem  12179  efsub  12200  eftlub  12209  eflegeo  12220  tanval2ap  12232  sinadd  12255  cos2t  12269  cos2tsin  12270  sin01bnd  12276  cos01bnd  12277  eirraplem  12296  dvdsval2  12309  dvdsdc  12317  dvds0lem  12320  zdvdsdc  12331  dvdscmulr  12339  dvdsmulcr  12340  fsumdvds  12361  dvdslelemd  12362  divconjdvds  12368  dvdsext  12374  fzm1ndvds  12375  dvdsmod  12381  3dvds  12383  oexpneg  12396  2tp1odd  12403  mulsucdiv2z  12404  2teven  12406  zeo5  12407  opeo  12416  omeo  12417  nn0ob  12427  divalglemnqt  12439  bitsdc  12466  bits0o  12469  bitsfzolem  12473  bitsfzo  12474  bitsmod  12475  bitscmp  12477  bitsinv1lem  12480  gcddvds  12492  dvdslegcd  12493  gcdneg  12511  bezoutlemnewy  12525  bezoutlemstep  12526  bezoutlema  12528  bezoutlemb  12529  bezoutlemmo  12535  bezoutlemle  12537  bezoutlemsup  12538  dfgcd3  12539  bezout  12540  dfgcd2  12543  uzwodc  12566  lcmcllem  12597  lcmneg  12604  lcmgcdlem  12607  lcmdvds  12609  lcmid  12610  3lcm2e6woprm  12616  6lcm4e12  12617  ncoprmgcdne1b  12619  mulgcddvds  12624  divgcdcoprmex  12632  cncongr1  12633  cncongr2  12634  isprm2lem  12646  prmind2  12650  dvdsnprmd  12655  prm2orodd  12656  sqnprm  12666  isprm5lem  12671  rpexp  12683  sqrt2irrlem  12691  oddpwdclemdc  12703  sqrt2irraplemnn  12709  qnumdencoprm  12723  qeqnumdivden  12724  nn0gcdsq  12730  nn0sqrtelqelz  12736  nonsq  12737  phicl2  12744  phibnd  12747  hashdvds  12751  phiprmpw  12752  phimullem  12755  eulerthlemrprm  12759  eulerthlema  12760  eulerthlemth  12762  prmdiveq  12766  hashgcdlem  12768  odzdvds  12776  modprminv  12780  nnnn0modprm0  12786  modprmn0modprm0  12787  pythagtriplem10  12800  pythagtriplem19  12813  pythagtrip  12814  pcpre1  12823  pcpremul  12824  pceu  12826  pcmul  12832  pcdiv  12833  pcqmul  12834  pcqdiv  12838  pcexp  12840  pcdvdsb  12851  pcidlem  12854  pcdvdstr  12858  pcgcd1  12859  pc2dvds  12861  pcprmpw2  12864  difsqpwdvds  12869  pcaddlem  12870  pcadd  12871  pcadd2  12872  pcmpt  12874  pcmptdvds  12876  pcprod  12877  fldivp1  12879  pcfaclem  12880  pcfac  12881  pcbc  12882  qexpz  12883  pockthlem  12887  pockthg  12888  1arithlem4  12897  1arith  12898  1arith2  12899  4sqlem6  12914  4sqlem8  12916  4sqlem9  12917  4sqlem10  12918  4sqexercise1  12929  4sqexercise2  12930  4sqlemsdc  12931  4sqlem11  12932  4sqlem12  12933  4sqlem15  12936  4sqlem16  12937  4sqlem17  12938  znnen  12977  ennnfonelemk  12979  ennnfonelemkh  12991  ennnfonelemhf1o  12992  ennnfonelemrnh  12995  ennnfonelemfun  12996  ennnfonelemf1  12997  ennnfonelemrn  12998  ennnfonelemnn0  13001  ctinfomlemom  13006  ctiunctlemudc  13016  unct  13021  omctfn  13022  ssnnctlemct  13025  nninfdclemp1  13029  nninfdc  13032  structfung  13057  setsfun  13075  setsfun0  13076  setscom  13080  strslfv3  13086  setsslid  13091  pwsdiagel  13338  pwssnf1o  13339  imasaddfnlemg  13355  imasaddvallemg  13356  mgmsscl  13402  plusffng  13406  mgmplusf  13407  mgm0  13410  mgm1  13411  opifismgmdc  13412  gsumfzval  13432  gsumprval  13440  sgrp1  13452  issgrpd  13453  prdsplusgsgrpcl  13455  mndpfo  13479  mndfo  13480  prdsplusgcl  13487  prdsidlem  13488  mnd1  13496  0subm  13525  mhmima  13532  grpinvfng  13585  isgrpinv  13595  grpinvid  13601  grpinvf1o  13611  grpinvadd  13619  grpsubf  13620  grpsubsub4  13634  grplactcnv  13643  grp1  13647  grp1inv  13648  prdsinvlem  13649  prdsinvgd  13651  qusgrp2  13658  mulgfng  13669  subginv  13726  resgrpisgrp  13740  subgintm  13743  0subg  13744  0nsg  13759  qusinv  13781  ghminv  13795  ghmrn  13802  ghmeql  13812  ghmnsgima  13813  kerf1ghm  13819  conjnmz  13824  rngass  13910  rngmneg1  13918  rngmneg2  13919  qusrng  13929  srgideu  13943  srgidmlem  13949  srgpcomp  13961  srg1expzeq1  13966  ringcl  13984  ringideu  13988  ringidmlem  13993  ringnegl  14022  ringnegr  14023  ring1  14030  qusring2  14037  opprringbg  14051  dvdsrd  14066  dvdsr01  14076  isunitd  14078  unitinvcl  14095  unitinvinv  14096  unitnegcl  14102  rhmmul  14136  rhmf1o  14140  nzrunit  14160  lringuplu  14168  subrngintm  14184  subrgsubm  14206  subrgintm  14215  aprsym  14256  scaffng  14281  lmodscaf  14282  lsssn0  14342  lss1d  14355  lssintclm  14356  lspval  14362  lspcl  14363  lspsnid  14379  lspprid1  14383  lspsn  14388  sraval  14409  rspcl  14463  rspssid  14464  rspssp  14466  rnglidlmmgm  14468  rnglidlmsgrp  14469  cnfldneg  14545  zringinvg  14576  expghmap  14579  znzrhfo  14620  znf1o  14623  znhash  14628  znidomb  14630  znrrg  14632  psrbagfi  14645  psraddcl  14652  psr0cl  14653  psrnegcl  14655  psrneg  14659  psr1clfi  14660  mplsubgfilemm  14670  mplsubgfilemcl  14671  baspartn  14732  eltg3i  14738  tgclb  14747  topbas  14749  2basgeng  14764  topcld  14791  0cld  14794  uncld  14795  neif  14823  elnei  14834  0nei  14848  restbasg  14850  iscnp4  14900  cnpnei  14901  cnclima  14905  cncnp  14912  cnrest2r  14919  cndis  14923  lmff  14931  lmtopcnp  14932  txbas  14940  txopn  14947  txcnp  14953  upxp  14954  txdis1cn  14960  cnmpt11  14965  cnmpt21  14973  psmetge0  15013  xmetge0  15047  xmettpos  15052  xmetrtri  15058  metrtri  15059  xblpnfps  15080  xblpnf  15081  blfps  15091  blf  15092  ssblps  15107  ssbl  15108  blbas  15115  metss2  15180  xmettxlem  15191  xmettx  15192  qtopbas  15204  divcnap  15247  cncfss  15265  cdivcncfap  15286  expcncf  15291  cnopnap  15293  maxcncf  15297  mincncf  15298  dedekindeulemuub  15299  dedekindeulemlu  15303  dedekindeu  15305  suplociccex  15307  dedekindicclemuub  15308  dedekindicclemlu  15312  dedekindicclemicc  15314  ivthinclemlopn  15318  ivthinclemuopn  15320  ivthinc  15325  ivthreinc  15327  hoverlt1  15331  ellimc3apf  15342  limcimolemlt  15346  limcimo  15347  limcresi  15348  cnplimclemle  15350  reldvg  15361  dvfgg  15370  dvidlemap  15373  dvidrelem  15374  dvidsslem  15375  dvcjbr  15390  dvcj  15391  dvrecap  15395  dveflem  15408  dvef  15409  elply2  15417  elplyr  15422  plycj  15443  plyreres  15446  reeff1oleme  15454  pilem3  15465  sinq34lt0t  15513  cosq14gt0  15514  coseq0q4123  15516  tangtx  15520  sincosq1eq  15521  cosordlem  15531  logdivlti  15563  relogbval  15633  relogbzcl  15634  nnlogbexp  15641  logbgcd1irr  15649  logbgcd1irraplemexp  15650  logbgcd1irraplemap  15651  wilthlem1  15662  mpodvdsmulf1o  15672  mersenne  15679  perfectlem2  15682  perfect  15683  zabsle1  15686  lgslem1  15687  lgsval  15691  lgsfvalg  15692  lgsfcl2  15693  lgsval2lem  15697  lgscl1  15710  lgsmod  15713  lgsdir2lem5  15719  lgsdir2  15720  lgsdilem2  15723  lgsdi  15724  lgsne0  15725  gausslemma2dlem0c  15738  gausslemma2dlem0h  15743  gausslemma2dlem1a  15745  gausslemma2dlem1f1o  15747  gausslemma2dlem3  15750  lgseisenlem1  15757  lgseisenlem2  15758  lgseisenlem3  15759  lgseisenlem4  15760  lgseisen  15761  lgsquadlem1  15764  lgsquadlem2  15765  lgsquadlem3  15766  lgsquad3  15771  2lgslem3b1  15785  2lgslem3c1  15786  2lgs  15791  2lgsoddprmlem2  15793  2lgsoddprm  15800  2sqlem3  15804  2sqlem8  15810  2sqlem10  15812  structgrssvtx  15851  structgrssiedg  15852  ushgruhgr  15888  uhgrun  15894  incistruhgr  15898  upgrop  15912  upgruhgr  15919  umgrupgr  15920  umgrnloopv  15922  umgredgprv  15923  umgr0e  15926  upgr1edc  15929  upgrun  15932  umgrun  15934  umgrislfupgrdom  15937  upgredg  15950  umgrpredgv  15953  usgrop  15972  usgrausgrien  15975  ausgrumgrien  15976  ausgrusgrien  15977  uspgrupgrushgr  15988  usgrumgr  15990  usgrumgruspgr  15991  usgruspgrben  15992  usgrislfuspgrdom  15996  edgssv2en  16005  usgrf1oedg  16011  usgredg4  16021  usgredg2vlem2  16029  usgredg2v  16030  ushgredgedg  16032  ushgredgedgloop  16034  usgrstrrepeen  16037  wlkm  16060  wlkvtxiedg  16066  wlkvtxiedgg  16067  wlkeq  16075  wlk1walkdom  16080  uspgr2wlkeq  16086  uspgr2wlkeqi  16088  upgr2wlkdc  16096  wlkres  16098  trlreslem  16107  fnmptd  16192  bj-sels  16301  bj-nnelon  16346  2omap  16388  pw1map  16390  pwle2  16393  pwf1oexmid  16394  pw1nct  16398  nninfall  16405  nninfsellemdc  16406  nninfself  16409  nnnninfex  16418  nninfnfiinf  16419  refeq  16426  isomninnlem  16428  cvgcmp2nlemabs  16430  trilpolemlt1  16439  trirec0  16442  apdifflemf  16444  apdifflemr  16445  apdiff  16446  iswomninnlem  16447  iswomni0  16449  ismkvnnlem  16450  reap0  16456  cndcap  16457