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  2309  eqnetrd  2436  3netr4d  2445  r19.30dc  2690  raleqtrrdv  2751  rexeqtrrdv  2752  sbcne12g  3156  eqsstrd  3274  3sstr4d  3283  eqbrtrd  4131  3brtr4d  4141  snelpwi  4327  prelpwi  4330  pwel  4334  ordelon  4504  onin  4507  elelsuc  4530  onsuc  4623  onsucb  4625  onintonm  4639  omsinds  4744  sosng  4823  relssdv  4842  eqbrrdv  4847  eqrelrdv2  4849  relsnopg  4854  breldmg  4962  elrnmptdv  5011  iss  5084  xpimasn  5211  elxp4  5250  elxp5  5251  iotam  5344  funssres  5395  f0rn0  5562  fimadmfo  5599  sefvex  5691  fdmeu  5720  fvun1  5743  eqfnfvd  5778  fvimacnvi  5792  fvimacnv  5793  fvelrn  5808  fmpt3d  5833  fmpt2d  5839  resflem  5841  fmptco  5843  fsn  5849  funopsn  5860  fncofn  5862  ftpg  5868  fconst2g  5899  funfvima3  5920  elabrexg  5931  foeqcnvco  5963  f1eqcocnv  5964  fliftfun  5969  fliftfund  5970  fliftval  5973  riota5f  6030  f1ofveu  6038  f1ocnvd  6257  f1opw2  6261  off  6279  offval2  6282  ofrfval2  6283  offveq  6287  caofref  6291  caofinvl  6292  elxp6  6363  cnvf1olem  6420  f2ndf  6422  f1od2  6431  elmpom  6434  fvn0elsupp  6451  suppfnss  6457  tposf12  6500  smores2  6525  tfrlemisucaccv  6556  tfrlemibfn  6559  tfr1onlemsucaccv  6572  tfr1onlembfn  6575  tfrcllemsucaccv  6585  tfrcllembfn  6588  tfrcl  6595  tfri3  6598  frecabcl  6630  nnsucsssuc  6725  ersym  6779  ertr  6782  swoer  6795  erth  6813  riinerm  6842  qliftfund  6852  eroprf  6862  ecopoverg  6870  th3qlem1  6871  elmapssres  6907  mapss  6926  fdiagfn  6927  ixpssmap2g  6962  mapsnf1o  6972  f1oen4g  6991  f1dom4g  6992  f1dom2g  6995  dom3d  7013  en2prd  7059  dom1oi  7070  pw2f1odclem  7087  fopwdom  7089  mapxpen  7101  nndomo  7118  dif1en  7136  findcard2  7146  findcard2s  7147  diffisn  7150  fimax2gtrilemstep  7158  eqsndc  7163  fientri3  7175  tpfidceq  7190  fiintim  7191  opabfi  7200  f1dmvrnfibi  7211  sbthlemi6  7232  0fsupp  7251  elfir  7260  fifo  7267  2omap  7269  supelti  7293  supsnti  7296  cnvinfex  7309  ordiso2  7326  updjud  7373  djudom  7384  difinfsn  7391  ctssdc  7404  enumctlemm  7405  enumct  7406  nninfninc  7414  enomnilem  7429  fodjuf  7436  ismkvnex  7446  omnimkv  7447  enmkvlem  7452  enwomnilem  7460  nninfdcinf  7462  nninfwlporlem  7464  isnumi  7478  exmidfodomrlemrALT  7506  finacn  7511  djudoml  7526  djudomr  7527  netap  7568  2omotaplemap  7571  2omotaplemst  7572  exmidapne  7574  cc2lem  7580  cc3  7582  ltsopi  7635  pitri3or  7637  ltdcpi  7638  indpi  7657  enqdc  7676  enqdc1  7677  addcmpblnq  7682  mulcanenq  7700  recrecnq  7709  nqtri3or  7711  ltdcnq  7712  ltsonq  7713  ltaddnq  7722  subhalfnqq  7729  archnqq  7732  prarloclemarch2  7734  enq0tr  7749  nqnq0  7756  addcmpblnq0  7758  mulcanenq0ec  7760  nnnq0lem1  7761  nqpnq0nq  7768  nq0m0r  7771  nq02m  7780  prarloclemlt  7808  prarloclemcalc  7817  addlocpr  7851  nqprl  7866  nqpru  7867  addnqprlemrl  7872  addnqprlemru  7873  prmuloclemcalc  7880  mullocprlem  7885  mulnqprlemrl  7888  mulnqprlemru  7889  1idprl  7905  1idpru  7906  ltaddpr  7912  ltexprlemm  7915  ltexprlemopl  7916  ltexprlemopu  7918  ltexprlemdisj  7921  ltexprlemrl  7925  ltexprlemru  7927  addcanprleml  7929  addcanprlemu  7930  addcanprg  7931  prplnqu  7935  recexprlemloc  7946  recexprlem1ssl  7948  recexprlem1ssu  7949  aptiprleml  7954  aptiprlemu  7955  archpr  7958  cauappcvgprlemm  7960  cauappcvgprlemopl  7961  cauappcvgprlemloc  7967  cauappcvgprlemladdfu  7969  cauappcvgprlemladdfl  7970  cauappcvgprlem1  7974  cauappcvgprlem2  7975  caucvgprlemnkj  7981  caucvgprlemopl  7984  caucvgprlemloc  7990  caucvgprlemladdfu  7992  caucvgprlem2  7995  caucvgprprlemnkltj  8004  caucvgprprlemopl  8012  caucvgprprlemloc  8018  caucvgprprlemexbt  8021  caucvgprprlemaddq  8023  caucvgprprlem2  8025  suplocexprlemmu  8033  suplocexprlemru  8034  suplocexprlemloc  8036  suplocexprlemlub  8039  prsrlem1  8057  0idsr  8082  1idsr  8083  recexgt0sr  8088  archsr  8097  prsradd  8101  caucvgsrlemcau  8108  caucvgsrlembound  8109  caucvgsrlemoffgt1  8114  suplocsrlemb  8121  suplocsrlempr  8122  suplocsrlem  8123  pitonnlem1p1  8161  pitonn  8163  pitoregt0  8164  peano2nnnn  8168  recidpirq  8173  axcaucvglemval  8212  leid  8357  nltled  8394  readdcan  8413  addneintrd  8461  addneintr2d  8462  pncan  8479  subsub2  8501  subsub4  8506  negned  8581  subne0d  8593  subneintrd  8628  subneintr2d  8630  subeq0bd  8652  subdi  8658  gt0add  8847  rimul  8859  rereim  8860  ltmul1a  8865  apreim  8877  apirr  8879  mulap0r  8889  msqge0  8890  mulge0  8893  gt0ap0  8900  ltap  8907  subap0d  8918  recexaplem2  8926  mulap0bad  8933  mulap0bbd  8934  mul0eqap  8944  divrecap  8962  div0ap  8976  div1  8977  recrecap  8983  divdivdivap  8987  ddcanap  9000  rerecclap  9004  div2negap  9009  diveqap1bd  9110  recgt0  9124  prodgt0  9126  lemul1a  9132  recp1lt1  9173  squeeze0  9178  peano2nn  9249  div4p1lem1div2  9492  arch  9493  peano2z  9613  peano2zm  9615  ztri3or  9620  nn0n0n1ge2  9648  zextle  9669  gtndiv  9673  suprzclex  9676  nn0ind-raph  9695  uzid  9868  uzneg  9873  uztric  9876  uz11  9877  eluzp1l  9879  qdivcl  9975  irrmul  9979  irrmulap  9980  rpnegap  10019  negelrpd  10021  ledivge1le  10059  mul2lt0rlt0  10092  mul2lt0rgt0  10093  nn0ledivnn  10100  ltpnf  10113  mnflt  10116  pnfge  10122  mnfle  10125  xrlttr  10128  xrltso  10129  xrlttri3  10130  xrleid  10133  xaddass2  10203  xltadd1  10209  xlt2add  10213  xleaddadd  10220  lincmble  10337  iccf1o  10338  fztri3or  10373  fznlem  10375  fzn  10376  fzsplit2  10384  fznatpl1  10410  uzsplit  10426  fseq1p1m1  10428  fzm1  10434  fznn0sub2  10462  difelfznle  10469  1fv  10473  fzodcel  10487  fzospliti  10512  fzouzsplit  10515  eluzgtdifelfzo  10542  exfzdc  10586  subfzo0  10588  zsupcllemstep  10589  zsupcl  10591  zssinfcl  10592  infssuzex  10593  infssuzcldc  10595  suprzubdc  10596  nninfdcex  10597  qdcle  10606  exbtwnz  10610  qbtwnrelemcalc  10615  flqlelt  10636  qfraclt1  10640  qfracge0  10641  flqltnz  10647  btwnzge0  10660  flhalf  10662  fldiv4lem1div2uz2  10666  ceiqle  10675  intfracq  10682  mulqmod0  10692  modqge0  10694  modqlt  10695  modqid  10711  modqid0  10712  m1modge3gt1  10733  modqltm1p1mod  10738  q2txmodxeq0  10746  modaddmodlo  10750  modsumfzodifsn  10758  addmodlteq  10760  frecuzrdgtcl  10774  frecuzrdgtclt  10783  uzennn  10798  uzsinds  10806  seqf  10826  seqf2  10830  monoord2  10848  iseqf1olemqk  10869  iseqf1olemjpcl  10870  iseqf1olemqpcl  10871  seq3f1olemqsumkj  10873  seq3f1olemqsum  10875  seq3f1olemstep  10876  seq3f1oleml  10878  seqf1oglem1  10881  ser3le  10899  exp3vallem  10902  exp3val  10903  expp1  10908  expcllem  10912  ltexp2a  10953  leexp2a  10954  nn0ltexp2  11071  faclbnd  11103  faclbnd2  11104  faclbnd3  11105  bcval5  11125  bcpasc  11128  bcm1n  11131  hashennn  11143  fihasheqf1oi  11150  hashsng  11161  fihashfn  11164  hashun  11169  fihashss  11181  fihashssdif  11183  hashfz  11186  hashxp  11191  hashmap  11192  hashpwfi  11193  fimaxq  11194  sseqn  11203  hashfibclem  11206  zfz1isolem1  11212  seq3coll  11214  hashdmprop2dom  11216  wrdf  11230  wrdlenge2n0  11260  fstwrdne0  11264  wrdred1hash  11268  ccatvalfn  11289  ccatsymb  11290  ccatlid  11294  ccatrid  11295  ccatrn  11297  ccatalpha  11301  eqs1  11316  ccats1val2  11328  fzowrddc  11339  swrdlen  11344  swrdnd  11351  swrd0g  11352  swrdfv2  11355  swrdwrdsymbg  11356  pfxn0  11380  pfxwrdsymbg  11382  pfxsuff1eqwrdeq  11391  swrdswrd  11397  ccats1pfxeq  11406  ccats1pfxeqrex  11407  wrdind  11414  wrd2ind  11415  swrdccatin1  11417  pfxccatin12lem4  11418  swrdccatin2  11421  pfxccatin12  11425  pfxccat3a  11430  swrdccat3blem  11431  pfxccatid  11433  swrdccatin2d  11436  shftfn  11509  cjth  11531  cjmulrcl  11572  reim0bd  11629  rerebd  11630  cjrebd  11631  caucvgre  11666  cvg1nlemcxze  11667  cvg1nlemcau  11669  cvg1nlemres  11670  recvguniq  11680  resqrexlemover  11695  resqrexlemdec  11696  resqrexlemgt0  11705  resqrexlemoverl  11706  resqrexlemglsq  11707  rersqrtthlem  11715  sqrtgt0  11719  leabs  11759  absexpzap  11765  absle  11774  recvalap  11782  abstri  11789  abs2dif  11791  amgm2  11803  absne0d  11872  maxleim  11890  maxabslemab  11891  maxabslemlub  11892  maxltsup  11903  zmaxcl  11909  fimaxre2  11912  minmax  11915  rpmincl  11923  bdtrilem  11924  bdtri  11925  xrmaxleim  11929  xrmaxiflemcom  11934  xrmaxltsup  11943  xrmaxadd  11946  xrminmax  11950  xrminrpcl  11959  climconst  11975  climuni  11978  2clim  11986  climcn1  11993  climcn2  11994  reccn2ap  11998  climge0  12010  climle  12019  climsqz  12020  climsqz2  12021  serf0  12037  summodclem3  12066  summodclem2a  12067  fsumcl2lem  12084  sumpr  12099  sumtp  12100  fsum0diaglem  12126  mptfzshft  12128  fsumle  12149  fsumlt  12150  divcnv  12183  trireciplem  12186  expcnvap0  12188  expcnv  12190  explecnv  12191  geosergap  12192  cvgratnnlembern  12209  cvgratnnlemabsle  12213  cvgratnnlemsumlt  12214  cvgratz  12218  cvgratgt0  12219  mertenslemi1  12221  mertenslem2  12222  mertensabs  12223  clim2divap  12226  prodmodclem3  12261  prodmodclem2a  12262  fprodseq  12269  fprodmul  12277  fprodfac  12301  fprodconst  12306  fprodap0  12307  fprodap0f  12322  fprodle  12326  eftcl  12340  ef0lem  12346  efsub  12367  eftlub  12376  eflegeo  12387  tanval2ap  12399  sinadd  12422  cos2t  12436  cos2tsin  12437  sin01bnd  12443  cos01bnd  12444  eirraplem  12463  dvdsval2  12476  dvdsdc  12484  dvds0lem  12487  zdvdsdc  12498  dvdscmulr  12506  dvdsmulcr  12507  fsumdvds  12528  dvdslelemd  12529  divconjdvds  12535  dvdsext  12541  fzm1ndvds  12542  dvdsmod  12548  3dvds  12550  oexpneg  12563  2tp1odd  12570  mulsucdiv2z  12571  2teven  12573  zeo5  12574  opeo  12583  omeo  12584  nn0ob  12594  divalglemnqt  12606  bitsdc  12633  bits0o  12636  bitsfzolem  12640  bitsfzo  12641  bitsmod  12642  bitscmp  12644  bitsinv1lem  12647  gcddvds  12659  dvdslegcd  12660  gcdneg  12678  bezoutlemnewy  12692  bezoutlemstep  12693  bezoutlema  12695  bezoutlemb  12696  bezoutlemmo  12702  bezoutlemle  12704  bezoutlemsup  12705  dfgcd3  12706  bezout  12707  dfgcd2  12710  uzwodc  12733  lcmcllem  12764  lcmneg  12771  lcmgcdlem  12774  lcmdvds  12776  lcmid  12777  3lcm2e6woprm  12783  6lcm4e12  12784  ncoprmgcdne1b  12786  mulgcddvds  12791  divgcdcoprmex  12799  cncongr1  12800  cncongr2  12801  isprm2lem  12813  prmind2  12817  dvdsnprmd  12822  prm2orodd  12823  sqnprm  12833  isprm5lem  12838  rpexp  12850  sqrt2irrlem  12858  oddpwdclemdc  12870  sqrt2irraplemnn  12876  qnumdencoprm  12890  qeqnumdivden  12891  nn0gcdsq  12897  nn0sqrtelqelz  12903  nonsq  12904  phicl2  12911  phibnd  12914  hashdvds  12918  phiprmpw  12919  phimullem  12922  eulerthlemrprm  12926  eulerthlema  12927  eulerthlemth  12929  prmdiveq  12933  hashgcdlem  12935  odzdvds  12943  modprminv  12947  nnnn0modprm0  12953  modprmn0modprm0  12954  pythagtriplem10  12967  pythagtriplem19  12980  pythagtrip  12981  pcpre1  12990  pcpremul  12991  pceu  12993  pcmul  12999  pcdiv  13000  pcqmul  13001  pcqdiv  13005  pcexp  13007  pcdvdsb  13018  pcidlem  13021  pcdvdstr  13025  pcgcd1  13026  pc2dvds  13028  pcprmpw2  13031  difsqpwdvds  13036  pcaddlem  13037  pcadd  13038  pcadd2  13039  pcmpt  13041  pcmptdvds  13043  pcprod  13044  fldivp1  13046  pcfaclem  13047  pcfac  13048  pcbc  13049  qexpz  13050  pockthlem  13054  pockthg  13055  1arithlem4  13064  1arith  13065  1arith2  13066  4sqlem6  13081  4sqlem8  13083  4sqlem9  13084  4sqlem10  13085  4sqexercise1  13096  4sqexercise2  13097  4sqlemsdc  13098  4sqlem11  13099  4sqlem12  13100  4sqlem15  13103  4sqlem16  13104  4sqlem17  13105  znnen  13149  ennnfonelemk  13151  ennnfonelemkh  13163  ennnfonelemhf1o  13164  ennnfonelemrnh  13167  ennnfonelemfun  13168  ennnfonelemf1  13169  ennnfonelemrn  13170  ennnfonelemnn0  13173  ctinfomlemom  13178  ctiunctlemudc  13188  unct  13193  omctfn  13194  ssnnctlemct  13197  nninfdclemp1  13201  nninfdc  13204  structfung  13229  setsfun  13247  setsfun0  13248  setscom  13252  strslfv3  13258  setsslid  13263  pwsdiagel  13510  pwssnf1o  13511  imasaddfnlemg  13527  imasaddvallemg  13528  mgmsscl  13574  plusffng  13578  mgmplusf  13579  mgm0  13582  mgm1  13583  opifismgmdc  13584  gsumfzval  13604  gsumprval  13612  sgrp1  13624  issgrpd  13625  prdsplusgsgrpcl  13627  mndpfo  13651  mndfo  13652  prdsplusgcl  13659  prdsidlem  13660  mnd1  13668  0subm  13697  mhmima  13704  grpinvfng  13757  isgrpinv  13767  grpinvid  13773  grpinvf1o  13783  grpinvadd  13791  grpsubf  13792  grpsubsub4  13806  grplactcnv  13815  grp1  13819  grp1inv  13820  prdsinvlem  13821  prdsinvgd  13823  qusgrp2  13830  mulgfng  13841  subginv  13898  resgrpisgrp  13912  subgintm  13915  0subg  13916  0nsg  13931  qusinv  13953  ghminv  13967  ghmrn  13974  ghmeql  13984  ghmnsgima  13985  kerf1ghm  13991  conjnmz  13996  rngass  14083  rngmneg1  14091  rngmneg2  14092  qusrng  14102  srgideu  14116  srgidmlem  14122  srgpcomp  14134  srg1expzeq1  14139  ringcl  14157  ringideu  14161  ringidmlem  14166  ringnegl  14195  ringnegr  14196  ring1  14203  qusring2  14210  opprringbg  14224  dvdsrd  14239  dvdsr01  14249  isunitd  14251  unitinvcl  14268  unitinvinv  14269  unitnegcl  14275  rhmmul  14309  rhmf1o  14313  nzrunit  14333  lringuplu  14341  subrngintm  14357  subrgsubm  14379  subrgintm  14388  rrgsupp  14411  aprsym  14430  aprnzr  14433  aprlring  14434  scaffng  14457  lmodscaf  14458  lsssn0  14518  lss1d  14531  lssintclm  14532  lspval  14538  lspcl  14539  lspsnid  14555  lspprid1  14559  lspsn  14564  sraval  14585  rspcl  14639  rspssid  14640  rspssp  14642  rnglidlmmgm  14644  rnglidlmsgrp  14645  cnfldneg  14721  zringinvg  14752  expghmap  14755  znzrhfo  14796  znf1o  14799  znhash  14804  znidomb  14806  znrrg  14808  psrbagfsupp  14819  psrbagfi  14823  psrbaglecl  14824  psrbagaddclfi  14825  psrbagcon  14826  psraddcl  14835  psr0cl  14836  psrnegcl  14838  psrneg  14842  psr1clfi  14843  mplsubgfilemm  14853  mplsubgfilemcl  14854  baspartn  14915  eltg3i  14921  tgclb  14930  topbas  14932  2basgeng  14947  topcld  14974  0cld  14977  uncld  14978  neif  15006  elnei  15017  0nei  15031  restbasg  15033  iscnp4  15083  cnpnei  15084  cnclima  15088  cncnp  15095  cnrest2r  15102  cndis  15106  lmff  15114  lmtopcnp  15115  txbas  15123  txopn  15130  txcnp  15136  upxp  15137  txdis1cn  15143  cnmpt11  15148  cnmpt21  15156  psmetge0  15196  xmetge0  15230  xmettpos  15235  xmetrtri  15241  metrtri  15242  xblpnfps  15263  xblpnf  15264  blfps  15274  blf  15275  ssblps  15290  ssbl  15291  blbas  15298  metss2  15363  xmettxlem  15374  xmettx  15375  qtopbas  15387  divcnap  15430  cncfss  15448  cdivcncfap  15469  expcncf  15474  cnopnap  15476  maxcncf  15480  mincncf  15481  dedekindeulemuub  15482  dedekindeulemlu  15486  dedekindeu  15488  suplociccex  15490  dedekindicclemuub  15491  dedekindicclemlu  15495  dedekindicclemicc  15497  ivthinclemlopn  15501  ivthinclemuopn  15503  ivthinc  15508  ivthreinc  15510  hoverlt1  15514  ellimc3apf  15525  limcimolemlt  15529  limcimo  15530  limcresi  15531  cnplimclemle  15533  reldvg  15544  dvfgg  15553  dvidlemap  15556  dvidrelem  15557  dvidsslem  15558  dvcjbr  15573  dvcj  15574  dvrecap  15578  dveflem  15591  dvef  15592  elply2  15600  elplyr  15605  plycj  15626  plyreres  15629  reeff1oleme  15637  pilem3  15648  sinq34lt0t  15696  cosq14gt0  15697  coseq0q4123  15699  tangtx  15703  sincosq1eq  15704  cosordlem  15714  logdivlti  15746  relogbval  15816  relogbzcl  15817  nnlogbexp  15824  logbgcd1irr  15832  logbgcd1irraplemexp  15833  logbgcd1irraplemap  15834  pellexlem1  15845  pellexlem3  15847  wilthlem1  15848  mpodvdsmulf1o  15858  mersenne  15865  perfectlem2  15868  perfect  15869  zabsle1  15872  lgslem1  15873  lgsval  15877  lgsfvalg  15878  lgsfcl2  15879  lgsval2lem  15883  lgscl1  15896  lgsmod  15899  lgsdir2lem5  15905  lgsdir2  15906  lgsdilem2  15909  lgsdi  15910  lgsne0  15911  gausslemma2dlem0c  15924  gausslemma2dlem0h  15929  gausslemma2dlem1a  15931  gausslemma2dlem1f1o  15933  gausslemma2dlem3  15936  lgseisenlem1  15943  lgseisenlem2  15944  lgseisenlem3  15945  lgseisenlem4  15946  lgseisen  15947  lgsquadlem1  15950  lgsquadlem2  15951  lgsquadlem3  15952  lgsquad3  15957  2lgslem3b1  15971  2lgslem3c1  15972  2lgs  15977  2lgsoddprmlem2  15979  2lgsoddprm  15986  2sqlem3  15990  2sqlem8  15996  2sqlem10  15998  structgrssvtx  16037  structgrssiedg  16038  ushgruhgr  16075  uhgrun  16081  incistruhgr  16085  upgrop  16099  upgruhgr  16106  umgrupgr  16107  umgrnloopv  16109  umgredgprv  16110  umgr0e  16113  upgr1edc  16116  umgr1een  16120  upgrun  16121  umgrun  16123  umgrislfupgrdom  16126  upgredg  16139  umgrpredgv  16142  usgrop  16161  usgrausgrien  16164  ausgrumgrien  16165  ausgrusgrien  16166  uspgrupgrushgr  16177  usgrumgr  16179  usgrumgruspgr  16180  usgruspgrben  16181  usgrislfuspgrdom  16185  edgssv2en  16194  usgrf1oedg  16200  usgredg4  16210  usgredg2vlem2  16218  usgredg2v  16219  ushgredgedg  16221  ushgredgedgloop  16223  usgrstrrepeen  16226  usgr0e  16227  uhgr0v0e  16229  uspgr1edc  16235  usgr1e  16236  griedg0ssusgr  16246  subgrprop3  16257  subgruhgredgdm  16265  subuhgr  16267  subupgr  16268  subumgr  16269  subusgr  16270  uhgrspansubgrlem  16271  1loopgrvd2fi  16300  1loopgrvd0fi  16301  1hevtxdg0fi  16302  vdegp1aid  16309  vdegp1bid  16310  wlkm  16334  wlkvtxiedg  16340  wlkvtxiedgg  16341  wlkeq  16349  wlk1walkdom  16354  uspgr2wlkeq  16360  uspgr2wlkeqi  16362  upgr2wlkdc  16372  wlkres  16374  trlreslem  16384  clwwlkccatlem  16395  clwwlkn1loopb  16415  clwwlkext2edg  16417  clwwlknonex2lem1  16432  clwwlknonex2  16434  trlsegvdeglem2  16456  trlsegvdeglem3  16457  eupth2lem3lem4fi  16468  eupth2lemsfi  16473  fnmptd  16576  bj-sels  16684  bj-nnelon  16729  pw1map  16769  pwle2  16772  pwf1oexmid  16773  pw1nct  16777  nninfall  16787  nninfsellemdc  16788  nninfself  16791  nnnninfex  16800  nninfnfiinf  16801  refeq  16808  isomninnlem  16814  cvgcmp2nlemabs  16816  trilpolemlt1  16825  trirec0  16828  apdifflemf  16830  apdifflemr  16831  apdiff  16832  qdiff  16833  iswomninnlem  16834  iswomni0  16836  ismkvnnlem  16837  reap0  16843  cndcap  16844  trimul0or  16845  gfsumval  16862  gsumgfsumlem  16865  gsumgfsum  16866  gfsumsn  16867  gfsump1  16868