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  3143  eqsstrd  3261  3sstr4d  3270  eqbrtrd  4108  3brtr4d  4118  snelpwi  4301  prelpwi  4304  pwel  4308  ordelon  4478  onin  4481  elelsuc  4504  onsuc  4597  onsucb  4599  onintonm  4613  omsinds  4718  sosng  4797  relssdv  4816  eqbrrdv  4821  eqrelrdv2  4823  relsnopg  4828  breldmg  4935  elrnmptdv  4984  iss  5057  xpimasn  5183  elxp4  5222  elxp5  5223  iotam  5316  funssres  5366  f0rn0  5528  fimadmfo  5565  sefvex  5656  fdmeu  5685  fvun1  5708  eqfnfvd  5743  fvimacnvi  5757  fvimacnv  5758  fvelrn  5774  fmpt3d  5799  fmpt2d  5805  resflem  5807  fmptco  5809  fsn  5815  funopsn  5825  fncofn  5827  ftpg  5833  fconst2g  5864  funfvima3  5883  elabrexg  5894  foeqcnvco  5926  f1eqcocnv  5927  fliftfun  5932  fliftfund  5933  fliftval  5936  riota5f  5993  f1ofveu  6001  f1ocnvd  6220  f1opw2  6224  off  6243  offval2  6246  ofrfval2  6247  offveq  6251  caofref  6255  caofinvl  6256  elxp6  6327  cnvf1olem  6384  f2ndf  6386  f1od2  6395  elmpom  6398  tposf12  6430  smores2  6455  tfrlemisucaccv  6486  tfrlemibfn  6489  tfr1onlemsucaccv  6502  tfr1onlembfn  6505  tfrcllemsucaccv  6515  tfrcllembfn  6518  tfrcl  6525  tfri3  6528  frecabcl  6560  nnsucsssuc  6655  ersym  6709  ertr  6712  swoer  6725  erth  6743  riinerm  6772  qliftfund  6782  eroprf  6792  ecopoverg  6800  th3qlem1  6801  elmapssres  6837  mapss  6855  fdiagfn  6856  ixpssmap2g  6891  mapsnf1o  6901  f1oen4g  6920  f1dom4g  6921  f1dom2g  6924  dom3d  6942  en2prd  6987  dom1oi  6998  pw2f1odclem  7015  fopwdom  7017  mapxpen  7029  nndomo  7045  dif1en  7061  findcard2  7071  findcard2s  7072  diffisn  7075  fimax2gtrilemstep  7083  eqsndc  7088  fientri3  7100  tpfidceq  7115  fiintim  7116  opabfi  7123  f1dmvrnfibi  7134  sbthlemi6  7152  elfir  7163  fifo  7170  supelti  7192  supsnti  7195  cnvinfex  7208  ordiso2  7225  updjud  7272  djudom  7283  difinfsn  7290  ctssdc  7303  enumctlemm  7304  enumct  7305  nninfninc  7313  enomnilem  7328  fodjuf  7335  ismkvnex  7345  omnimkv  7346  enmkvlem  7351  enwomnilem  7359  nninfdcinf  7361  nninfwlporlem  7363  isnumi  7377  exmidfodomrlemrALT  7404  finacn  7409  djudoml  7424  djudomr  7425  netap  7463  2omotaplemap  7466  2omotaplemst  7467  exmidapne  7469  cc2lem  7475  cc3  7477  ltsopi  7530  pitri3or  7532  ltdcpi  7533  indpi  7552  enqdc  7571  enqdc1  7572  addcmpblnq  7577  mulcanenq  7595  recrecnq  7604  nqtri3or  7606  ltdcnq  7607  ltsonq  7608  ltaddnq  7617  subhalfnqq  7624  archnqq  7627  prarloclemarch2  7629  enq0tr  7644  nqnq0  7651  addcmpblnq0  7653  mulcanenq0ec  7655  nnnq0lem1  7656  nqpnq0nq  7663  nq0m0r  7666  nq02m  7675  prarloclemlt  7703  prarloclemcalc  7712  addlocpr  7746  nqprl  7761  nqpru  7762  addnqprlemrl  7767  addnqprlemru  7768  prmuloclemcalc  7775  mullocprlem  7780  mulnqprlemrl  7783  mulnqprlemru  7784  1idprl  7800  1idpru  7801  ltaddpr  7807  ltexprlemm  7810  ltexprlemopl  7811  ltexprlemopu  7813  ltexprlemdisj  7816  ltexprlemrl  7820  ltexprlemru  7822  addcanprleml  7824  addcanprlemu  7825  addcanprg  7826  prplnqu  7830  recexprlemloc  7841  recexprlem1ssl  7843  recexprlem1ssu  7844  aptiprleml  7849  aptiprlemu  7850  archpr  7853  cauappcvgprlemm  7855  cauappcvgprlemopl  7856  cauappcvgprlemloc  7862  cauappcvgprlemladdfu  7864  cauappcvgprlemladdfl  7865  cauappcvgprlem1  7869  cauappcvgprlem2  7870  caucvgprlemnkj  7876  caucvgprlemopl  7879  caucvgprlemloc  7885  caucvgprlemladdfu  7887  caucvgprlem2  7890  caucvgprprlemnkltj  7899  caucvgprprlemopl  7907  caucvgprprlemloc  7913  caucvgprprlemexbt  7916  caucvgprprlemaddq  7918  caucvgprprlem2  7920  suplocexprlemmu  7928  suplocexprlemru  7929  suplocexprlemloc  7931  suplocexprlemlub  7934  prsrlem1  7952  0idsr  7977  1idsr  7978  recexgt0sr  7983  archsr  7992  prsradd  7996  caucvgsrlemcau  8003  caucvgsrlembound  8004  caucvgsrlemoffgt1  8009  suplocsrlemb  8016  suplocsrlempr  8017  suplocsrlem  8018  pitonnlem1p1  8056  pitonn  8058  pitoregt0  8059  peano2nnnn  8063  recidpirq  8068  axcaucvglemval  8107  leid  8253  nltled  8290  readdcan  8309  addneintrd  8357  addneintr2d  8358  pncan  8375  subsub2  8397  subsub4  8402  negned  8477  subne0d  8489  subneintrd  8524  subneintr2d  8526  subeq0bd  8548  subdi  8554  gt0add  8743  rimul  8755  rereim  8756  ltmul1a  8761  apreim  8773  apirr  8775  mulap0r  8785  msqge0  8786  mulge0  8789  gt0ap0  8796  ltap  8803  subap0d  8814  recexaplem2  8822  mulap0bad  8829  mulap0bbd  8830  mul0eqap  8840  divrecap  8858  div0ap  8872  div1  8873  recrecap  8879  divdivdivap  8883  ddcanap  8896  rerecclap  8900  div2negap  8905  diveqap1bd  9006  recgt0  9020  prodgt0  9022  lemul1a  9028  recp1lt1  9069  squeeze0  9074  peano2nn  9145  div4p1lem1div2  9388  arch  9389  peano2z  9505  peano2zm  9507  ztri3or  9512  nn0n0n1ge2  9540  zextle  9561  gtndiv  9565  suprzclex  9568  nn0ind-raph  9587  uzid  9760  uzneg  9765  uztric  9768  uz11  9769  eluzp1l  9771  qdivcl  9867  irrmul  9871  irrmulap  9872  rpnegap  9911  negelrpd  9913  ledivge1le  9951  mul2lt0rlt0  9984  mul2lt0rgt0  9985  nn0ledivnn  9992  ltpnf  10005  mnflt  10008  pnfge  10014  mnfle  10017  xrlttr  10020  xrltso  10021  xrlttri3  10022  xrleid  10025  xaddass2  10095  xltadd1  10101  xlt2add  10105  xleaddadd  10112  iccf1o  10229  fztri3or  10264  fznlem  10266  fzn  10267  fzsplit2  10275  fznatpl1  10301  uzsplit  10317  fseq1p1m1  10319  fzm1  10325  fznn0sub2  10353  difelfznle  10360  1fv  10364  fzodcel  10378  fzospliti  10403  fzouzsplit  10406  eluzgtdifelfzo  10432  exfzdc  10476  subfzo0  10478  zsupcllemstep  10479  zsupcl  10481  zssinfcl  10482  infssuzex  10483  infssuzcldc  10485  suprzubdc  10486  nninfdcex  10487  qdcle  10496  exbtwnz  10500  qbtwnrelemcalc  10505  flqlelt  10526  qfraclt1  10530  qfracge0  10531  flqltnz  10537  btwnzge0  10550  flhalf  10552  fldiv4lem1div2uz2  10556  ceiqle  10565  intfracq  10572  mulqmod0  10582  modqge0  10584  modqlt  10585  modqid  10601  modqid0  10602  m1modge3gt1  10623  modqltm1p1mod  10628  q2txmodxeq0  10636  modaddmodlo  10640  modsumfzodifsn  10648  addmodlteq  10650  frecuzrdgtcl  10664  frecuzrdgtclt  10673  uzennn  10688  uzsinds  10696  seqf  10716  seqf2  10720  monoord2  10738  iseqf1olemqk  10759  iseqf1olemjpcl  10760  iseqf1olemqpcl  10761  seq3f1olemqsumkj  10763  seq3f1olemqsum  10765  seq3f1olemstep  10766  seq3f1oleml  10768  seqf1oglem1  10771  ser3le  10789  exp3vallem  10792  exp3val  10793  expp1  10798  expcllem  10802  ltexp2a  10843  leexp2a  10844  nn0ltexp2  10961  faclbnd  10993  faclbnd2  10994  faclbnd3  10995  bcval5  11015  bcpasc  11018  hashennn  11032  fihasheqf1oi  11039  hashsng  11050  fihashfn  11053  hashun  11058  fihashss  11070  fihashssdif  11072  hashfz  11075  hashxp  11080  fimaxq  11081  zfz1isolem1  11094  seq3coll  11096  hashdmprop2dom  11098  wrdf  11109  wrdlenge2n0  11139  fstwrdne0  11143  wrdred1hash  11147  ccatvalfn  11168  ccatsymb  11169  ccatlid  11173  ccatrid  11174  ccatrn  11176  ccatalpha  11180  eqs1  11195  ccats1val2  11207  fzowrddc  11218  swrdlen  11223  swrdnd  11230  swrd0g  11231  swrdfv2  11234  swrdwrdsymbg  11235  pfxn0  11259  pfxwrdsymbg  11261  pfxsuff1eqwrdeq  11270  swrdswrd  11276  ccats1pfxeq  11285  ccats1pfxeqrex  11286  wrdind  11293  wrd2ind  11294  swrdccatin1  11296  pfxccatin12lem4  11297  swrdccatin2  11300  pfxccatin12  11304  pfxccat3a  11309  swrdccat3blem  11310  pfxccatid  11312  swrdccatin2d  11315  shftfn  11375  cjth  11397  cjmulrcl  11438  reim0bd  11495  rerebd  11496  cjrebd  11497  caucvgre  11532  cvg1nlemcxze  11533  cvg1nlemcau  11535  cvg1nlemres  11536  recvguniq  11546  resqrexlemover  11561  resqrexlemdec  11562  resqrexlemgt0  11571  resqrexlemoverl  11572  resqrexlemglsq  11573  rersqrtthlem  11581  sqrtgt0  11585  leabs  11625  absexpzap  11631  absle  11640  recvalap  11648  abstri  11655  abs2dif  11657  amgm2  11669  absne0d  11738  maxleim  11756  maxabslemab  11757  maxabslemlub  11758  maxltsup  11769  zmaxcl  11775  fimaxre2  11778  minmax  11781  rpmincl  11789  bdtrilem  11790  bdtri  11791  xrmaxleim  11795  xrmaxiflemcom  11800  xrmaxltsup  11809  xrmaxadd  11812  xrminmax  11816  xrminrpcl  11825  climconst  11841  climuni  11844  2clim  11852  climcn1  11859  climcn2  11860  reccn2ap  11864  climge0  11876  climle  11885  climsqz  11886  climsqz2  11887  serf0  11903  summodclem3  11931  summodclem2a  11932  fsumcl2lem  11949  sumpr  11964  sumtp  11965  fsum0diaglem  11991  mptfzshft  11993  fsumle  12014  fsumlt  12015  divcnv  12048  trireciplem  12051  expcnvap0  12053  expcnv  12055  explecnv  12056  geosergap  12057  cvgratnnlembern  12074  cvgratnnlemabsle  12078  cvgratnnlemsumlt  12079  cvgratz  12083  cvgratgt0  12084  mertenslemi1  12086  mertenslem2  12087  mertensabs  12088  clim2divap  12091  prodmodclem3  12126  prodmodclem2a  12127  fprodseq  12134  fprodmul  12142  fprodfac  12166  fprodconst  12171  fprodap0  12172  fprodap0f  12187  fprodle  12191  eftcl  12205  ef0lem  12211  efsub  12232  eftlub  12241  eflegeo  12252  tanval2ap  12264  sinadd  12287  cos2t  12301  cos2tsin  12302  sin01bnd  12308  cos01bnd  12309  eirraplem  12328  dvdsval2  12341  dvdsdc  12349  dvds0lem  12352  zdvdsdc  12363  dvdscmulr  12371  dvdsmulcr  12372  fsumdvds  12393  dvdslelemd  12394  divconjdvds  12400  dvdsext  12406  fzm1ndvds  12407  dvdsmod  12413  3dvds  12415  oexpneg  12428  2tp1odd  12435  mulsucdiv2z  12436  2teven  12438  zeo5  12439  opeo  12448  omeo  12449  nn0ob  12459  divalglemnqt  12471  bitsdc  12498  bits0o  12501  bitsfzolem  12505  bitsfzo  12506  bitsmod  12507  bitscmp  12509  bitsinv1lem  12512  gcddvds  12524  dvdslegcd  12525  gcdneg  12543  bezoutlemnewy  12557  bezoutlemstep  12558  bezoutlema  12560  bezoutlemb  12561  bezoutlemmo  12567  bezoutlemle  12569  bezoutlemsup  12570  dfgcd3  12571  bezout  12572  dfgcd2  12575  uzwodc  12598  lcmcllem  12629  lcmneg  12636  lcmgcdlem  12639  lcmdvds  12641  lcmid  12642  3lcm2e6woprm  12648  6lcm4e12  12649  ncoprmgcdne1b  12651  mulgcddvds  12656  divgcdcoprmex  12664  cncongr1  12665  cncongr2  12666  isprm2lem  12678  prmind2  12682  dvdsnprmd  12687  prm2orodd  12688  sqnprm  12698  isprm5lem  12703  rpexp  12715  sqrt2irrlem  12723  oddpwdclemdc  12735  sqrt2irraplemnn  12741  qnumdencoprm  12755  qeqnumdivden  12756  nn0gcdsq  12762  nn0sqrtelqelz  12768  nonsq  12769  phicl2  12776  phibnd  12779  hashdvds  12783  phiprmpw  12784  phimullem  12787  eulerthlemrprm  12791  eulerthlema  12792  eulerthlemth  12794  prmdiveq  12798  hashgcdlem  12800  odzdvds  12808  modprminv  12812  nnnn0modprm0  12818  modprmn0modprm0  12819  pythagtriplem10  12832  pythagtriplem19  12845  pythagtrip  12846  pcpre1  12855  pcpremul  12856  pceu  12858  pcmul  12864  pcdiv  12865  pcqmul  12866  pcqdiv  12870  pcexp  12872  pcdvdsb  12883  pcidlem  12886  pcdvdstr  12890  pcgcd1  12891  pc2dvds  12893  pcprmpw2  12896  difsqpwdvds  12901  pcaddlem  12902  pcadd  12903  pcadd2  12904  pcmpt  12906  pcmptdvds  12908  pcprod  12909  fldivp1  12911  pcfaclem  12912  pcfac  12913  pcbc  12914  qexpz  12915  pockthlem  12919  pockthg  12920  1arithlem4  12929  1arith  12930  1arith2  12931  4sqlem6  12946  4sqlem8  12948  4sqlem9  12949  4sqlem10  12950  4sqexercise1  12961  4sqexercise2  12962  4sqlemsdc  12963  4sqlem11  12964  4sqlem12  12965  4sqlem15  12968  4sqlem16  12969  4sqlem17  12970  znnen  13009  ennnfonelemk  13011  ennnfonelemkh  13023  ennnfonelemhf1o  13024  ennnfonelemrnh  13027  ennnfonelemfun  13028  ennnfonelemf1  13029  ennnfonelemrn  13030  ennnfonelemnn0  13033  ctinfomlemom  13038  ctiunctlemudc  13048  unct  13053  omctfn  13054  ssnnctlemct  13057  nninfdclemp1  13061  nninfdc  13064  structfung  13089  setsfun  13107  setsfun0  13108  setscom  13112  strslfv3  13118  setsslid  13123  pwsdiagel  13370  pwssnf1o  13371  imasaddfnlemg  13387  imasaddvallemg  13388  mgmsscl  13434  plusffng  13438  mgmplusf  13439  mgm0  13442  mgm1  13443  opifismgmdc  13444  gsumfzval  13464  gsumprval  13472  sgrp1  13484  issgrpd  13485  prdsplusgsgrpcl  13487  mndpfo  13511  mndfo  13512  prdsplusgcl  13519  prdsidlem  13520  mnd1  13528  0subm  13557  mhmima  13564  grpinvfng  13617  isgrpinv  13627  grpinvid  13633  grpinvf1o  13643  grpinvadd  13651  grpsubf  13652  grpsubsub4  13666  grplactcnv  13675  grp1  13679  grp1inv  13680  prdsinvlem  13681  prdsinvgd  13683  qusgrp2  13690  mulgfng  13701  subginv  13758  resgrpisgrp  13772  subgintm  13775  0subg  13776  0nsg  13791  qusinv  13813  ghminv  13827  ghmrn  13834  ghmeql  13844  ghmnsgima  13845  kerf1ghm  13851  conjnmz  13856  rngass  13942  rngmneg1  13950  rngmneg2  13951  qusrng  13961  srgideu  13975  srgidmlem  13981  srgpcomp  13993  srg1expzeq1  13998  ringcl  14016  ringideu  14020  ringidmlem  14025  ringnegl  14054  ringnegr  14055  ring1  14062  qusring2  14069  opprringbg  14083  dvdsrd  14098  dvdsr01  14108  isunitd  14110  unitinvcl  14127  unitinvinv  14128  unitnegcl  14134  rhmmul  14168  rhmf1o  14172  nzrunit  14192  lringuplu  14200  subrngintm  14216  subrgsubm  14238  subrgintm  14247  aprsym  14288  scaffng  14313  lmodscaf  14314  lsssn0  14374  lss1d  14387  lssintclm  14388  lspval  14394  lspcl  14395  lspsnid  14411  lspprid1  14415  lspsn  14420  sraval  14441  rspcl  14495  rspssid  14496  rspssp  14498  rnglidlmmgm  14500  rnglidlmsgrp  14501  cnfldneg  14577  zringinvg  14608  expghmap  14611  znzrhfo  14652  znf1o  14655  znhash  14660  znidomb  14662  znrrg  14664  psrbagfi  14677  psraddcl  14684  psr0cl  14685  psrnegcl  14687  psrneg  14691  psr1clfi  14692  mplsubgfilemm  14702  mplsubgfilemcl  14703  baspartn  14764  eltg3i  14770  tgclb  14779  topbas  14781  2basgeng  14796  topcld  14823  0cld  14826  uncld  14827  neif  14855  elnei  14866  0nei  14880  restbasg  14882  iscnp4  14932  cnpnei  14933  cnclima  14937  cncnp  14944  cnrest2r  14951  cndis  14955  lmff  14963  lmtopcnp  14964  txbas  14972  txopn  14979  txcnp  14985  upxp  14986  txdis1cn  14992  cnmpt11  14997  cnmpt21  15005  psmetge0  15045  xmetge0  15079  xmettpos  15084  xmetrtri  15090  metrtri  15091  xblpnfps  15112  xblpnf  15113  blfps  15123  blf  15124  ssblps  15139  ssbl  15140  blbas  15147  metss2  15212  xmettxlem  15223  xmettx  15224  qtopbas  15236  divcnap  15279  cncfss  15297  cdivcncfap  15318  expcncf  15323  cnopnap  15325  maxcncf  15329  mincncf  15330  dedekindeulemuub  15331  dedekindeulemlu  15335  dedekindeu  15337  suplociccex  15339  dedekindicclemuub  15340  dedekindicclemlu  15344  dedekindicclemicc  15346  ivthinclemlopn  15350  ivthinclemuopn  15352  ivthinc  15357  ivthreinc  15359  hoverlt1  15363  ellimc3apf  15374  limcimolemlt  15378  limcimo  15379  limcresi  15380  cnplimclemle  15382  reldvg  15393  dvfgg  15402  dvidlemap  15405  dvidrelem  15406  dvidsslem  15407  dvcjbr  15422  dvcj  15423  dvrecap  15427  dveflem  15440  dvef  15441  elply2  15449  elplyr  15454  plycj  15475  plyreres  15478  reeff1oleme  15486  pilem3  15497  sinq34lt0t  15545  cosq14gt0  15546  coseq0q4123  15548  tangtx  15552  sincosq1eq  15553  cosordlem  15563  logdivlti  15595  relogbval  15665  relogbzcl  15666  nnlogbexp  15673  logbgcd1irr  15681  logbgcd1irraplemexp  15682  logbgcd1irraplemap  15683  wilthlem1  15694  mpodvdsmulf1o  15704  mersenne  15711  perfectlem2  15714  perfect  15715  zabsle1  15718  lgslem1  15719  lgsval  15723  lgsfvalg  15724  lgsfcl2  15725  lgsval2lem  15729  lgscl1  15742  lgsmod  15745  lgsdir2lem5  15751  lgsdir2  15752  lgsdilem2  15755  lgsdi  15756  lgsne0  15757  gausslemma2dlem0c  15770  gausslemma2dlem0h  15775  gausslemma2dlem1a  15777  gausslemma2dlem1f1o  15779  gausslemma2dlem3  15782  lgseisenlem1  15789  lgseisenlem2  15790  lgseisenlem3  15791  lgseisenlem4  15792  lgseisen  15793  lgsquadlem1  15796  lgsquadlem2  15797  lgsquadlem3  15798  lgsquad3  15803  2lgslem3b1  15817  2lgslem3c1  15818  2lgs  15823  2lgsoddprmlem2  15825  2lgsoddprm  15832  2sqlem3  15836  2sqlem8  15842  2sqlem10  15844  structgrssvtx  15883  structgrssiedg  15884  ushgruhgr  15921  uhgrun  15927  incistruhgr  15931  upgrop  15945  upgruhgr  15952  umgrupgr  15953  umgrnloopv  15955  umgredgprv  15956  umgr0e  15959  upgr1edc  15962  upgrun  15965  umgrun  15967  umgrislfupgrdom  15970  upgredg  15983  umgrpredgv  15986  usgrop  16005  usgrausgrien  16008  ausgrumgrien  16009  ausgrusgrien  16010  uspgrupgrushgr  16021  usgrumgr  16023  usgrumgruspgr  16024  usgruspgrben  16025  usgrislfuspgrdom  16029  edgssv2en  16038  usgrf1oedg  16044  usgredg4  16054  usgredg2vlem2  16062  usgredg2v  16063  ushgredgedg  16065  ushgredgedgloop  16067  usgrstrrepeen  16070  usgr0e  16071  uhgr0v0e  16073  uspgr1edc  16079  usgr1e  16080  griedg0ssusgr  16090  1loopgrvd2fi  16111  1loopgrvd0fi  16112  1hevtxdg0fi  16113  wlkm  16136  wlkvtxiedg  16142  wlkvtxiedgg  16143  wlkeq  16151  wlk1walkdom  16156  uspgr2wlkeq  16162  uspgr2wlkeqi  16164  upgr2wlkdc  16172  wlkres  16174  trlreslem  16184  clwwlkccatlem  16195  clwwlkn1loopb  16215  clwwlkext2edg  16217  clwwlknonex2lem1  16232  clwwlknonex2  16234  fnmptd  16336  bj-sels  16445  bj-nnelon  16490  2omap  16530  pw1map  16532  pwle2  16535  pwf1oexmid  16536  pw1nct  16540  nninfall  16547  nninfsellemdc  16548  nninfself  16551  nnnninfex  16560  nninfnfiinf  16561  refeq  16568  isomninnlem  16570  cvgcmp2nlemabs  16572  trilpolemlt1  16581  trirec0  16584  apdifflemf  16586  apdifflemr  16587  apdiff  16588  iswomninnlem  16589  iswomni0  16591  ismkvnnlem  16592  reap0  16598  cndcap  16599