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  714  pm4.55dc  947  mpbir2and  953  pm3.12dc  967  mpbir3and  1207  pm5.15dc  1434  eqeltrd  2308  eqnetrd  2427  3netr4d  2436  r19.30dc  2681  raleqtrrdv  2741  rexeqtrrdv  2742  sbcne12g  3146  eqsstrd  3264  3sstr4d  3273  eqbrtrd  4115  3brtr4d  4125  snelpwi  4309  prelpwi  4312  pwel  4316  ordelon  4486  onin  4489  elelsuc  4512  onsuc  4605  onsucb  4607  onintonm  4621  omsinds  4726  sosng  4805  relssdv  4824  eqbrrdv  4829  eqrelrdv2  4831  relsnopg  4836  breldmg  4943  elrnmptdv  4992  iss  5065  xpimasn  5192  elxp4  5231  elxp5  5232  iotam  5325  funssres  5376  f0rn0  5540  fimadmfo  5577  sefvex  5669  fdmeu  5698  fvun1  5721  eqfnfvd  5756  fvimacnvi  5770  fvimacnv  5771  fvelrn  5786  fmpt3d  5811  fmpt2d  5817  resflem  5819  fmptco  5821  fsn  5827  funopsn  5838  fncofn  5840  ftpg  5846  fconst2g  5877  funfvima3  5898  elabrexg  5909  foeqcnvco  5941  f1eqcocnv  5942  fliftfun  5947  fliftfund  5948  fliftval  5951  riota5f  6008  f1ofveu  6016  f1ocnvd  6235  f1opw2  6239  off  6257  offval2  6260  ofrfval2  6261  offveq  6265  caofref  6269  caofinvl  6270  elxp6  6341  cnvf1olem  6398  f2ndf  6400  f1od2  6409  elmpom  6412  fvn0elsupp  6429  suppfnss  6435  tposf12  6478  smores2  6503  tfrlemisucaccv  6534  tfrlemibfn  6537  tfr1onlemsucaccv  6550  tfr1onlembfn  6553  tfrcllemsucaccv  6563  tfrcllembfn  6566  tfrcl  6573  tfri3  6576  frecabcl  6608  nnsucsssuc  6703  ersym  6757  ertr  6760  swoer  6773  erth  6791  riinerm  6820  qliftfund  6830  eroprf  6840  ecopoverg  6848  th3qlem1  6849  elmapssres  6885  mapss  6903  fdiagfn  6904  ixpssmap2g  6939  mapsnf1o  6949  f1oen4g  6968  f1dom4g  6969  f1dom2g  6972  dom3d  6990  en2prd  7035  dom1oi  7046  pw2f1odclem  7063  fopwdom  7065  mapxpen  7077  nndomo  7093  dif1en  7111  findcard2  7121  findcard2s  7122  diffisn  7125  fimax2gtrilemstep  7133  eqsndc  7138  fientri3  7150  tpfidceq  7165  fiintim  7166  opabfi  7175  f1dmvrnfibi  7186  sbthlemi6  7204  elfir  7215  fifo  7222  supelti  7244  supsnti  7247  cnvinfex  7260  ordiso2  7277  updjud  7324  djudom  7335  difinfsn  7342  ctssdc  7355  enumctlemm  7356  enumct  7357  nninfninc  7365  enomnilem  7380  fodjuf  7387  ismkvnex  7397  omnimkv  7398  enmkvlem  7403  enwomnilem  7411  nninfdcinf  7413  nninfwlporlem  7415  isnumi  7429  exmidfodomrlemrALT  7457  finacn  7462  djudoml  7477  djudomr  7478  netap  7516  2omotaplemap  7519  2omotaplemst  7520  exmidapne  7522  cc2lem  7528  cc3  7530  ltsopi  7583  pitri3or  7585  ltdcpi  7586  indpi  7605  enqdc  7624  enqdc1  7625  addcmpblnq  7630  mulcanenq  7648  recrecnq  7657  nqtri3or  7659  ltdcnq  7660  ltsonq  7661  ltaddnq  7670  subhalfnqq  7677  archnqq  7680  prarloclemarch2  7682  enq0tr  7697  nqnq0  7704  addcmpblnq0  7706  mulcanenq0ec  7708  nnnq0lem1  7709  nqpnq0nq  7716  nq0m0r  7719  nq02m  7728  prarloclemlt  7756  prarloclemcalc  7765  addlocpr  7799  nqprl  7814  nqpru  7815  addnqprlemrl  7820  addnqprlemru  7821  prmuloclemcalc  7828  mullocprlem  7833  mulnqprlemrl  7836  mulnqprlemru  7837  1idprl  7853  1idpru  7854  ltaddpr  7860  ltexprlemm  7863  ltexprlemopl  7864  ltexprlemopu  7866  ltexprlemdisj  7869  ltexprlemrl  7873  ltexprlemru  7875  addcanprleml  7877  addcanprlemu  7878  addcanprg  7879  prplnqu  7883  recexprlemloc  7894  recexprlem1ssl  7896  recexprlem1ssu  7897  aptiprleml  7902  aptiprlemu  7903  archpr  7906  cauappcvgprlemm  7908  cauappcvgprlemopl  7909  cauappcvgprlemloc  7915  cauappcvgprlemladdfu  7917  cauappcvgprlemladdfl  7918  cauappcvgprlem1  7922  cauappcvgprlem2  7923  caucvgprlemnkj  7929  caucvgprlemopl  7932  caucvgprlemloc  7938  caucvgprlemladdfu  7940  caucvgprlem2  7943  caucvgprprlemnkltj  7952  caucvgprprlemopl  7960  caucvgprprlemloc  7966  caucvgprprlemexbt  7969  caucvgprprlemaddq  7971  caucvgprprlem2  7973  suplocexprlemmu  7981  suplocexprlemru  7982  suplocexprlemloc  7984  suplocexprlemlub  7987  prsrlem1  8005  0idsr  8030  1idsr  8031  recexgt0sr  8036  archsr  8045  prsradd  8049  caucvgsrlemcau  8056  caucvgsrlembound  8057  caucvgsrlemoffgt1  8062  suplocsrlemb  8069  suplocsrlempr  8070  suplocsrlem  8071  pitonnlem1p1  8109  pitonn  8111  pitoregt0  8112  peano2nnnn  8116  recidpirq  8121  axcaucvglemval  8160  leid  8305  nltled  8342  readdcan  8361  addneintrd  8409  addneintr2d  8410  pncan  8427  subsub2  8449  subsub4  8454  negned  8529  subne0d  8541  subneintrd  8576  subneintr2d  8578  subeq0bd  8600  subdi  8606  gt0add  8795  rimul  8807  rereim  8808  ltmul1a  8813  apreim  8825  apirr  8827  mulap0r  8837  msqge0  8838  mulge0  8841  gt0ap0  8848  ltap  8855  subap0d  8866  recexaplem2  8874  mulap0bad  8881  mulap0bbd  8882  mul0eqap  8892  divrecap  8910  div0ap  8924  div1  8925  recrecap  8931  divdivdivap  8935  ddcanap  8948  rerecclap  8952  div2negap  8957  diveqap1bd  9058  recgt0  9072  prodgt0  9074  lemul1a  9080  recp1lt1  9121  squeeze0  9126  peano2nn  9197  div4p1lem1div2  9440  arch  9441  peano2z  9559  peano2zm  9561  ztri3or  9566  nn0n0n1ge2  9594  zextle  9615  gtndiv  9619  suprzclex  9622  nn0ind-raph  9641  uzid  9814  uzneg  9819  uztric  9822  uz11  9823  eluzp1l  9825  qdivcl  9921  irrmul  9925  irrmulap  9926  rpnegap  9965  negelrpd  9967  ledivge1le  10005  mul2lt0rlt0  10038  mul2lt0rgt0  10039  nn0ledivnn  10046  ltpnf  10059  mnflt  10062  pnfge  10068  mnfle  10071  xrlttr  10074  xrltso  10075  xrlttri3  10076  xrleid  10079  xaddass2  10149  xltadd1  10155  xlt2add  10159  xleaddadd  10166  lincmble  10283  iccf1o  10284  fztri3or  10319  fznlem  10321  fzn  10322  fzsplit2  10330  fznatpl1  10356  uzsplit  10372  fseq1p1m1  10374  fzm1  10380  fznn0sub2  10408  difelfznle  10415  1fv  10419  fzodcel  10433  fzospliti  10458  fzouzsplit  10461  eluzgtdifelfzo  10488  exfzdc  10532  subfzo0  10534  zsupcllemstep  10535  zsupcl  10537  zssinfcl  10538  infssuzex  10539  infssuzcldc  10541  suprzubdc  10542  nninfdcex  10543  qdcle  10552  exbtwnz  10556  qbtwnrelemcalc  10561  flqlelt  10582  qfraclt1  10586  qfracge0  10587  flqltnz  10593  btwnzge0  10606  flhalf  10608  fldiv4lem1div2uz2  10612  ceiqle  10621  intfracq  10628  mulqmod0  10638  modqge0  10640  modqlt  10641  modqid  10657  modqid0  10658  m1modge3gt1  10679  modqltm1p1mod  10684  q2txmodxeq0  10692  modaddmodlo  10696  modsumfzodifsn  10704  addmodlteq  10706  frecuzrdgtcl  10720  frecuzrdgtclt  10729  uzennn  10744  uzsinds  10752  seqf  10772  seqf2  10776  monoord2  10794  iseqf1olemqk  10815  iseqf1olemjpcl  10816  iseqf1olemqpcl  10817  seq3f1olemqsumkj  10819  seq3f1olemqsum  10821  seq3f1olemstep  10822  seq3f1oleml  10824  seqf1oglem1  10827  ser3le  10845  exp3vallem  10848  exp3val  10849  expp1  10854  expcllem  10858  ltexp2a  10899  leexp2a  10900  nn0ltexp2  11017  faclbnd  11049  faclbnd2  11050  faclbnd3  11051  bcval5  11071  bcpasc  11074  hashennn  11088  fihasheqf1oi  11095  hashsng  11106  fihashfn  11109  hashun  11114  fihashss  11126  fihashssdif  11128  hashfz  11131  hashxp  11136  fimaxq  11137  zfz1isolem1  11150  seq3coll  11152  hashdmprop2dom  11154  wrdf  11168  wrdlenge2n0  11198  fstwrdne0  11202  wrdred1hash  11206  ccatvalfn  11227  ccatsymb  11228  ccatlid  11232  ccatrid  11233  ccatrn  11235  ccatalpha  11239  eqs1  11254  ccats1val2  11266  fzowrddc  11277  swrdlen  11282  swrdnd  11289  swrd0g  11290  swrdfv2  11293  swrdwrdsymbg  11294  pfxn0  11318  pfxwrdsymbg  11320  pfxsuff1eqwrdeq  11329  swrdswrd  11335  ccats1pfxeq  11344  ccats1pfxeqrex  11345  wrdind  11352  wrd2ind  11353  swrdccatin1  11355  pfxccatin12lem4  11356  swrdccatin2  11359  pfxccatin12  11363  pfxccat3a  11368  swrdccat3blem  11369  pfxccatid  11371  swrdccatin2d  11374  shftfn  11447  cjth  11469  cjmulrcl  11510  reim0bd  11567  rerebd  11568  cjrebd  11569  caucvgre  11604  cvg1nlemcxze  11605  cvg1nlemcau  11607  cvg1nlemres  11608  recvguniq  11618  resqrexlemover  11633  resqrexlemdec  11634  resqrexlemgt0  11643  resqrexlemoverl  11644  resqrexlemglsq  11645  rersqrtthlem  11653  sqrtgt0  11657  leabs  11697  absexpzap  11703  absle  11712  recvalap  11720  abstri  11727  abs2dif  11729  amgm2  11741  absne0d  11810  maxleim  11828  maxabslemab  11829  maxabslemlub  11830  maxltsup  11841  zmaxcl  11847  fimaxre2  11850  minmax  11853  rpmincl  11861  bdtrilem  11862  bdtri  11863  xrmaxleim  11867  xrmaxiflemcom  11872  xrmaxltsup  11881  xrmaxadd  11884  xrminmax  11888  xrminrpcl  11897  climconst  11913  climuni  11916  2clim  11924  climcn1  11931  climcn2  11932  reccn2ap  11936  climge0  11948  climle  11957  climsqz  11958  climsqz2  11959  serf0  11975  summodclem3  12004  summodclem2a  12005  fsumcl2lem  12022  sumpr  12037  sumtp  12038  fsum0diaglem  12064  mptfzshft  12066  fsumle  12087  fsumlt  12088  divcnv  12121  trireciplem  12124  expcnvap0  12126  expcnv  12128  explecnv  12129  geosergap  12130  cvgratnnlembern  12147  cvgratnnlemabsle  12151  cvgratnnlemsumlt  12152  cvgratz  12156  cvgratgt0  12157  mertenslemi1  12159  mertenslem2  12160  mertensabs  12161  clim2divap  12164  prodmodclem3  12199  prodmodclem2a  12200  fprodseq  12207  fprodmul  12215  fprodfac  12239  fprodconst  12244  fprodap0  12245  fprodap0f  12260  fprodle  12264  eftcl  12278  ef0lem  12284  efsub  12305  eftlub  12314  eflegeo  12325  tanval2ap  12337  sinadd  12360  cos2t  12374  cos2tsin  12375  sin01bnd  12381  cos01bnd  12382  eirraplem  12401  dvdsval2  12414  dvdsdc  12422  dvds0lem  12425  zdvdsdc  12436  dvdscmulr  12444  dvdsmulcr  12445  fsumdvds  12466  dvdslelemd  12467  divconjdvds  12473  dvdsext  12479  fzm1ndvds  12480  dvdsmod  12486  3dvds  12488  oexpneg  12501  2tp1odd  12508  mulsucdiv2z  12509  2teven  12511  zeo5  12512  opeo  12521  omeo  12522  nn0ob  12532  divalglemnqt  12544  bitsdc  12571  bits0o  12574  bitsfzolem  12578  bitsfzo  12579  bitsmod  12580  bitscmp  12582  bitsinv1lem  12585  gcddvds  12597  dvdslegcd  12598  gcdneg  12616  bezoutlemnewy  12630  bezoutlemstep  12631  bezoutlema  12633  bezoutlemb  12634  bezoutlemmo  12640  bezoutlemle  12642  bezoutlemsup  12643  dfgcd3  12644  bezout  12645  dfgcd2  12648  uzwodc  12671  lcmcllem  12702  lcmneg  12709  lcmgcdlem  12712  lcmdvds  12714  lcmid  12715  3lcm2e6woprm  12721  6lcm4e12  12722  ncoprmgcdne1b  12724  mulgcddvds  12729  divgcdcoprmex  12737  cncongr1  12738  cncongr2  12739  isprm2lem  12751  prmind2  12755  dvdsnprmd  12760  prm2orodd  12761  sqnprm  12771  isprm5lem  12776  rpexp  12788  sqrt2irrlem  12796  oddpwdclemdc  12808  sqrt2irraplemnn  12814  qnumdencoprm  12828  qeqnumdivden  12829  nn0gcdsq  12835  nn0sqrtelqelz  12841  nonsq  12842  phicl2  12849  phibnd  12852  hashdvds  12856  phiprmpw  12857  phimullem  12860  eulerthlemrprm  12864  eulerthlema  12865  eulerthlemth  12867  prmdiveq  12871  hashgcdlem  12873  odzdvds  12881  modprminv  12885  nnnn0modprm0  12891  modprmn0modprm0  12892  pythagtriplem10  12905  pythagtriplem19  12918  pythagtrip  12919  pcpre1  12928  pcpremul  12929  pceu  12931  pcmul  12937  pcdiv  12938  pcqmul  12939  pcqdiv  12943  pcexp  12945  pcdvdsb  12956  pcidlem  12959  pcdvdstr  12963  pcgcd1  12964  pc2dvds  12966  pcprmpw2  12969  difsqpwdvds  12974  pcaddlem  12975  pcadd  12976  pcadd2  12977  pcmpt  12979  pcmptdvds  12981  pcprod  12982  fldivp1  12984  pcfaclem  12985  pcfac  12986  pcbc  12987  qexpz  12988  pockthlem  12992  pockthg  12993  1arithlem4  13002  1arith  13003  1arith2  13004  4sqlem6  13019  4sqlem8  13021  4sqlem9  13022  4sqlem10  13023  4sqexercise1  13034  4sqexercise2  13035  4sqlemsdc  13036  4sqlem11  13037  4sqlem12  13038  4sqlem15  13041  4sqlem16  13042  4sqlem17  13043  znnen  13082  ennnfonelemk  13084  ennnfonelemkh  13096  ennnfonelemhf1o  13097  ennnfonelemrnh  13100  ennnfonelemfun  13101  ennnfonelemf1  13102  ennnfonelemrn  13103  ennnfonelemnn0  13106  ctinfomlemom  13111  ctiunctlemudc  13121  unct  13126  omctfn  13127  ssnnctlemct  13130  nninfdclemp1  13134  nninfdc  13137  structfung  13162  setsfun  13180  setsfun0  13181  setscom  13185  strslfv3  13191  setsslid  13196  pwsdiagel  13443  pwssnf1o  13444  imasaddfnlemg  13460  imasaddvallemg  13461  mgmsscl  13507  plusffng  13511  mgmplusf  13512  mgm0  13515  mgm1  13516  opifismgmdc  13517  gsumfzval  13537  gsumprval  13545  sgrp1  13557  issgrpd  13558  prdsplusgsgrpcl  13560  mndpfo  13584  mndfo  13585  prdsplusgcl  13592  prdsidlem  13593  mnd1  13601  0subm  13630  mhmima  13637  grpinvfng  13690  isgrpinv  13700  grpinvid  13706  grpinvf1o  13716  grpinvadd  13724  grpsubf  13725  grpsubsub4  13739  grplactcnv  13748  grp1  13752  grp1inv  13753  prdsinvlem  13754  prdsinvgd  13756  qusgrp2  13763  mulgfng  13774  subginv  13831  resgrpisgrp  13845  subgintm  13848  0subg  13849  0nsg  13864  qusinv  13886  ghminv  13900  ghmrn  13907  ghmeql  13917  ghmnsgima  13918  kerf1ghm  13924  conjnmz  13929  rngass  14016  rngmneg1  14024  rngmneg2  14025  qusrng  14035  srgideu  14049  srgidmlem  14055  srgpcomp  14067  srg1expzeq1  14072  ringcl  14090  ringideu  14094  ringidmlem  14099  ringnegl  14128  ringnegr  14129  ring1  14136  qusring2  14143  opprringbg  14157  dvdsrd  14172  dvdsr01  14182  isunitd  14184  unitinvcl  14201  unitinvinv  14202  unitnegcl  14208  rhmmul  14242  rhmf1o  14246  nzrunit  14266  lringuplu  14274  subrngintm  14290  subrgsubm  14312  subrgintm  14321  rrgsupp  14344  aprsym  14363  scaffng  14388  lmodscaf  14389  lsssn0  14449  lss1d  14462  lssintclm  14463  lspval  14469  lspcl  14470  lspsnid  14486  lspprid1  14490  lspsn  14495  sraval  14516  rspcl  14570  rspssid  14571  rspssp  14573  rnglidlmmgm  14575  rnglidlmsgrp  14576  cnfldneg  14652  zringinvg  14683  expghmap  14686  znzrhfo  14727  znf1o  14730  znhash  14735  znidomb  14737  znrrg  14739  psrbagfi  14753  psrbaglecl  14754  psrbagcon  14755  psraddcl  14764  psr0cl  14765  psrnegcl  14767  psrneg  14771  psr1clfi  14772  mplsubgfilemm  14782  mplsubgfilemcl  14783  baspartn  14844  eltg3i  14850  tgclb  14859  topbas  14861  2basgeng  14876  topcld  14903  0cld  14906  uncld  14907  neif  14935  elnei  14946  0nei  14960  restbasg  14962  iscnp4  15012  cnpnei  15013  cnclima  15017  cncnp  15024  cnrest2r  15031  cndis  15035  lmff  15043  lmtopcnp  15044  txbas  15052  txopn  15059  txcnp  15065  upxp  15066  txdis1cn  15072  cnmpt11  15077  cnmpt21  15085  psmetge0  15125  xmetge0  15159  xmettpos  15164  xmetrtri  15170  metrtri  15171  xblpnfps  15192  xblpnf  15193  blfps  15203  blf  15204  ssblps  15219  ssbl  15220  blbas  15227  metss2  15292  xmettxlem  15303  xmettx  15304  qtopbas  15316  divcnap  15359  cncfss  15377  cdivcncfap  15398  expcncf  15403  cnopnap  15405  maxcncf  15409  mincncf  15410  dedekindeulemuub  15411  dedekindeulemlu  15415  dedekindeu  15417  suplociccex  15419  dedekindicclemuub  15420  dedekindicclemlu  15424  dedekindicclemicc  15426  ivthinclemlopn  15430  ivthinclemuopn  15432  ivthinc  15437  ivthreinc  15439  hoverlt1  15443  ellimc3apf  15454  limcimolemlt  15458  limcimo  15459  limcresi  15460  cnplimclemle  15462  reldvg  15473  dvfgg  15482  dvidlemap  15485  dvidrelem  15486  dvidsslem  15487  dvcjbr  15502  dvcj  15503  dvrecap  15507  dveflem  15520  dvef  15521  elply2  15529  elplyr  15534  plycj  15555  plyreres  15558  reeff1oleme  15566  pilem3  15577  sinq34lt0t  15625  cosq14gt0  15626  coseq0q4123  15628  tangtx  15632  sincosq1eq  15633  cosordlem  15643  logdivlti  15675  relogbval  15745  relogbzcl  15746  nnlogbexp  15753  logbgcd1irr  15761  logbgcd1irraplemexp  15762  logbgcd1irraplemap  15763  pellexlem1  15774  pellexlem3  15776  wilthlem1  15777  mpodvdsmulf1o  15787  mersenne  15794  perfectlem2  15797  perfect  15798  zabsle1  15801  lgslem1  15802  lgsval  15806  lgsfvalg  15807  lgsfcl2  15808  lgsval2lem  15812  lgscl1  15825  lgsmod  15828  lgsdir2lem5  15834  lgsdir2  15835  lgsdilem2  15838  lgsdi  15839  lgsne0  15840  gausslemma2dlem0c  15853  gausslemma2dlem0h  15858  gausslemma2dlem1a  15860  gausslemma2dlem1f1o  15862  gausslemma2dlem3  15865  lgseisenlem1  15872  lgseisenlem2  15873  lgseisenlem3  15874  lgseisenlem4  15875  lgseisen  15876  lgsquadlem1  15879  lgsquadlem2  15880  lgsquadlem3  15881  lgsquad3  15886  2lgslem3b1  15900  2lgslem3c1  15901  2lgs  15906  2lgsoddprmlem2  15908  2lgsoddprm  15915  2sqlem3  15919  2sqlem8  15925  2sqlem10  15927  structgrssvtx  15966  structgrssiedg  15967  ushgruhgr  16004  uhgrun  16010  incistruhgr  16014  upgrop  16028  upgruhgr  16035  umgrupgr  16036  umgrnloopv  16038  umgredgprv  16039  umgr0e  16042  upgr1edc  16045  umgr1een  16049  upgrun  16050  umgrun  16052  umgrislfupgrdom  16055  upgredg  16068  umgrpredgv  16071  usgrop  16090  usgrausgrien  16093  ausgrumgrien  16094  ausgrusgrien  16095  uspgrupgrushgr  16106  usgrumgr  16108  usgrumgruspgr  16109  usgruspgrben  16110  usgrislfuspgrdom  16114  edgssv2en  16123  usgrf1oedg  16129  usgredg4  16139  usgredg2vlem2  16147  usgredg2v  16148  ushgredgedg  16150  ushgredgedgloop  16152  usgrstrrepeen  16155  usgr0e  16156  uhgr0v0e  16158  uspgr1edc  16164  usgr1e  16165  griedg0ssusgr  16175  subgrprop3  16186  subgruhgredgdm  16194  subuhgr  16196  subupgr  16197  subumgr  16198  subusgr  16199  uhgrspansubgrlem  16200  1loopgrvd2fi  16229  1loopgrvd0fi  16230  1hevtxdg0fi  16231  vdegp1aid  16238  vdegp1bid  16239  wlkm  16263  wlkvtxiedg  16269  wlkvtxiedgg  16270  wlkeq  16278  wlk1walkdom  16283  uspgr2wlkeq  16289  uspgr2wlkeqi  16291  upgr2wlkdc  16301  wlkres  16303  trlreslem  16313  clwwlkccatlem  16324  clwwlkn1loopb  16344  clwwlkext2edg  16346  clwwlknonex2lem1  16361  clwwlknonex2  16363  trlsegvdeglem2  16385  trlsegvdeglem3  16386  eupth2lem3lem4fi  16397  eupth2lemsfi  16402  fnmptd  16505  bj-sels  16613  bj-nnelon  16658  2omap  16698  pw1map  16700  pwle2  16703  pwf1oexmid  16704  pw1nct  16708  nninfall  16718  nninfsellemdc  16719  nninfself  16722  nnnninfex  16731  nninfnfiinf  16732  refeq  16739  isomninnlem  16745  cvgcmp2nlemabs  16747  trilpolemlt1  16756  trirec0  16759  apdifflemf  16761  apdifflemr  16762  apdiff  16763  qdiff  16764  iswomninnlem  16765  iswomni0  16767  ismkvnnlem  16768  reap0  16774  cndcap  16775  gfsumval  16792  gsumgfsumlem  16795  gsumgfsum  16796  gfsumsn  16797  gfsump1  16798