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  3143  eqsstrd  3261  3sstr4d  3270  eqbrtrd  4106  3brtr4d  4116  snelpwi  4299  prelpwi  4302  pwel  4306  ordelon  4476  onin  4479  elelsuc  4502  onsuc  4595  onsucb  4597  onintonm  4611  omsinds  4716  sosng  4795  relssdv  4814  eqbrrdv  4819  eqrelrdv2  4821  relsnopg  4826  breldmg  4933  elrnmptdv  4982  iss  5055  xpimasn  5181  elxp4  5220  elxp5  5221  iotam  5314  funssres  5364  f0rn0  5526  fimadmfo  5563  sefvex  5654  fdmeu  5683  fvun1  5706  eqfnfvd  5741  fvimacnvi  5755  fvimacnv  5756  fvelrn  5772  fmpt3d  5797  fmpt2d  5803  resflem  5805  fmptco  5807  fsn  5813  funopsn  5823  fncofn  5825  ftpg  5831  fconst2g  5862  funfvima3  5881  elabrexg  5892  foeqcnvco  5924  f1eqcocnv  5925  fliftfun  5930  fliftfund  5931  fliftval  5934  riota5f  5991  f1ofveu  5999  f1ocnvd  6218  f1opw2  6222  off  6241  offval2  6244  ofrfval2  6245  offveq  6249  caofref  6253  caofinvl  6254  elxp6  6325  cnvf1olem  6382  f2ndf  6384  f1od2  6393  elmpom  6396  tposf12  6428  smores2  6453  tfrlemisucaccv  6484  tfrlemibfn  6487  tfr1onlemsucaccv  6500  tfr1onlembfn  6503  tfrcllemsucaccv  6513  tfrcllembfn  6516  tfrcl  6523  tfri3  6526  frecabcl  6558  nnsucsssuc  6653  ersym  6707  ertr  6710  swoer  6723  erth  6741  riinerm  6770  qliftfund  6780  eroprf  6790  ecopoverg  6798  th3qlem1  6799  elmapssres  6835  mapss  6853  fdiagfn  6854  ixpssmap2g  6889  mapsnf1o  6899  f1oen4g  6918  f1dom4g  6919  f1dom2g  6922  dom3d  6940  en2prd  6985  dom1oi  6996  pw2f1odclem  7013  fopwdom  7015  mapxpen  7027  nndomo  7043  dif1en  7059  findcard2  7069  findcard2s  7070  diffisn  7073  fimax2gtrilemstep  7081  eqsndc  7086  fientri3  7098  tpfidceq  7113  fiintim  7114  opabfi  7121  f1dmvrnfibi  7132  sbthlemi6  7150  elfir  7161  fifo  7168  supelti  7190  supsnti  7193  cnvinfex  7206  ordiso2  7223  updjud  7270  djudom  7281  difinfsn  7288  ctssdc  7301  enumctlemm  7302  enumct  7303  nninfninc  7311  enomnilem  7326  fodjuf  7333  ismkvnex  7343  omnimkv  7344  enmkvlem  7349  enwomnilem  7357  nninfdcinf  7359  nninfwlporlem  7361  isnumi  7375  exmidfodomrlemrALT  7402  finacn  7407  djudoml  7422  djudomr  7423  netap  7461  2omotaplemap  7464  2omotaplemst  7465  exmidapne  7467  cc2lem  7473  cc3  7475  ltsopi  7528  pitri3or  7530  ltdcpi  7531  indpi  7550  enqdc  7569  enqdc1  7570  addcmpblnq  7575  mulcanenq  7593  recrecnq  7602  nqtri3or  7604  ltdcnq  7605  ltsonq  7606  ltaddnq  7615  subhalfnqq  7622  archnqq  7625  prarloclemarch2  7627  enq0tr  7642  nqnq0  7649  addcmpblnq0  7651  mulcanenq0ec  7653  nnnq0lem1  7654  nqpnq0nq  7661  nq0m0r  7664  nq02m  7673  prarloclemlt  7701  prarloclemcalc  7710  addlocpr  7744  nqprl  7759  nqpru  7760  addnqprlemrl  7765  addnqprlemru  7766  prmuloclemcalc  7773  mullocprlem  7778  mulnqprlemrl  7781  mulnqprlemru  7782  1idprl  7798  1idpru  7799  ltaddpr  7805  ltexprlemm  7808  ltexprlemopl  7809  ltexprlemopu  7811  ltexprlemdisj  7814  ltexprlemrl  7818  ltexprlemru  7820  addcanprleml  7822  addcanprlemu  7823  addcanprg  7824  prplnqu  7828  recexprlemloc  7839  recexprlem1ssl  7841  recexprlem1ssu  7842  aptiprleml  7847  aptiprlemu  7848  archpr  7851  cauappcvgprlemm  7853  cauappcvgprlemopl  7854  cauappcvgprlemloc  7860  cauappcvgprlemladdfu  7862  cauappcvgprlemladdfl  7863  cauappcvgprlem1  7867  cauappcvgprlem2  7868  caucvgprlemnkj  7874  caucvgprlemopl  7877  caucvgprlemloc  7883  caucvgprlemladdfu  7885  caucvgprlem2  7888  caucvgprprlemnkltj  7897  caucvgprprlemopl  7905  caucvgprprlemloc  7911  caucvgprprlemexbt  7914  caucvgprprlemaddq  7916  caucvgprprlem2  7918  suplocexprlemmu  7926  suplocexprlemru  7927  suplocexprlemloc  7929  suplocexprlemlub  7932  prsrlem1  7950  0idsr  7975  1idsr  7976  recexgt0sr  7981  archsr  7990  prsradd  7994  caucvgsrlemcau  8001  caucvgsrlembound  8002  caucvgsrlemoffgt1  8007  suplocsrlemb  8014  suplocsrlempr  8015  suplocsrlem  8016  pitonnlem1p1  8054  pitonn  8056  pitoregt0  8057  peano2nnnn  8061  recidpirq  8066  axcaucvglemval  8105  leid  8251  nltled  8288  readdcan  8307  addneintrd  8355  addneintr2d  8356  pncan  8373  subsub2  8395  subsub4  8400  negned  8475  subne0d  8487  subneintrd  8522  subneintr2d  8524  subeq0bd  8546  subdi  8552  gt0add  8741  rimul  8753  rereim  8754  ltmul1a  8759  apreim  8771  apirr  8773  mulap0r  8783  msqge0  8784  mulge0  8787  gt0ap0  8794  ltap  8801  subap0d  8812  recexaplem2  8820  mulap0bad  8827  mulap0bbd  8828  mul0eqap  8838  divrecap  8856  div0ap  8870  div1  8871  recrecap  8877  divdivdivap  8881  ddcanap  8894  rerecclap  8898  div2negap  8903  diveqap1bd  9004  recgt0  9018  prodgt0  9020  lemul1a  9026  recp1lt1  9067  squeeze0  9072  peano2nn  9143  div4p1lem1div2  9386  arch  9387  peano2z  9503  peano2zm  9505  ztri3or  9510  nn0n0n1ge2  9538  zextle  9559  gtndiv  9563  suprzclex  9566  nn0ind-raph  9585  uzid  9758  uzneg  9763  uztric  9766  uz11  9767  eluzp1l  9769  qdivcl  9865  irrmul  9869  irrmulap  9870  rpnegap  9909  negelrpd  9911  ledivge1le  9949  mul2lt0rlt0  9982  mul2lt0rgt0  9983  nn0ledivnn  9990  ltpnf  10003  mnflt  10006  pnfge  10012  mnfle  10015  xrlttr  10018  xrltso  10019  xrlttri3  10020  xrleid  10023  xaddass2  10093  xltadd1  10099  xlt2add  10103  xleaddadd  10110  iccf1o  10227  fztri3or  10262  fznlem  10264  fzn  10265  fzsplit2  10273  fznatpl1  10299  uzsplit  10315  fseq1p1m1  10317  fzm1  10323  fznn0sub2  10351  difelfznle  10358  1fv  10362  fzodcel  10376  fzospliti  10401  fzouzsplit  10404  eluzgtdifelfzo  10430  exfzdc  10474  subfzo0  10476  zsupcllemstep  10477  zsupcl  10479  zssinfcl  10480  infssuzex  10481  infssuzcldc  10483  suprzubdc  10484  nninfdcex  10485  qdcle  10494  exbtwnz  10498  qbtwnrelemcalc  10503  flqlelt  10524  qfraclt1  10528  qfracge0  10529  flqltnz  10535  btwnzge0  10548  flhalf  10550  fldiv4lem1div2uz2  10554  ceiqle  10563  intfracq  10570  mulqmod0  10580  modqge0  10582  modqlt  10583  modqid  10599  modqid0  10600  m1modge3gt1  10621  modqltm1p1mod  10626  q2txmodxeq0  10634  modaddmodlo  10638  modsumfzodifsn  10646  addmodlteq  10648  frecuzrdgtcl  10662  frecuzrdgtclt  10671  uzennn  10686  uzsinds  10694  seqf  10714  seqf2  10718  monoord2  10736  iseqf1olemqk  10757  iseqf1olemjpcl  10758  iseqf1olemqpcl  10759  seq3f1olemqsumkj  10761  seq3f1olemqsum  10763  seq3f1olemstep  10764  seq3f1oleml  10766  seqf1oglem1  10769  ser3le  10787  exp3vallem  10790  exp3val  10791  expp1  10796  expcllem  10800  ltexp2a  10841  leexp2a  10842  nn0ltexp2  10959  faclbnd  10991  faclbnd2  10992  faclbnd3  10993  bcval5  11013  bcpasc  11016  hashennn  11030  fihasheqf1oi  11037  hashsng  11048  fihashfn  11050  hashun  11055  fihashss  11067  fihashssdif  11069  hashfz  11072  hashxp  11077  fimaxq  11078  zfz1isolem1  11091  seq3coll  11093  hashdmprop2dom  11095  wrdf  11106  wrdlenge2n0  11136  fstwrdne0  11140  wrdred1hash  11144  ccatvalfn  11165  ccatsymb  11166  ccatlid  11170  ccatrid  11171  ccatrn  11173  ccatalpha  11177  eqs1  11192  ccats1val2  11204  fzowrddc  11215  swrdlen  11220  swrdnd  11227  swrd0g  11228  swrdfv2  11231  swrdwrdsymbg  11232  pfxn0  11256  pfxwrdsymbg  11258  pfxsuff1eqwrdeq  11267  swrdswrd  11273  ccats1pfxeq  11282  ccats1pfxeqrex  11283  wrdind  11290  wrd2ind  11291  swrdccatin1  11293  pfxccatin12lem4  11294  swrdccatin2  11297  pfxccatin12  11301  pfxccat3a  11306  swrdccat3blem  11307  pfxccatid  11309  swrdccatin2d  11312  shftfn  11372  cjth  11394  cjmulrcl  11435  reim0bd  11492  rerebd  11493  cjrebd  11494  caucvgre  11529  cvg1nlemcxze  11530  cvg1nlemcau  11532  cvg1nlemres  11533  recvguniq  11543  resqrexlemover  11558  resqrexlemdec  11559  resqrexlemgt0  11568  resqrexlemoverl  11569  resqrexlemglsq  11570  rersqrtthlem  11578  sqrtgt0  11582  leabs  11622  absexpzap  11628  absle  11637  recvalap  11645  abstri  11652  abs2dif  11654  amgm2  11666  absne0d  11735  maxleim  11753  maxabslemab  11754  maxabslemlub  11755  maxltsup  11766  zmaxcl  11772  fimaxre2  11775  minmax  11778  rpmincl  11786  bdtrilem  11787  bdtri  11788  xrmaxleim  11792  xrmaxiflemcom  11797  xrmaxltsup  11806  xrmaxadd  11809  xrminmax  11813  xrminrpcl  11822  climconst  11838  climuni  11841  2clim  11849  climcn1  11856  climcn2  11857  reccn2ap  11861  climge0  11873  climle  11882  climsqz  11883  climsqz2  11884  serf0  11900  summodclem3  11928  summodclem2a  11929  fsumcl2lem  11946  sumpr  11961  sumtp  11962  fsum0diaglem  11988  mptfzshft  11990  fsumle  12011  fsumlt  12012  divcnv  12045  trireciplem  12048  expcnvap0  12050  expcnv  12052  explecnv  12053  geosergap  12054  cvgratnnlembern  12071  cvgratnnlemabsle  12075  cvgratnnlemsumlt  12076  cvgratz  12080  cvgratgt0  12081  mertenslemi1  12083  mertenslem2  12084  mertensabs  12085  clim2divap  12088  prodmodclem3  12123  prodmodclem2a  12124  fprodseq  12131  fprodmul  12139  fprodfac  12163  fprodconst  12168  fprodap0  12169  fprodap0f  12184  fprodle  12188  eftcl  12202  ef0lem  12208  efsub  12229  eftlub  12238  eflegeo  12249  tanval2ap  12261  sinadd  12284  cos2t  12298  cos2tsin  12299  sin01bnd  12305  cos01bnd  12306  eirraplem  12325  dvdsval2  12338  dvdsdc  12346  dvds0lem  12349  zdvdsdc  12360  dvdscmulr  12368  dvdsmulcr  12369  fsumdvds  12390  dvdslelemd  12391  divconjdvds  12397  dvdsext  12403  fzm1ndvds  12404  dvdsmod  12410  3dvds  12412  oexpneg  12425  2tp1odd  12432  mulsucdiv2z  12433  2teven  12435  zeo5  12436  opeo  12445  omeo  12446  nn0ob  12456  divalglemnqt  12468  bitsdc  12495  bits0o  12498  bitsfzolem  12502  bitsfzo  12503  bitsmod  12504  bitscmp  12506  bitsinv1lem  12509  gcddvds  12521  dvdslegcd  12522  gcdneg  12540  bezoutlemnewy  12554  bezoutlemstep  12555  bezoutlema  12557  bezoutlemb  12558  bezoutlemmo  12564  bezoutlemle  12566  bezoutlemsup  12567  dfgcd3  12568  bezout  12569  dfgcd2  12572  uzwodc  12595  lcmcllem  12626  lcmneg  12633  lcmgcdlem  12636  lcmdvds  12638  lcmid  12639  3lcm2e6woprm  12645  6lcm4e12  12646  ncoprmgcdne1b  12648  mulgcddvds  12653  divgcdcoprmex  12661  cncongr1  12662  cncongr2  12663  isprm2lem  12675  prmind2  12679  dvdsnprmd  12684  prm2orodd  12685  sqnprm  12695  isprm5lem  12700  rpexp  12712  sqrt2irrlem  12720  oddpwdclemdc  12732  sqrt2irraplemnn  12738  qnumdencoprm  12752  qeqnumdivden  12753  nn0gcdsq  12759  nn0sqrtelqelz  12765  nonsq  12766  phicl2  12773  phibnd  12776  hashdvds  12780  phiprmpw  12781  phimullem  12784  eulerthlemrprm  12788  eulerthlema  12789  eulerthlemth  12791  prmdiveq  12795  hashgcdlem  12797  odzdvds  12805  modprminv  12809  nnnn0modprm0  12815  modprmn0modprm0  12816  pythagtriplem10  12829  pythagtriplem19  12842  pythagtrip  12843  pcpre1  12852  pcpremul  12853  pceu  12855  pcmul  12861  pcdiv  12862  pcqmul  12863  pcqdiv  12867  pcexp  12869  pcdvdsb  12880  pcidlem  12883  pcdvdstr  12887  pcgcd1  12888  pc2dvds  12890  pcprmpw2  12893  difsqpwdvds  12898  pcaddlem  12899  pcadd  12900  pcadd2  12901  pcmpt  12903  pcmptdvds  12905  pcprod  12906  fldivp1  12908  pcfaclem  12909  pcfac  12910  pcbc  12911  qexpz  12912  pockthlem  12916  pockthg  12917  1arithlem4  12926  1arith  12927  1arith2  12928  4sqlem6  12943  4sqlem8  12945  4sqlem9  12946  4sqlem10  12947  4sqexercise1  12958  4sqexercise2  12959  4sqlemsdc  12960  4sqlem11  12961  4sqlem12  12962  4sqlem15  12965  4sqlem16  12966  4sqlem17  12967  znnen  13006  ennnfonelemk  13008  ennnfonelemkh  13020  ennnfonelemhf1o  13021  ennnfonelemrnh  13024  ennnfonelemfun  13025  ennnfonelemf1  13026  ennnfonelemrn  13027  ennnfonelemnn0  13030  ctinfomlemom  13035  ctiunctlemudc  13045  unct  13050  omctfn  13051  ssnnctlemct  13054  nninfdclemp1  13058  nninfdc  13061  structfung  13086  setsfun  13104  setsfun0  13105  setscom  13109  strslfv3  13115  setsslid  13120  pwsdiagel  13367  pwssnf1o  13368  imasaddfnlemg  13384  imasaddvallemg  13385  mgmsscl  13431  plusffng  13435  mgmplusf  13436  mgm0  13439  mgm1  13440  opifismgmdc  13441  gsumfzval  13461  gsumprval  13469  sgrp1  13481  issgrpd  13482  prdsplusgsgrpcl  13484  mndpfo  13508  mndfo  13509  prdsplusgcl  13516  prdsidlem  13517  mnd1  13525  0subm  13554  mhmima  13561  grpinvfng  13614  isgrpinv  13624  grpinvid  13630  grpinvf1o  13640  grpinvadd  13648  grpsubf  13649  grpsubsub4  13663  grplactcnv  13672  grp1  13676  grp1inv  13677  prdsinvlem  13678  prdsinvgd  13680  qusgrp2  13687  mulgfng  13698  subginv  13755  resgrpisgrp  13769  subgintm  13772  0subg  13773  0nsg  13788  qusinv  13810  ghminv  13824  ghmrn  13831  ghmeql  13841  ghmnsgima  13842  kerf1ghm  13848  conjnmz  13853  rngass  13939  rngmneg1  13947  rngmneg2  13948  qusrng  13958  srgideu  13972  srgidmlem  13978  srgpcomp  13990  srg1expzeq1  13995  ringcl  14013  ringideu  14017  ringidmlem  14022  ringnegl  14051  ringnegr  14052  ring1  14059  qusring2  14066  opprringbg  14080  dvdsrd  14095  dvdsr01  14105  isunitd  14107  unitinvcl  14124  unitinvinv  14125  unitnegcl  14131  rhmmul  14165  rhmf1o  14169  nzrunit  14189  lringuplu  14197  subrngintm  14213  subrgsubm  14235  subrgintm  14244  aprsym  14285  scaffng  14310  lmodscaf  14311  lsssn0  14371  lss1d  14384  lssintclm  14385  lspval  14391  lspcl  14392  lspsnid  14408  lspprid1  14412  lspsn  14417  sraval  14438  rspcl  14492  rspssid  14493  rspssp  14495  rnglidlmmgm  14497  rnglidlmsgrp  14498  cnfldneg  14574  zringinvg  14605  expghmap  14608  znzrhfo  14649  znf1o  14652  znhash  14657  znidomb  14659  znrrg  14661  psrbagfi  14674  psraddcl  14681  psr0cl  14682  psrnegcl  14684  psrneg  14688  psr1clfi  14689  mplsubgfilemm  14699  mplsubgfilemcl  14700  baspartn  14761  eltg3i  14767  tgclb  14776  topbas  14778  2basgeng  14793  topcld  14820  0cld  14823  uncld  14824  neif  14852  elnei  14863  0nei  14877  restbasg  14879  iscnp4  14929  cnpnei  14930  cnclima  14934  cncnp  14941  cnrest2r  14948  cndis  14952  lmff  14960  lmtopcnp  14961  txbas  14969  txopn  14976  txcnp  14982  upxp  14983  txdis1cn  14989  cnmpt11  14994  cnmpt21  15002  psmetge0  15042  xmetge0  15076  xmettpos  15081  xmetrtri  15087  metrtri  15088  xblpnfps  15109  xblpnf  15110  blfps  15120  blf  15121  ssblps  15136  ssbl  15137  blbas  15144  metss2  15209  xmettxlem  15220  xmettx  15221  qtopbas  15233  divcnap  15276  cncfss  15294  cdivcncfap  15315  expcncf  15320  cnopnap  15322  maxcncf  15326  mincncf  15327  dedekindeulemuub  15328  dedekindeulemlu  15332  dedekindeu  15334  suplociccex  15336  dedekindicclemuub  15337  dedekindicclemlu  15341  dedekindicclemicc  15343  ivthinclemlopn  15347  ivthinclemuopn  15349  ivthinc  15354  ivthreinc  15356  hoverlt1  15360  ellimc3apf  15371  limcimolemlt  15375  limcimo  15376  limcresi  15377  cnplimclemle  15379  reldvg  15390  dvfgg  15399  dvidlemap  15402  dvidrelem  15403  dvidsslem  15404  dvcjbr  15419  dvcj  15420  dvrecap  15424  dveflem  15437  dvef  15438  elply2  15446  elplyr  15451  plycj  15472  plyreres  15475  reeff1oleme  15483  pilem3  15494  sinq34lt0t  15542  cosq14gt0  15543  coseq0q4123  15545  tangtx  15549  sincosq1eq  15550  cosordlem  15560  logdivlti  15592  relogbval  15662  relogbzcl  15663  nnlogbexp  15670  logbgcd1irr  15678  logbgcd1irraplemexp  15679  logbgcd1irraplemap  15680  wilthlem1  15691  mpodvdsmulf1o  15701  mersenne  15708  perfectlem2  15711  perfect  15712  zabsle1  15715  lgslem1  15716  lgsval  15720  lgsfvalg  15721  lgsfcl2  15722  lgsval2lem  15726  lgscl1  15739  lgsmod  15742  lgsdir2lem5  15748  lgsdir2  15749  lgsdilem2  15752  lgsdi  15753  lgsne0  15754  gausslemma2dlem0c  15767  gausslemma2dlem0h  15772  gausslemma2dlem1a  15774  gausslemma2dlem1f1o  15776  gausslemma2dlem3  15779  lgseisenlem1  15786  lgseisenlem2  15787  lgseisenlem3  15788  lgseisenlem4  15789  lgseisen  15790  lgsquadlem1  15793  lgsquadlem2  15794  lgsquadlem3  15795  lgsquad3  15800  2lgslem3b1  15814  2lgslem3c1  15815  2lgs  15820  2lgsoddprmlem2  15822  2lgsoddprm  15829  2sqlem3  15833  2sqlem8  15839  2sqlem10  15841  structgrssvtx  15880  structgrssiedg  15881  ushgruhgr  15917  uhgrun  15923  incistruhgr  15927  upgrop  15941  upgruhgr  15948  umgrupgr  15949  umgrnloopv  15951  umgredgprv  15952  umgr0e  15955  upgr1edc  15958  upgrun  15961  umgrun  15963  umgrislfupgrdom  15966  upgredg  15979  umgrpredgv  15982  usgrop  16001  usgrausgrien  16004  ausgrumgrien  16005  ausgrusgrien  16006  uspgrupgrushgr  16017  usgrumgr  16019  usgrumgruspgr  16020  usgruspgrben  16021  usgrislfuspgrdom  16025  edgssv2en  16034  usgrf1oedg  16040  usgredg4  16050  usgredg2vlem2  16058  usgredg2v  16059  ushgredgedg  16061  ushgredgedgloop  16063  usgrstrrepeen  16066  usgr0e  16067  uhgr0v0e  16069  uspgr1edc  16075  usgr1e  16076  griedg0ssusgr  16086  wlkm  16127  wlkvtxiedg  16133  wlkvtxiedgg  16134  wlkeq  16142  wlk1walkdom  16147  uspgr2wlkeq  16153  uspgr2wlkeqi  16155  upgr2wlkdc  16163  wlkres  16165  trlreslem  16174  clwwlkccatlem  16185  clwwlkn1loopb  16205  clwwlkext2edg  16207  clwwlknonex2lem1  16222  clwwlknonex2  16224  fnmptd  16310  bj-sels  16419  bj-nnelon  16464  2omap  16504  pw1map  16506  pwle2  16509  pwf1oexmid  16510  pw1nct  16514  nninfall  16521  nninfsellemdc  16522  nninfself  16525  nnnninfex  16534  nninfnfiinf  16535  refeq  16542  isomninnlem  16544  cvgcmp2nlemabs  16546  trilpolemlt1  16555  trirec0  16558  apdifflemf  16560  apdifflemr  16561  apdiff  16562  iswomninnlem  16563  iswomni0  16565  ismkvnnlem  16566  reap0  16572  cndcap  16573