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  4298  prelpwi  4301  pwel  4305  ordelon  4475  onin  4478  elelsuc  4501  onsuc  4594  onsucb  4596  onintonm  4610  omsinds  4715  sosng  4794  relssdv  4813  eqbrrdv  4818  eqrelrdv2  4820  relsnopg  4825  breldmg  4932  elrnmptdv  4981  iss  5054  xpimasn  5180  elxp4  5219  elxp5  5220  iotam  5313  funssres  5363  f0rn0  5525  fimadmfo  5562  sefvex  5653  fdmeu  5682  fvun1  5705  eqfnfvd  5740  fvimacnvi  5754  fvimacnv  5755  fvelrn  5771  fmpt3d  5796  fmpt2d  5802  resflem  5804  fmptco  5806  fsn  5812  funopsn  5822  fncofn  5824  ftpg  5830  fconst2g  5861  funfvima3  5880  elabrexg  5891  foeqcnvco  5923  f1eqcocnv  5924  fliftfun  5929  fliftfund  5930  fliftval  5933  riota5f  5990  f1ofveu  5998  f1ocnvd  6217  f1opw2  6221  off  6240  offval2  6243  ofrfval2  6244  offveq  6248  caofref  6252  caofinvl  6253  elxp6  6324  cnvf1olem  6381  f2ndf  6383  f1od2  6392  tposf12  6426  smores2  6451  tfrlemisucaccv  6482  tfrlemibfn  6485  tfr1onlemsucaccv  6498  tfr1onlembfn  6501  tfrcllemsucaccv  6511  tfrcllembfn  6514  tfrcl  6521  tfri3  6524  frecabcl  6556  nnsucsssuc  6651  ersym  6705  ertr  6708  swoer  6721  erth  6739  riinerm  6768  qliftfund  6778  eroprf  6788  ecopoverg  6796  th3qlem1  6797  elmapssres  6833  mapss  6851  fdiagfn  6852  ixpssmap2g  6887  mapsnf1o  6897  f1oen4g  6916  f1dom4g  6917  f1dom2g  6920  dom3d  6938  en2prd  6983  dom1oi  6991  pw2f1odclem  7008  fopwdom  7010  mapxpen  7022  nndomo  7038  dif1en  7054  findcard2  7064  findcard2s  7065  diffisn  7068  fimax2gtrilemstep  7076  eqsndc  7081  fientri3  7093  tpfidceq  7108  fiintim  7109  opabfi  7116  f1dmvrnfibi  7127  sbthlemi6  7145  elfir  7156  fifo  7163  supelti  7185  supsnti  7188  cnvinfex  7201  ordiso2  7218  updjud  7265  djudom  7276  difinfsn  7283  ctssdc  7296  enumctlemm  7297  enumct  7298  nninfninc  7306  enomnilem  7321  fodjuf  7328  ismkvnex  7338  omnimkv  7339  enmkvlem  7344  enwomnilem  7352  nninfdcinf  7354  nninfwlporlem  7356  isnumi  7370  exmidfodomrlemrALT  7397  finacn  7402  djudoml  7417  djudomr  7418  netap  7456  2omotaplemap  7459  2omotaplemst  7460  exmidapne  7462  cc2lem  7468  cc3  7470  ltsopi  7523  pitri3or  7525  ltdcpi  7526  indpi  7545  enqdc  7564  enqdc1  7565  addcmpblnq  7570  mulcanenq  7588  recrecnq  7597  nqtri3or  7599  ltdcnq  7600  ltsonq  7601  ltaddnq  7610  subhalfnqq  7617  archnqq  7620  prarloclemarch2  7622  enq0tr  7637  nqnq0  7644  addcmpblnq0  7646  mulcanenq0ec  7648  nnnq0lem1  7649  nqpnq0nq  7656  nq0m0r  7659  nq02m  7668  prarloclemlt  7696  prarloclemcalc  7705  addlocpr  7739  nqprl  7754  nqpru  7755  addnqprlemrl  7760  addnqprlemru  7761  prmuloclemcalc  7768  mullocprlem  7773  mulnqprlemrl  7776  mulnqprlemru  7777  1idprl  7793  1idpru  7794  ltaddpr  7800  ltexprlemm  7803  ltexprlemopl  7804  ltexprlemopu  7806  ltexprlemdisj  7809  ltexprlemrl  7813  ltexprlemru  7815  addcanprleml  7817  addcanprlemu  7818  addcanprg  7819  prplnqu  7823  recexprlemloc  7834  recexprlem1ssl  7836  recexprlem1ssu  7837  aptiprleml  7842  aptiprlemu  7843  archpr  7846  cauappcvgprlemm  7848  cauappcvgprlemopl  7849  cauappcvgprlemloc  7855  cauappcvgprlemladdfu  7857  cauappcvgprlemladdfl  7858  cauappcvgprlem1  7862  cauappcvgprlem2  7863  caucvgprlemnkj  7869  caucvgprlemopl  7872  caucvgprlemloc  7878  caucvgprlemladdfu  7880  caucvgprlem2  7883  caucvgprprlemnkltj  7892  caucvgprprlemopl  7900  caucvgprprlemloc  7906  caucvgprprlemexbt  7909  caucvgprprlemaddq  7911  caucvgprprlem2  7913  suplocexprlemmu  7921  suplocexprlemru  7922  suplocexprlemloc  7924  suplocexprlemlub  7927  prsrlem1  7945  0idsr  7970  1idsr  7971  recexgt0sr  7976  archsr  7985  prsradd  7989  caucvgsrlemcau  7996  caucvgsrlembound  7997  caucvgsrlemoffgt1  8002  suplocsrlemb  8009  suplocsrlempr  8010  suplocsrlem  8011  pitonnlem1p1  8049  pitonn  8051  pitoregt0  8052  peano2nnnn  8056  recidpirq  8061  axcaucvglemval  8100  leid  8246  nltled  8283  readdcan  8302  addneintrd  8350  addneintr2d  8351  pncan  8368  subsub2  8390  subsub4  8395  negned  8470  subne0d  8482  subneintrd  8517  subneintr2d  8519  subeq0bd  8541  subdi  8547  gt0add  8736  rimul  8748  rereim  8749  ltmul1a  8754  apreim  8766  apirr  8768  mulap0r  8778  msqge0  8779  mulge0  8782  gt0ap0  8789  ltap  8796  subap0d  8807  recexaplem2  8815  mulap0bad  8822  mulap0bbd  8823  mul0eqap  8833  divrecap  8851  div0ap  8865  div1  8866  recrecap  8872  divdivdivap  8876  ddcanap  8889  rerecclap  8893  div2negap  8898  diveqap1bd  8999  recgt0  9013  prodgt0  9015  lemul1a  9021  recp1lt1  9062  squeeze0  9067  peano2nn  9138  div4p1lem1div2  9381  arch  9382  peano2z  9498  peano2zm  9500  ztri3or  9505  nn0n0n1ge2  9533  zextle  9554  gtndiv  9558  suprzclex  9561  nn0ind-raph  9580  uzid  9753  uzneg  9758  uztric  9761  uz11  9762  eluzp1l  9764  qdivcl  9855  irrmul  9859  irrmulap  9860  rpnegap  9899  negelrpd  9901  ledivge1le  9939  mul2lt0rlt0  9972  mul2lt0rgt0  9973  nn0ledivnn  9980  ltpnf  9993  mnflt  9996  pnfge  10002  mnfle  10005  xrlttr  10008  xrltso  10009  xrlttri3  10010  xrleid  10013  xaddass2  10083  xltadd1  10089  xlt2add  10093  xleaddadd  10100  iccf1o  10217  fztri3or  10252  fznlem  10254  fzn  10255  fzsplit2  10263  fznatpl1  10289  uzsplit  10305  fseq1p1m1  10307  fzm1  10313  fznn0sub2  10341  difelfznle  10348  1fv  10352  fzodcel  10366  fzospliti  10391  fzouzsplit  10394  eluzgtdifelfzo  10420  exfzdc  10463  subfzo0  10465  zsupcllemstep  10466  zsupcl  10468  zssinfcl  10469  infssuzex  10470  infssuzcldc  10472  suprzubdc  10473  nninfdcex  10474  qdcle  10483  exbtwnz  10487  qbtwnrelemcalc  10492  flqlelt  10513  qfraclt1  10517  qfracge0  10518  flqltnz  10524  btwnzge0  10537  flhalf  10539  fldiv4lem1div2uz2  10543  ceiqle  10552  intfracq  10559  mulqmod0  10569  modqge0  10571  modqlt  10572  modqid  10588  modqid0  10589  m1modge3gt1  10610  modqltm1p1mod  10615  q2txmodxeq0  10623  modaddmodlo  10627  modsumfzodifsn  10635  addmodlteq  10637  frecuzrdgtcl  10651  frecuzrdgtclt  10660  uzennn  10675  uzsinds  10683  seqf  10703  seqf2  10707  monoord2  10725  iseqf1olemqk  10746  iseqf1olemjpcl  10747  iseqf1olemqpcl  10748  seq3f1olemqsumkj  10750  seq3f1olemqsum  10752  seq3f1olemstep  10753  seq3f1oleml  10755  seqf1oglem1  10758  ser3le  10776  exp3vallem  10779  exp3val  10780  expp1  10785  expcllem  10789  ltexp2a  10830  leexp2a  10831  nn0ltexp2  10948  faclbnd  10980  faclbnd2  10981  faclbnd3  10982  bcval5  11002  bcpasc  11005  hashennn  11019  fihasheqf1oi  11026  hashsng  11037  fihashfn  11039  hashun  11044  fihashss  11056  fihashssdif  11058  hashfz  11061  hashxp  11066  fimaxq  11067  zfz1isolem1  11080  seq3coll  11082  hashdmprop2dom  11084  wrdf  11095  wrdlenge2n0  11125  fstwrdne0  11129  wrdred1hash  11133  ccatvalfn  11154  ccatsymb  11155  ccatlid  11159  ccatrid  11160  ccatrn  11162  ccatalpha  11166  eqs1  11181  ccats1val2  11192  fzowrddc  11200  swrdlen  11205  swrdnd  11212  swrd0g  11213  swrdfv2  11216  swrdwrdsymbg  11217  pfxn0  11241  pfxwrdsymbg  11243  pfxsuff1eqwrdeq  11252  swrdswrd  11258  ccats1pfxeq  11267  ccats1pfxeqrex  11268  wrdind  11275  wrd2ind  11276  swrdccatin1  11278  pfxccatin12lem4  11279  swrdccatin2  11282  pfxccatin12  11286  pfxccat3a  11291  swrdccat3blem  11292  pfxccatid  11294  swrdccatin2d  11297  shftfn  11356  cjth  11378  cjmulrcl  11419  reim0bd  11476  rerebd  11477  cjrebd  11478  caucvgre  11513  cvg1nlemcxze  11514  cvg1nlemcau  11516  cvg1nlemres  11517  recvguniq  11527  resqrexlemover  11542  resqrexlemdec  11543  resqrexlemgt0  11552  resqrexlemoverl  11553  resqrexlemglsq  11554  rersqrtthlem  11562  sqrtgt0  11566  leabs  11606  absexpzap  11612  absle  11621  recvalap  11629  abstri  11636  abs2dif  11638  amgm2  11650  absne0d  11719  maxleim  11737  maxabslemab  11738  maxabslemlub  11739  maxltsup  11750  zmaxcl  11756  fimaxre2  11759  minmax  11762  rpmincl  11770  bdtrilem  11771  bdtri  11772  xrmaxleim  11776  xrmaxiflemcom  11781  xrmaxltsup  11790  xrmaxadd  11793  xrminmax  11797  xrminrpcl  11806  climconst  11822  climuni  11825  2clim  11833  climcn1  11840  climcn2  11841  reccn2ap  11845  climge0  11857  climle  11866  climsqz  11867  climsqz2  11868  serf0  11884  summodclem3  11912  summodclem2a  11913  fsumcl2lem  11930  sumpr  11945  sumtp  11946  fsum0diaglem  11972  mptfzshft  11974  fsumle  11995  fsumlt  11996  divcnv  12029  trireciplem  12032  expcnvap0  12034  expcnv  12036  explecnv  12037  geosergap  12038  cvgratnnlembern  12055  cvgratnnlemabsle  12059  cvgratnnlemsumlt  12060  cvgratz  12064  cvgratgt0  12065  mertenslemi1  12067  mertenslem2  12068  mertensabs  12069  clim2divap  12072  prodmodclem3  12107  prodmodclem2a  12108  fprodseq  12115  fprodmul  12123  fprodfac  12147  fprodconst  12152  fprodap0  12153  fprodap0f  12168  fprodle  12172  eftcl  12186  ef0lem  12192  efsub  12213  eftlub  12222  eflegeo  12233  tanval2ap  12245  sinadd  12268  cos2t  12282  cos2tsin  12283  sin01bnd  12289  cos01bnd  12290  eirraplem  12309  dvdsval2  12322  dvdsdc  12330  dvds0lem  12333  zdvdsdc  12344  dvdscmulr  12352  dvdsmulcr  12353  fsumdvds  12374  dvdslelemd  12375  divconjdvds  12381  dvdsext  12387  fzm1ndvds  12388  dvdsmod  12394  3dvds  12396  oexpneg  12409  2tp1odd  12416  mulsucdiv2z  12417  2teven  12419  zeo5  12420  opeo  12429  omeo  12430  nn0ob  12440  divalglemnqt  12452  bitsdc  12479  bits0o  12482  bitsfzolem  12486  bitsfzo  12487  bitsmod  12488  bitscmp  12490  bitsinv1lem  12493  gcddvds  12505  dvdslegcd  12506  gcdneg  12524  bezoutlemnewy  12538  bezoutlemstep  12539  bezoutlema  12541  bezoutlemb  12542  bezoutlemmo  12548  bezoutlemle  12550  bezoutlemsup  12551  dfgcd3  12552  bezout  12553  dfgcd2  12556  uzwodc  12579  lcmcllem  12610  lcmneg  12617  lcmgcdlem  12620  lcmdvds  12622  lcmid  12623  3lcm2e6woprm  12629  6lcm4e12  12630  ncoprmgcdne1b  12632  mulgcddvds  12637  divgcdcoprmex  12645  cncongr1  12646  cncongr2  12647  isprm2lem  12659  prmind2  12663  dvdsnprmd  12668  prm2orodd  12669  sqnprm  12679  isprm5lem  12684  rpexp  12696  sqrt2irrlem  12704  oddpwdclemdc  12716  sqrt2irraplemnn  12722  qnumdencoprm  12736  qeqnumdivden  12737  nn0gcdsq  12743  nn0sqrtelqelz  12749  nonsq  12750  phicl2  12757  phibnd  12760  hashdvds  12764  phiprmpw  12765  phimullem  12768  eulerthlemrprm  12772  eulerthlema  12773  eulerthlemth  12775  prmdiveq  12779  hashgcdlem  12781  odzdvds  12789  modprminv  12793  nnnn0modprm0  12799  modprmn0modprm0  12800  pythagtriplem10  12813  pythagtriplem19  12826  pythagtrip  12827  pcpre1  12836  pcpremul  12837  pceu  12839  pcmul  12845  pcdiv  12846  pcqmul  12847  pcqdiv  12851  pcexp  12853  pcdvdsb  12864  pcidlem  12867  pcdvdstr  12871  pcgcd1  12872  pc2dvds  12874  pcprmpw2  12877  difsqpwdvds  12882  pcaddlem  12883  pcadd  12884  pcadd2  12885  pcmpt  12887  pcmptdvds  12889  pcprod  12890  fldivp1  12892  pcfaclem  12893  pcfac  12894  pcbc  12895  qexpz  12896  pockthlem  12900  pockthg  12901  1arithlem4  12910  1arith  12911  1arith2  12912  4sqlem6  12927  4sqlem8  12929  4sqlem9  12930  4sqlem10  12931  4sqexercise1  12942  4sqexercise2  12943  4sqlemsdc  12944  4sqlem11  12945  4sqlem12  12946  4sqlem15  12949  4sqlem16  12950  4sqlem17  12951  znnen  12990  ennnfonelemk  12992  ennnfonelemkh  13004  ennnfonelemhf1o  13005  ennnfonelemrnh  13008  ennnfonelemfun  13009  ennnfonelemf1  13010  ennnfonelemrn  13011  ennnfonelemnn0  13014  ctinfomlemom  13019  ctiunctlemudc  13029  unct  13034  omctfn  13035  ssnnctlemct  13038  nninfdclemp1  13042  nninfdc  13045  structfung  13070  setsfun  13088  setsfun0  13089  setscom  13093  strslfv3  13099  setsslid  13104  pwsdiagel  13351  pwssnf1o  13352  imasaddfnlemg  13368  imasaddvallemg  13369  mgmsscl  13415  plusffng  13419  mgmplusf  13420  mgm0  13423  mgm1  13424  opifismgmdc  13425  gsumfzval  13445  gsumprval  13453  sgrp1  13465  issgrpd  13466  prdsplusgsgrpcl  13468  mndpfo  13492  mndfo  13493  prdsplusgcl  13500  prdsidlem  13501  mnd1  13509  0subm  13538  mhmima  13545  grpinvfng  13598  isgrpinv  13608  grpinvid  13614  grpinvf1o  13624  grpinvadd  13632  grpsubf  13633  grpsubsub4  13647  grplactcnv  13656  grp1  13660  grp1inv  13661  prdsinvlem  13662  prdsinvgd  13664  qusgrp2  13671  mulgfng  13682  subginv  13739  resgrpisgrp  13753  subgintm  13756  0subg  13757  0nsg  13772  qusinv  13794  ghminv  13808  ghmrn  13815  ghmeql  13825  ghmnsgima  13826  kerf1ghm  13832  conjnmz  13837  rngass  13923  rngmneg1  13931  rngmneg2  13932  qusrng  13942  srgideu  13956  srgidmlem  13962  srgpcomp  13974  srg1expzeq1  13979  ringcl  13997  ringideu  14001  ringidmlem  14006  ringnegl  14035  ringnegr  14036  ring1  14043  qusring2  14050  opprringbg  14064  dvdsrd  14079  dvdsr01  14089  isunitd  14091  unitinvcl  14108  unitinvinv  14109  unitnegcl  14115  rhmmul  14149  rhmf1o  14153  nzrunit  14173  lringuplu  14181  subrngintm  14197  subrgsubm  14219  subrgintm  14228  aprsym  14269  scaffng  14294  lmodscaf  14295  lsssn0  14355  lss1d  14368  lssintclm  14369  lspval  14375  lspcl  14376  lspsnid  14392  lspprid1  14396  lspsn  14401  sraval  14422  rspcl  14476  rspssid  14477  rspssp  14479  rnglidlmmgm  14481  rnglidlmsgrp  14482  cnfldneg  14558  zringinvg  14589  expghmap  14592  znzrhfo  14633  znf1o  14636  znhash  14641  znidomb  14643  znrrg  14645  psrbagfi  14658  psraddcl  14665  psr0cl  14666  psrnegcl  14668  psrneg  14672  psr1clfi  14673  mplsubgfilemm  14683  mplsubgfilemcl  14684  baspartn  14745  eltg3i  14751  tgclb  14760  topbas  14762  2basgeng  14777  topcld  14804  0cld  14807  uncld  14808  neif  14836  elnei  14847  0nei  14861  restbasg  14863  iscnp4  14913  cnpnei  14914  cnclima  14918  cncnp  14925  cnrest2r  14932  cndis  14936  lmff  14944  lmtopcnp  14945  txbas  14953  txopn  14960  txcnp  14966  upxp  14967  txdis1cn  14973  cnmpt11  14978  cnmpt21  14986  psmetge0  15026  xmetge0  15060  xmettpos  15065  xmetrtri  15071  metrtri  15072  xblpnfps  15093  xblpnf  15094  blfps  15104  blf  15105  ssblps  15120  ssbl  15121  blbas  15128  metss2  15193  xmettxlem  15204  xmettx  15205  qtopbas  15217  divcnap  15260  cncfss  15278  cdivcncfap  15299  expcncf  15304  cnopnap  15306  maxcncf  15310  mincncf  15311  dedekindeulemuub  15312  dedekindeulemlu  15316  dedekindeu  15318  suplociccex  15320  dedekindicclemuub  15321  dedekindicclemlu  15325  dedekindicclemicc  15327  ivthinclemlopn  15331  ivthinclemuopn  15333  ivthinc  15338  ivthreinc  15340  hoverlt1  15344  ellimc3apf  15355  limcimolemlt  15359  limcimo  15360  limcresi  15361  cnplimclemle  15363  reldvg  15374  dvfgg  15383  dvidlemap  15386  dvidrelem  15387  dvidsslem  15388  dvcjbr  15403  dvcj  15404  dvrecap  15408  dveflem  15421  dvef  15422  elply2  15430  elplyr  15435  plycj  15456  plyreres  15459  reeff1oleme  15467  pilem3  15478  sinq34lt0t  15526  cosq14gt0  15527  coseq0q4123  15529  tangtx  15533  sincosq1eq  15534  cosordlem  15544  logdivlti  15576  relogbval  15646  relogbzcl  15647  nnlogbexp  15654  logbgcd1irr  15662  logbgcd1irraplemexp  15663  logbgcd1irraplemap  15664  wilthlem1  15675  mpodvdsmulf1o  15685  mersenne  15692  perfectlem2  15695  perfect  15696  zabsle1  15699  lgslem1  15700  lgsval  15704  lgsfvalg  15705  lgsfcl2  15706  lgsval2lem  15710  lgscl1  15723  lgsmod  15726  lgsdir2lem5  15732  lgsdir2  15733  lgsdilem2  15736  lgsdi  15737  lgsne0  15738  gausslemma2dlem0c  15751  gausslemma2dlem0h  15756  gausslemma2dlem1a  15758  gausslemma2dlem1f1o  15760  gausslemma2dlem3  15763  lgseisenlem1  15770  lgseisenlem2  15771  lgseisenlem3  15772  lgseisenlem4  15773  lgseisen  15774  lgsquadlem1  15777  lgsquadlem2  15778  lgsquadlem3  15779  lgsquad3  15784  2lgslem3b1  15798  2lgslem3c1  15799  2lgs  15804  2lgsoddprmlem2  15806  2lgsoddprm  15813  2sqlem3  15817  2sqlem8  15823  2sqlem10  15825  structgrssvtx  15864  structgrssiedg  15865  ushgruhgr  15901  uhgrun  15907  incistruhgr  15911  upgrop  15925  upgruhgr  15932  umgrupgr  15933  umgrnloopv  15935  umgredgprv  15936  umgr0e  15939  upgr1edc  15942  upgrun  15945  umgrun  15947  umgrislfupgrdom  15950  upgredg  15963  umgrpredgv  15966  usgrop  15985  usgrausgrien  15988  ausgrumgrien  15989  ausgrusgrien  15990  uspgrupgrushgr  16001  usgrumgr  16003  usgrumgruspgr  16004  usgruspgrben  16005  usgrislfuspgrdom  16009  edgssv2en  16018  usgrf1oedg  16024  usgredg4  16034  usgredg2vlem2  16042  usgredg2v  16043  ushgredgedg  16045  ushgredgedgloop  16047  usgrstrrepeen  16050  usgr0e  16051  uhgr0v0e  16053  uspgr1edc  16059  usgr1e  16060  griedg0ssusgr  16070  wlkm  16111  wlkvtxiedg  16117  wlkvtxiedgg  16118  wlkeq  16126  wlk1walkdom  16131  uspgr2wlkeq  16137  uspgr2wlkeqi  16139  upgr2wlkdc  16147  wlkres  16149  trlreslem  16158  clwwlkccatlem  16169  clwwlkn1loopb  16188  clwwlkext2edg  16190  fnmptd  16277  bj-sels  16386  bj-nnelon  16431  2omap  16472  pw1map  16474  pwle2  16477  pwf1oexmid  16478  pw1nct  16482  nninfall  16489  nninfsellemdc  16490  nninfself  16493  nnnninfex  16502  nninfnfiinf  16503  refeq  16510  isomninnlem  16512  cvgcmp2nlemabs  16514  trilpolemlt1  16523  trirec0  16526  apdifflemf  16528  apdifflemr  16529  apdiff  16530  iswomninnlem  16531  iswomni0  16533  ismkvnnlem  16534  reap0  16540  cndcap  16541