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  713  pm4.55dc  946  mpbir2and  952  pm3.12dc  966  mpbir3and  1206  pm5.15dc  1433  eqeltrd  2308  eqnetrd  2426  3netr4d  2435  r19.30dc  2680  raleqtrrdv  2740  rexeqtrrdv  2741  sbcne12g  3145  eqsstrd  3263  3sstr4d  3272  eqbrtrd  4110  3brtr4d  4120  snelpwi  4303  prelpwi  4306  pwel  4310  ordelon  4480  onin  4483  elelsuc  4506  onsuc  4599  onsucb  4601  onintonm  4615  omsinds  4720  sosng  4799  relssdv  4818  eqbrrdv  4823  eqrelrdv2  4825  relsnopg  4830  breldmg  4937  elrnmptdv  4986  iss  5059  xpimasn  5185  elxp4  5224  elxp5  5225  iotam  5318  funssres  5369  f0rn0  5531  fimadmfo  5568  sefvex  5660  fdmeu  5689  fvun1  5712  eqfnfvd  5747  fvimacnvi  5761  fvimacnv  5762  fvelrn  5778  fmpt3d  5803  fmpt2d  5809  resflem  5811  fmptco  5813  fsn  5819  funopsn  5830  fncofn  5832  ftpg  5838  fconst2g  5869  funfvima3  5888  elabrexg  5899  foeqcnvco  5931  f1eqcocnv  5932  fliftfun  5937  fliftfund  5938  fliftval  5941  riota5f  5998  f1ofveu  6006  f1ocnvd  6225  f1opw2  6229  off  6248  offval2  6251  ofrfval2  6252  offveq  6256  caofref  6260  caofinvl  6261  elxp6  6332  cnvf1olem  6389  f2ndf  6391  f1od2  6400  elmpom  6403  tposf12  6435  smores2  6460  tfrlemisucaccv  6491  tfrlemibfn  6494  tfr1onlemsucaccv  6507  tfr1onlembfn  6510  tfrcllemsucaccv  6520  tfrcllembfn  6523  tfrcl  6530  tfri3  6533  frecabcl  6565  nnsucsssuc  6660  ersym  6714  ertr  6717  swoer  6730  erth  6748  riinerm  6777  qliftfund  6787  eroprf  6797  ecopoverg  6805  th3qlem1  6806  elmapssres  6842  mapss  6860  fdiagfn  6861  ixpssmap2g  6896  mapsnf1o  6906  f1oen4g  6925  f1dom4g  6926  f1dom2g  6929  dom3d  6947  en2prd  6992  dom1oi  7003  pw2f1odclem  7020  fopwdom  7022  mapxpen  7034  nndomo  7050  dif1en  7068  findcard2  7078  findcard2s  7079  diffisn  7082  fimax2gtrilemstep  7090  eqsndc  7095  fientri3  7107  tpfidceq  7122  fiintim  7123  opabfi  7132  f1dmvrnfibi  7143  sbthlemi6  7161  elfir  7172  fifo  7179  supelti  7201  supsnti  7204  cnvinfex  7217  ordiso2  7234  updjud  7281  djudom  7292  difinfsn  7299  ctssdc  7312  enumctlemm  7313  enumct  7314  nninfninc  7322  enomnilem  7337  fodjuf  7344  ismkvnex  7354  omnimkv  7355  enmkvlem  7360  enwomnilem  7368  nninfdcinf  7370  nninfwlporlem  7372  isnumi  7386  exmidfodomrlemrALT  7414  finacn  7419  djudoml  7434  djudomr  7435  netap  7473  2omotaplemap  7476  2omotaplemst  7477  exmidapne  7479  cc2lem  7485  cc3  7487  ltsopi  7540  pitri3or  7542  ltdcpi  7543  indpi  7562  enqdc  7581  enqdc1  7582  addcmpblnq  7587  mulcanenq  7605  recrecnq  7614  nqtri3or  7616  ltdcnq  7617  ltsonq  7618  ltaddnq  7627  subhalfnqq  7634  archnqq  7637  prarloclemarch2  7639  enq0tr  7654  nqnq0  7661  addcmpblnq0  7663  mulcanenq0ec  7665  nnnq0lem1  7666  nqpnq0nq  7673  nq0m0r  7676  nq02m  7685  prarloclemlt  7713  prarloclemcalc  7722  addlocpr  7756  nqprl  7771  nqpru  7772  addnqprlemrl  7777  addnqprlemru  7778  prmuloclemcalc  7785  mullocprlem  7790  mulnqprlemrl  7793  mulnqprlemru  7794  1idprl  7810  1idpru  7811  ltaddpr  7817  ltexprlemm  7820  ltexprlemopl  7821  ltexprlemopu  7823  ltexprlemdisj  7826  ltexprlemrl  7830  ltexprlemru  7832  addcanprleml  7834  addcanprlemu  7835  addcanprg  7836  prplnqu  7840  recexprlemloc  7851  recexprlem1ssl  7853  recexprlem1ssu  7854  aptiprleml  7859  aptiprlemu  7860  archpr  7863  cauappcvgprlemm  7865  cauappcvgprlemopl  7866  cauappcvgprlemloc  7872  cauappcvgprlemladdfu  7874  cauappcvgprlemladdfl  7875  cauappcvgprlem1  7879  cauappcvgprlem2  7880  caucvgprlemnkj  7886  caucvgprlemopl  7889  caucvgprlemloc  7895  caucvgprlemladdfu  7897  caucvgprlem2  7900  caucvgprprlemnkltj  7909  caucvgprprlemopl  7917  caucvgprprlemloc  7923  caucvgprprlemexbt  7926  caucvgprprlemaddq  7928  caucvgprprlem2  7930  suplocexprlemmu  7938  suplocexprlemru  7939  suplocexprlemloc  7941  suplocexprlemlub  7944  prsrlem1  7962  0idsr  7987  1idsr  7988  recexgt0sr  7993  archsr  8002  prsradd  8006  caucvgsrlemcau  8013  caucvgsrlembound  8014  caucvgsrlemoffgt1  8019  suplocsrlemb  8026  suplocsrlempr  8027  suplocsrlem  8028  pitonnlem1p1  8066  pitonn  8068  pitoregt0  8069  peano2nnnn  8073  recidpirq  8078  axcaucvglemval  8117  leid  8263  nltled  8300  readdcan  8319  addneintrd  8367  addneintr2d  8368  pncan  8385  subsub2  8407  subsub4  8412  negned  8487  subne0d  8499  subneintrd  8534  subneintr2d  8536  subeq0bd  8558  subdi  8564  gt0add  8753  rimul  8765  rereim  8766  ltmul1a  8771  apreim  8783  apirr  8785  mulap0r  8795  msqge0  8796  mulge0  8799  gt0ap0  8806  ltap  8813  subap0d  8824  recexaplem2  8832  mulap0bad  8839  mulap0bbd  8840  mul0eqap  8850  divrecap  8868  div0ap  8882  div1  8883  recrecap  8889  divdivdivap  8893  ddcanap  8906  rerecclap  8910  div2negap  8915  diveqap1bd  9016  recgt0  9030  prodgt0  9032  lemul1a  9038  recp1lt1  9079  squeeze0  9084  peano2nn  9155  div4p1lem1div2  9398  arch  9399  peano2z  9515  peano2zm  9517  ztri3or  9522  nn0n0n1ge2  9550  zextle  9571  gtndiv  9575  suprzclex  9578  nn0ind-raph  9597  uzid  9770  uzneg  9775  uztric  9778  uz11  9779  eluzp1l  9781  qdivcl  9877  irrmul  9881  irrmulap  9882  rpnegap  9921  negelrpd  9923  ledivge1le  9961  mul2lt0rlt0  9994  mul2lt0rgt0  9995  nn0ledivnn  10002  ltpnf  10015  mnflt  10018  pnfge  10024  mnfle  10027  xrlttr  10030  xrltso  10031  xrlttri3  10032  xrleid  10035  xaddass2  10105  xltadd1  10111  xlt2add  10115  xleaddadd  10122  iccf1o  10239  fztri3or  10274  fznlem  10276  fzn  10277  fzsplit2  10285  fznatpl1  10311  uzsplit  10327  fseq1p1m1  10329  fzm1  10335  fznn0sub2  10363  difelfznle  10370  1fv  10374  fzodcel  10388  fzospliti  10413  fzouzsplit  10416  eluzgtdifelfzo  10443  exfzdc  10487  subfzo0  10489  zsupcllemstep  10490  zsupcl  10492  zssinfcl  10493  infssuzex  10494  infssuzcldc  10496  suprzubdc  10497  nninfdcex  10498  qdcle  10507  exbtwnz  10511  qbtwnrelemcalc  10516  flqlelt  10537  qfraclt1  10541  qfracge0  10542  flqltnz  10548  btwnzge0  10561  flhalf  10563  fldiv4lem1div2uz2  10567  ceiqle  10576  intfracq  10583  mulqmod0  10593  modqge0  10595  modqlt  10596  modqid  10612  modqid0  10613  m1modge3gt1  10634  modqltm1p1mod  10639  q2txmodxeq0  10647  modaddmodlo  10651  modsumfzodifsn  10659  addmodlteq  10661  frecuzrdgtcl  10675  frecuzrdgtclt  10684  uzennn  10699  uzsinds  10707  seqf  10727  seqf2  10731  monoord2  10749  iseqf1olemqk  10770  iseqf1olemjpcl  10771  iseqf1olemqpcl  10772  seq3f1olemqsumkj  10774  seq3f1olemqsum  10776  seq3f1olemstep  10777  seq3f1oleml  10779  seqf1oglem1  10782  ser3le  10800  exp3vallem  10803  exp3val  10804  expp1  10809  expcllem  10813  ltexp2a  10854  leexp2a  10855  nn0ltexp2  10972  faclbnd  11004  faclbnd2  11005  faclbnd3  11006  bcval5  11026  bcpasc  11029  hashennn  11043  fihasheqf1oi  11050  hashsng  11061  fihashfn  11064  hashun  11069  fihashss  11081  fihashssdif  11083  hashfz  11086  hashxp  11091  fimaxq  11092  zfz1isolem1  11105  seq3coll  11107  hashdmprop2dom  11109  wrdf  11123  wrdlenge2n0  11153  fstwrdne0  11157  wrdred1hash  11161  ccatvalfn  11182  ccatsymb  11183  ccatlid  11187  ccatrid  11188  ccatrn  11190  ccatalpha  11194  eqs1  11209  ccats1val2  11221  fzowrddc  11232  swrdlen  11237  swrdnd  11244  swrd0g  11245  swrdfv2  11248  swrdwrdsymbg  11249  pfxn0  11273  pfxwrdsymbg  11275  pfxsuff1eqwrdeq  11284  swrdswrd  11290  ccats1pfxeq  11299  ccats1pfxeqrex  11300  wrdind  11307  wrd2ind  11308  swrdccatin1  11310  pfxccatin12lem4  11311  swrdccatin2  11314  pfxccatin12  11318  pfxccat3a  11323  swrdccat3blem  11324  pfxccatid  11326  swrdccatin2d  11329  shftfn  11402  cjth  11424  cjmulrcl  11465  reim0bd  11522  rerebd  11523  cjrebd  11524  caucvgre  11559  cvg1nlemcxze  11560  cvg1nlemcau  11562  cvg1nlemres  11563  recvguniq  11573  resqrexlemover  11588  resqrexlemdec  11589  resqrexlemgt0  11598  resqrexlemoverl  11599  resqrexlemglsq  11600  rersqrtthlem  11608  sqrtgt0  11612  leabs  11652  absexpzap  11658  absle  11667  recvalap  11675  abstri  11682  abs2dif  11684  amgm2  11696  absne0d  11765  maxleim  11783  maxabslemab  11784  maxabslemlub  11785  maxltsup  11796  zmaxcl  11802  fimaxre2  11805  minmax  11808  rpmincl  11816  bdtrilem  11817  bdtri  11818  xrmaxleim  11822  xrmaxiflemcom  11827  xrmaxltsup  11836  xrmaxadd  11839  xrminmax  11843  xrminrpcl  11852  climconst  11868  climuni  11871  2clim  11879  climcn1  11886  climcn2  11887  reccn2ap  11891  climge0  11903  climle  11912  climsqz  11913  climsqz2  11914  serf0  11930  summodclem3  11959  summodclem2a  11960  fsumcl2lem  11977  sumpr  11992  sumtp  11993  fsum0diaglem  12019  mptfzshft  12021  fsumle  12042  fsumlt  12043  divcnv  12076  trireciplem  12079  expcnvap0  12081  expcnv  12083  explecnv  12084  geosergap  12085  cvgratnnlembern  12102  cvgratnnlemabsle  12106  cvgratnnlemsumlt  12107  cvgratz  12111  cvgratgt0  12112  mertenslemi1  12114  mertenslem2  12115  mertensabs  12116  clim2divap  12119  prodmodclem3  12154  prodmodclem2a  12155  fprodseq  12162  fprodmul  12170  fprodfac  12194  fprodconst  12199  fprodap0  12200  fprodap0f  12215  fprodle  12219  eftcl  12233  ef0lem  12239  efsub  12260  eftlub  12269  eflegeo  12280  tanval2ap  12292  sinadd  12315  cos2t  12329  cos2tsin  12330  sin01bnd  12336  cos01bnd  12337  eirraplem  12356  dvdsval2  12369  dvdsdc  12377  dvds0lem  12380  zdvdsdc  12391  dvdscmulr  12399  dvdsmulcr  12400  fsumdvds  12421  dvdslelemd  12422  divconjdvds  12428  dvdsext  12434  fzm1ndvds  12435  dvdsmod  12441  3dvds  12443  oexpneg  12456  2tp1odd  12463  mulsucdiv2z  12464  2teven  12466  zeo5  12467  opeo  12476  omeo  12477  nn0ob  12487  divalglemnqt  12499  bitsdc  12526  bits0o  12529  bitsfzolem  12533  bitsfzo  12534  bitsmod  12535  bitscmp  12537  bitsinv1lem  12540  gcddvds  12552  dvdslegcd  12553  gcdneg  12571  bezoutlemnewy  12585  bezoutlemstep  12586  bezoutlema  12588  bezoutlemb  12589  bezoutlemmo  12595  bezoutlemle  12597  bezoutlemsup  12598  dfgcd3  12599  bezout  12600  dfgcd2  12603  uzwodc  12626  lcmcllem  12657  lcmneg  12664  lcmgcdlem  12667  lcmdvds  12669  lcmid  12670  3lcm2e6woprm  12676  6lcm4e12  12677  ncoprmgcdne1b  12679  mulgcddvds  12684  divgcdcoprmex  12692  cncongr1  12693  cncongr2  12694  isprm2lem  12706  prmind2  12710  dvdsnprmd  12715  prm2orodd  12716  sqnprm  12726  isprm5lem  12731  rpexp  12743  sqrt2irrlem  12751  oddpwdclemdc  12763  sqrt2irraplemnn  12769  qnumdencoprm  12783  qeqnumdivden  12784  nn0gcdsq  12790  nn0sqrtelqelz  12796  nonsq  12797  phicl2  12804  phibnd  12807  hashdvds  12811  phiprmpw  12812  phimullem  12815  eulerthlemrprm  12819  eulerthlema  12820  eulerthlemth  12822  prmdiveq  12826  hashgcdlem  12828  odzdvds  12836  modprminv  12840  nnnn0modprm0  12846  modprmn0modprm0  12847  pythagtriplem10  12860  pythagtriplem19  12873  pythagtrip  12874  pcpre1  12883  pcpremul  12884  pceu  12886  pcmul  12892  pcdiv  12893  pcqmul  12894  pcqdiv  12898  pcexp  12900  pcdvdsb  12911  pcidlem  12914  pcdvdstr  12918  pcgcd1  12919  pc2dvds  12921  pcprmpw2  12924  difsqpwdvds  12929  pcaddlem  12930  pcadd  12931  pcadd2  12932  pcmpt  12934  pcmptdvds  12936  pcprod  12937  fldivp1  12939  pcfaclem  12940  pcfac  12941  pcbc  12942  qexpz  12943  pockthlem  12947  pockthg  12948  1arithlem4  12957  1arith  12958  1arith2  12959  4sqlem6  12974  4sqlem8  12976  4sqlem9  12977  4sqlem10  12978  4sqexercise1  12989  4sqexercise2  12990  4sqlemsdc  12991  4sqlem11  12992  4sqlem12  12993  4sqlem15  12996  4sqlem16  12997  4sqlem17  12998  znnen  13037  ennnfonelemk  13039  ennnfonelemkh  13051  ennnfonelemhf1o  13052  ennnfonelemrnh  13055  ennnfonelemfun  13056  ennnfonelemf1  13057  ennnfonelemrn  13058  ennnfonelemnn0  13061  ctinfomlemom  13066  ctiunctlemudc  13076  unct  13081  omctfn  13082  ssnnctlemct  13085  nninfdclemp1  13089  nninfdc  13092  structfung  13117  setsfun  13135  setsfun0  13136  setscom  13140  strslfv3  13146  setsslid  13151  pwsdiagel  13398  pwssnf1o  13399  imasaddfnlemg  13415  imasaddvallemg  13416  mgmsscl  13462  plusffng  13466  mgmplusf  13467  mgm0  13470  mgm1  13471  opifismgmdc  13472  gsumfzval  13492  gsumprval  13500  sgrp1  13512  issgrpd  13513  prdsplusgsgrpcl  13515  mndpfo  13539  mndfo  13540  prdsplusgcl  13547  prdsidlem  13548  mnd1  13556  0subm  13585  mhmima  13592  grpinvfng  13645  isgrpinv  13655  grpinvid  13661  grpinvf1o  13671  grpinvadd  13679  grpsubf  13680  grpsubsub4  13694  grplactcnv  13703  grp1  13707  grp1inv  13708  prdsinvlem  13709  prdsinvgd  13711  qusgrp2  13718  mulgfng  13729  subginv  13786  resgrpisgrp  13800  subgintm  13803  0subg  13804  0nsg  13819  qusinv  13841  ghminv  13855  ghmrn  13862  ghmeql  13872  ghmnsgima  13873  kerf1ghm  13879  conjnmz  13884  rngass  13971  rngmneg1  13979  rngmneg2  13980  qusrng  13990  srgideu  14004  srgidmlem  14010  srgpcomp  14022  srg1expzeq1  14027  ringcl  14045  ringideu  14049  ringidmlem  14054  ringnegl  14083  ringnegr  14084  ring1  14091  qusring2  14098  opprringbg  14112  dvdsrd  14127  dvdsr01  14137  isunitd  14139  unitinvcl  14156  unitinvinv  14157  unitnegcl  14163  rhmmul  14197  rhmf1o  14201  nzrunit  14221  lringuplu  14229  subrngintm  14245  subrgsubm  14267  subrgintm  14276  aprsym  14317  scaffng  14342  lmodscaf  14343  lsssn0  14403  lss1d  14416  lssintclm  14417  lspval  14423  lspcl  14424  lspsnid  14440  lspprid1  14444  lspsn  14449  sraval  14470  rspcl  14524  rspssid  14525  rspssp  14527  rnglidlmmgm  14529  rnglidlmsgrp  14530  cnfldneg  14606  zringinvg  14637  expghmap  14640  znzrhfo  14681  znf1o  14684  znhash  14689  znidomb  14691  znrrg  14693  psrbagfi  14706  psraddcl  14713  psr0cl  14714  psrnegcl  14716  psrneg  14720  psr1clfi  14721  mplsubgfilemm  14731  mplsubgfilemcl  14732  baspartn  14793  eltg3i  14799  tgclb  14808  topbas  14810  2basgeng  14825  topcld  14852  0cld  14855  uncld  14856  neif  14884  elnei  14895  0nei  14909  restbasg  14911  iscnp4  14961  cnpnei  14962  cnclima  14966  cncnp  14973  cnrest2r  14980  cndis  14984  lmff  14992  lmtopcnp  14993  txbas  15001  txopn  15008  txcnp  15014  upxp  15015  txdis1cn  15021  cnmpt11  15026  cnmpt21  15034  psmetge0  15074  xmetge0  15108  xmettpos  15113  xmetrtri  15119  metrtri  15120  xblpnfps  15141  xblpnf  15142  blfps  15152  blf  15153  ssblps  15168  ssbl  15169  blbas  15176  metss2  15241  xmettxlem  15252  xmettx  15253  qtopbas  15265  divcnap  15308  cncfss  15326  cdivcncfap  15347  expcncf  15352  cnopnap  15354  maxcncf  15358  mincncf  15359  dedekindeulemuub  15360  dedekindeulemlu  15364  dedekindeu  15366  suplociccex  15368  dedekindicclemuub  15369  dedekindicclemlu  15373  dedekindicclemicc  15375  ivthinclemlopn  15379  ivthinclemuopn  15381  ivthinc  15386  ivthreinc  15388  hoverlt1  15392  ellimc3apf  15403  limcimolemlt  15407  limcimo  15408  limcresi  15409  cnplimclemle  15411  reldvg  15422  dvfgg  15431  dvidlemap  15434  dvidrelem  15435  dvidsslem  15436  dvcjbr  15451  dvcj  15452  dvrecap  15456  dveflem  15469  dvef  15470  elply2  15478  elplyr  15483  plycj  15504  plyreres  15507  reeff1oleme  15515  pilem3  15526  sinq34lt0t  15574  cosq14gt0  15575  coseq0q4123  15577  tangtx  15581  sincosq1eq  15582  cosordlem  15592  logdivlti  15624  relogbval  15694  relogbzcl  15695  nnlogbexp  15702  logbgcd1irr  15710  logbgcd1irraplemexp  15711  logbgcd1irraplemap  15712  wilthlem1  15723  mpodvdsmulf1o  15733  mersenne  15740  perfectlem2  15743  perfect  15744  zabsle1  15747  lgslem1  15748  lgsval  15752  lgsfvalg  15753  lgsfcl2  15754  lgsval2lem  15758  lgscl1  15771  lgsmod  15774  lgsdir2lem5  15780  lgsdir2  15781  lgsdilem2  15784  lgsdi  15785  lgsne0  15786  gausslemma2dlem0c  15799  gausslemma2dlem0h  15804  gausslemma2dlem1a  15806  gausslemma2dlem1f1o  15808  gausslemma2dlem3  15811  lgseisenlem1  15818  lgseisenlem2  15819  lgseisenlem3  15820  lgseisenlem4  15821  lgseisen  15822  lgsquadlem1  15825  lgsquadlem2  15826  lgsquadlem3  15827  lgsquad3  15832  2lgslem3b1  15846  2lgslem3c1  15847  2lgs  15852  2lgsoddprmlem2  15854  2lgsoddprm  15861  2sqlem3  15865  2sqlem8  15871  2sqlem10  15873  structgrssvtx  15912  structgrssiedg  15913  ushgruhgr  15950  uhgrun  15956  incistruhgr  15960  upgrop  15974  upgruhgr  15981  umgrupgr  15982  umgrnloopv  15984  umgredgprv  15985  umgr0e  15988  upgr1edc  15991  umgr1een  15995  upgrun  15996  umgrun  15998  umgrislfupgrdom  16001  upgredg  16014  umgrpredgv  16017  usgrop  16036  usgrausgrien  16039  ausgrumgrien  16040  ausgrusgrien  16041  uspgrupgrushgr  16052  usgrumgr  16054  usgrumgruspgr  16055  usgruspgrben  16056  usgrislfuspgrdom  16060  edgssv2en  16069  usgrf1oedg  16075  usgredg4  16085  usgredg2vlem2  16093  usgredg2v  16094  ushgredgedg  16096  ushgredgedgloop  16098  usgrstrrepeen  16101  usgr0e  16102  uhgr0v0e  16104  uspgr1edc  16110  usgr1e  16111  griedg0ssusgr  16121  subgrprop3  16132  subgruhgredgdm  16140  subuhgr  16142  subupgr  16143  subumgr  16144  subusgr  16145  uhgrspansubgrlem  16146  1loopgrvd2fi  16175  1loopgrvd0fi  16176  1hevtxdg0fi  16177  vdegp1aid  16184  vdegp1bid  16185  wlkm  16209  wlkvtxiedg  16215  wlkvtxiedgg  16216  wlkeq  16224  wlk1walkdom  16229  uspgr2wlkeq  16235  uspgr2wlkeqi  16237  upgr2wlkdc  16247  wlkres  16249  trlreslem  16259  clwwlkccatlem  16270  clwwlkn1loopb  16290  clwwlkext2edg  16292  clwwlknonex2lem1  16307  clwwlknonex2  16309  trlsegvdeglem2  16331  trlsegvdeglem3  16332  eupth2lem3lem4fi  16343  eupth2lemsfi  16348  fnmptd  16451  bj-sels  16560  bj-nnelon  16605  2omap  16645  pw1map  16647  pwle2  16650  pwf1oexmid  16651  pw1nct  16655  nninfall  16662  nninfsellemdc  16663  nninfself  16666  nnnninfex  16675  nninfnfiinf  16676  refeq  16683  isomninnlem  16685  cvgcmp2nlemabs  16687  trilpolemlt1  16696  trirec0  16699  apdifflemf  16701  apdifflemr  16702  apdiff  16703  qdiff  16704  iswomninnlem  16705  iswomni0  16707  ismkvnnlem  16708  reap0  16714  cndcap  16715  gfsumval  16732  gsumgfsumlem  16735  gsumgfsum  16736  gfsumsn  16737  gfsump1  16738