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  713  pm4.55dc  946  mpbir2and  952  pm3.12dc  966  mpbir3and  1206  pm5.15dc  1433  eqeltrd  2307  eqnetrd  2425  3netr4d  2434  r19.30dc  2679  raleqtrrdv  2739  rexeqtrrdv  2740  sbcne12g  3144  eqsstrd  3262  3sstr4d  3271  eqbrtrd  4111  3brtr4d  4121  snelpwi  4305  prelpwi  4308  pwel  4312  ordelon  4482  onin  4485  elelsuc  4508  onsuc  4601  onsucb  4603  onintonm  4617  omsinds  4722  sosng  4801  relssdv  4820  eqbrrdv  4825  eqrelrdv2  4827  relsnopg  4832  breldmg  4939  elrnmptdv  4988  iss  5061  xpimasn  5187  elxp4  5226  elxp5  5227  iotam  5320  funssres  5371  f0rn0  5534  fimadmfo  5571  sefvex  5663  fdmeu  5692  fvun1  5715  eqfnfvd  5750  fvimacnvi  5764  fvimacnv  5765  fvelrn  5781  fmpt3d  5806  fmpt2d  5812  resflem  5814  fmptco  5816  fsn  5822  funopsn  5833  fncofn  5835  ftpg  5841  fconst2g  5872  funfvima3  5893  elabrexg  5904  foeqcnvco  5936  f1eqcocnv  5937  fliftfun  5942  fliftfund  5943  fliftval  5946  riota5f  6003  f1ofveu  6011  f1ocnvd  6230  f1opw2  6234  off  6253  offval2  6256  ofrfval2  6257  offveq  6261  caofref  6265  caofinvl  6266  elxp6  6337  cnvf1olem  6394  f2ndf  6396  f1od2  6405  elmpom  6408  tposf12  6440  smores2  6465  tfrlemisucaccv  6496  tfrlemibfn  6499  tfr1onlemsucaccv  6512  tfr1onlembfn  6515  tfrcllemsucaccv  6525  tfrcllembfn  6528  tfrcl  6535  tfri3  6538  frecabcl  6570  nnsucsssuc  6665  ersym  6719  ertr  6722  swoer  6735  erth  6753  riinerm  6782  qliftfund  6792  eroprf  6802  ecopoverg  6810  th3qlem1  6811  elmapssres  6847  mapss  6865  fdiagfn  6866  ixpssmap2g  6901  mapsnf1o  6911  f1oen4g  6930  f1dom4g  6931  f1dom2g  6934  dom3d  6952  en2prd  6997  dom1oi  7008  pw2f1odclem  7025  fopwdom  7027  mapxpen  7039  nndomo  7055  dif1en  7073  findcard2  7083  findcard2s  7084  diffisn  7087  fimax2gtrilemstep  7095  eqsndc  7100  fientri3  7112  tpfidceq  7127  fiintim  7128  opabfi  7137  f1dmvrnfibi  7148  sbthlemi6  7166  elfir  7177  fifo  7184  supelti  7206  supsnti  7209  cnvinfex  7222  ordiso2  7239  updjud  7286  djudom  7297  difinfsn  7304  ctssdc  7317  enumctlemm  7318  enumct  7319  nninfninc  7327  enomnilem  7342  fodjuf  7349  ismkvnex  7359  omnimkv  7360  enmkvlem  7365  enwomnilem  7373  nninfdcinf  7375  nninfwlporlem  7377  isnumi  7391  exmidfodomrlemrALT  7419  finacn  7424  djudoml  7439  djudomr  7440  netap  7478  2omotaplemap  7481  2omotaplemst  7482  exmidapne  7484  cc2lem  7490  cc3  7492  ltsopi  7545  pitri3or  7547  ltdcpi  7548  indpi  7567  enqdc  7586  enqdc1  7587  addcmpblnq  7592  mulcanenq  7610  recrecnq  7619  nqtri3or  7621  ltdcnq  7622  ltsonq  7623  ltaddnq  7632  subhalfnqq  7639  archnqq  7642  prarloclemarch2  7644  enq0tr  7659  nqnq0  7666  addcmpblnq0  7668  mulcanenq0ec  7670  nnnq0lem1  7671  nqpnq0nq  7678  nq0m0r  7681  nq02m  7690  prarloclemlt  7718  prarloclemcalc  7727  addlocpr  7761  nqprl  7776  nqpru  7777  addnqprlemrl  7782  addnqprlemru  7783  prmuloclemcalc  7790  mullocprlem  7795  mulnqprlemrl  7798  mulnqprlemru  7799  1idprl  7815  1idpru  7816  ltaddpr  7822  ltexprlemm  7825  ltexprlemopl  7826  ltexprlemopu  7828  ltexprlemdisj  7831  ltexprlemrl  7835  ltexprlemru  7837  addcanprleml  7839  addcanprlemu  7840  addcanprg  7841  prplnqu  7845  recexprlemloc  7856  recexprlem1ssl  7858  recexprlem1ssu  7859  aptiprleml  7864  aptiprlemu  7865  archpr  7868  cauappcvgprlemm  7870  cauappcvgprlemopl  7871  cauappcvgprlemloc  7877  cauappcvgprlemladdfu  7879  cauappcvgprlemladdfl  7880  cauappcvgprlem1  7884  cauappcvgprlem2  7885  caucvgprlemnkj  7891  caucvgprlemopl  7894  caucvgprlemloc  7900  caucvgprlemladdfu  7902  caucvgprlem2  7905  caucvgprprlemnkltj  7914  caucvgprprlemopl  7922  caucvgprprlemloc  7928  caucvgprprlemexbt  7931  caucvgprprlemaddq  7933  caucvgprprlem2  7935  suplocexprlemmu  7943  suplocexprlemru  7944  suplocexprlemloc  7946  suplocexprlemlub  7949  prsrlem1  7967  0idsr  7992  1idsr  7993  recexgt0sr  7998  archsr  8007  prsradd  8011  caucvgsrlemcau  8018  caucvgsrlembound  8019  caucvgsrlemoffgt1  8024  suplocsrlemb  8031  suplocsrlempr  8032  suplocsrlem  8033  pitonnlem1p1  8071  pitonn  8073  pitoregt0  8074  peano2nnnn  8078  recidpirq  8083  axcaucvglemval  8122  leid  8268  nltled  8305  readdcan  8324  addneintrd  8372  addneintr2d  8373  pncan  8390  subsub2  8412  subsub4  8417  negned  8492  subne0d  8504  subneintrd  8539  subneintr2d  8541  subeq0bd  8563  subdi  8569  gt0add  8758  rimul  8770  rereim  8771  ltmul1a  8776  apreim  8788  apirr  8790  mulap0r  8800  msqge0  8801  mulge0  8804  gt0ap0  8811  ltap  8818  subap0d  8829  recexaplem2  8837  mulap0bad  8844  mulap0bbd  8845  mul0eqap  8855  divrecap  8873  div0ap  8887  div1  8888  recrecap  8894  divdivdivap  8898  ddcanap  8911  rerecclap  8915  div2negap  8920  diveqap1bd  9021  recgt0  9035  prodgt0  9037  lemul1a  9043  recp1lt1  9084  squeeze0  9089  peano2nn  9160  div4p1lem1div2  9403  arch  9404  peano2z  9520  peano2zm  9522  ztri3or  9527  nn0n0n1ge2  9555  zextle  9576  gtndiv  9580  suprzclex  9583  nn0ind-raph  9602  uzid  9775  uzneg  9780  uztric  9783  uz11  9784  eluzp1l  9786  qdivcl  9882  irrmul  9886  irrmulap  9887  rpnegap  9926  negelrpd  9928  ledivge1le  9966  mul2lt0rlt0  9999  mul2lt0rgt0  10000  nn0ledivnn  10007  ltpnf  10020  mnflt  10023  pnfge  10029  mnfle  10032  xrlttr  10035  xrltso  10036  xrlttri3  10037  xrleid  10040  xaddass2  10110  xltadd1  10116  xlt2add  10120  xleaddadd  10127  iccf1o  10244  fztri3or  10279  fznlem  10281  fzn  10282  fzsplit2  10290  fznatpl1  10316  uzsplit  10332  fseq1p1m1  10334  fzm1  10340  fznn0sub2  10368  difelfznle  10375  1fv  10379  fzodcel  10393  fzospliti  10418  fzouzsplit  10421  eluzgtdifelfzo  10448  exfzdc  10492  subfzo0  10494  zsupcllemstep  10495  zsupcl  10497  zssinfcl  10498  infssuzex  10499  infssuzcldc  10501  suprzubdc  10502  nninfdcex  10503  qdcle  10512  exbtwnz  10516  qbtwnrelemcalc  10521  flqlelt  10542  qfraclt1  10546  qfracge0  10547  flqltnz  10553  btwnzge0  10566  flhalf  10568  fldiv4lem1div2uz2  10572  ceiqle  10581  intfracq  10588  mulqmod0  10598  modqge0  10600  modqlt  10601  modqid  10617  modqid0  10618  m1modge3gt1  10639  modqltm1p1mod  10644  q2txmodxeq0  10652  modaddmodlo  10656  modsumfzodifsn  10664  addmodlteq  10666  frecuzrdgtcl  10680  frecuzrdgtclt  10689  uzennn  10704  uzsinds  10712  seqf  10732  seqf2  10736  monoord2  10754  iseqf1olemqk  10775  iseqf1olemjpcl  10776  iseqf1olemqpcl  10777  seq3f1olemqsumkj  10779  seq3f1olemqsum  10781  seq3f1olemstep  10782  seq3f1oleml  10784  seqf1oglem1  10787  ser3le  10805  exp3vallem  10808  exp3val  10809  expp1  10814  expcllem  10818  ltexp2a  10859  leexp2a  10860  nn0ltexp2  10977  faclbnd  11009  faclbnd2  11010  faclbnd3  11011  bcval5  11031  bcpasc  11034  hashennn  11048  fihasheqf1oi  11055  hashsng  11066  fihashfn  11069  hashun  11074  fihashss  11086  fihashssdif  11088  hashfz  11091  hashxp  11096  fimaxq  11097  zfz1isolem1  11110  seq3coll  11112  hashdmprop2dom  11114  wrdf  11128  wrdlenge2n0  11158  fstwrdne0  11162  wrdred1hash  11166  ccatvalfn  11187  ccatsymb  11188  ccatlid  11192  ccatrid  11193  ccatrn  11195  ccatalpha  11199  eqs1  11214  ccats1val2  11226  fzowrddc  11237  swrdlen  11242  swrdnd  11249  swrd0g  11250  swrdfv2  11253  swrdwrdsymbg  11254  pfxn0  11278  pfxwrdsymbg  11280  pfxsuff1eqwrdeq  11289  swrdswrd  11295  ccats1pfxeq  11304  ccats1pfxeqrex  11305  wrdind  11312  wrd2ind  11313  swrdccatin1  11315  pfxccatin12lem4  11316  swrdccatin2  11319  pfxccatin12  11323  pfxccat3a  11328  swrdccat3blem  11329  pfxccatid  11331  swrdccatin2d  11334  shftfn  11407  cjth  11429  cjmulrcl  11470  reim0bd  11527  rerebd  11528  cjrebd  11529  caucvgre  11564  cvg1nlemcxze  11565  cvg1nlemcau  11567  cvg1nlemres  11568  recvguniq  11578  resqrexlemover  11593  resqrexlemdec  11594  resqrexlemgt0  11603  resqrexlemoverl  11604  resqrexlemglsq  11605  rersqrtthlem  11613  sqrtgt0  11617  leabs  11657  absexpzap  11663  absle  11672  recvalap  11680  abstri  11687  abs2dif  11689  amgm2  11701  absne0d  11770  maxleim  11788  maxabslemab  11789  maxabslemlub  11790  maxltsup  11801  zmaxcl  11807  fimaxre2  11810  minmax  11813  rpmincl  11821  bdtrilem  11822  bdtri  11823  xrmaxleim  11827  xrmaxiflemcom  11832  xrmaxltsup  11841  xrmaxadd  11844  xrminmax  11848  xrminrpcl  11857  climconst  11873  climuni  11876  2clim  11884  climcn1  11891  climcn2  11892  reccn2ap  11896  climge0  11908  climle  11917  climsqz  11918  climsqz2  11919  serf0  11935  summodclem3  11964  summodclem2a  11965  fsumcl2lem  11982  sumpr  11997  sumtp  11998  fsum0diaglem  12024  mptfzshft  12026  fsumle  12047  fsumlt  12048  divcnv  12081  trireciplem  12084  expcnvap0  12086  expcnv  12088  explecnv  12089  geosergap  12090  cvgratnnlembern  12107  cvgratnnlemabsle  12111  cvgratnnlemsumlt  12112  cvgratz  12116  cvgratgt0  12117  mertenslemi1  12119  mertenslem2  12120  mertensabs  12121  clim2divap  12124  prodmodclem3  12159  prodmodclem2a  12160  fprodseq  12167  fprodmul  12175  fprodfac  12199  fprodconst  12204  fprodap0  12205  fprodap0f  12220  fprodle  12224  eftcl  12238  ef0lem  12244  efsub  12265  eftlub  12274  eflegeo  12285  tanval2ap  12297  sinadd  12320  cos2t  12334  cos2tsin  12335  sin01bnd  12341  cos01bnd  12342  eirraplem  12361  dvdsval2  12374  dvdsdc  12382  dvds0lem  12385  zdvdsdc  12396  dvdscmulr  12404  dvdsmulcr  12405  fsumdvds  12426  dvdslelemd  12427  divconjdvds  12433  dvdsext  12439  fzm1ndvds  12440  dvdsmod  12446  3dvds  12448  oexpneg  12461  2tp1odd  12468  mulsucdiv2z  12469  2teven  12471  zeo5  12472  opeo  12481  omeo  12482  nn0ob  12492  divalglemnqt  12504  bitsdc  12531  bits0o  12534  bitsfzolem  12538  bitsfzo  12539  bitsmod  12540  bitscmp  12542  bitsinv1lem  12545  gcddvds  12557  dvdslegcd  12558  gcdneg  12576  bezoutlemnewy  12590  bezoutlemstep  12591  bezoutlema  12593  bezoutlemb  12594  bezoutlemmo  12600  bezoutlemle  12602  bezoutlemsup  12603  dfgcd3  12604  bezout  12605  dfgcd2  12608  uzwodc  12631  lcmcllem  12662  lcmneg  12669  lcmgcdlem  12672  lcmdvds  12674  lcmid  12675  3lcm2e6woprm  12681  6lcm4e12  12682  ncoprmgcdne1b  12684  mulgcddvds  12689  divgcdcoprmex  12697  cncongr1  12698  cncongr2  12699  isprm2lem  12711  prmind2  12715  dvdsnprmd  12720  prm2orodd  12721  sqnprm  12731  isprm5lem  12736  rpexp  12748  sqrt2irrlem  12756  oddpwdclemdc  12768  sqrt2irraplemnn  12774  qnumdencoprm  12788  qeqnumdivden  12789  nn0gcdsq  12795  nn0sqrtelqelz  12801  nonsq  12802  phicl2  12809  phibnd  12812  hashdvds  12816  phiprmpw  12817  phimullem  12820  eulerthlemrprm  12824  eulerthlema  12825  eulerthlemth  12827  prmdiveq  12831  hashgcdlem  12833  odzdvds  12841  modprminv  12845  nnnn0modprm0  12851  modprmn0modprm0  12852  pythagtriplem10  12865  pythagtriplem19  12878  pythagtrip  12879  pcpre1  12888  pcpremul  12889  pceu  12891  pcmul  12897  pcdiv  12898  pcqmul  12899  pcqdiv  12903  pcexp  12905  pcdvdsb  12916  pcidlem  12919  pcdvdstr  12923  pcgcd1  12924  pc2dvds  12926  pcprmpw2  12929  difsqpwdvds  12934  pcaddlem  12935  pcadd  12936  pcadd2  12937  pcmpt  12939  pcmptdvds  12941  pcprod  12942  fldivp1  12944  pcfaclem  12945  pcfac  12946  pcbc  12947  qexpz  12948  pockthlem  12952  pockthg  12953  1arithlem4  12962  1arith  12963  1arith2  12964  4sqlem6  12979  4sqlem8  12981  4sqlem9  12982  4sqlem10  12983  4sqexercise1  12994  4sqexercise2  12995  4sqlemsdc  12996  4sqlem11  12997  4sqlem12  12998  4sqlem15  13001  4sqlem16  13002  4sqlem17  13003  znnen  13042  ennnfonelemk  13044  ennnfonelemkh  13056  ennnfonelemhf1o  13057  ennnfonelemrnh  13060  ennnfonelemfun  13061  ennnfonelemf1  13062  ennnfonelemrn  13063  ennnfonelemnn0  13066  ctinfomlemom  13071  ctiunctlemudc  13081  unct  13086  omctfn  13087  ssnnctlemct  13090  nninfdclemp1  13094  nninfdc  13097  structfung  13122  setsfun  13140  setsfun0  13141  setscom  13145  strslfv3  13151  setsslid  13156  pwsdiagel  13403  pwssnf1o  13404  imasaddfnlemg  13420  imasaddvallemg  13421  mgmsscl  13467  plusffng  13471  mgmplusf  13472  mgm0  13475  mgm1  13476  opifismgmdc  13477  gsumfzval  13497  gsumprval  13505  sgrp1  13517  issgrpd  13518  prdsplusgsgrpcl  13520  mndpfo  13544  mndfo  13545  prdsplusgcl  13552  prdsidlem  13553  mnd1  13561  0subm  13590  mhmima  13597  grpinvfng  13650  isgrpinv  13660  grpinvid  13666  grpinvf1o  13676  grpinvadd  13684  grpsubf  13685  grpsubsub4  13699  grplactcnv  13708  grp1  13712  grp1inv  13713  prdsinvlem  13714  prdsinvgd  13716  qusgrp2  13723  mulgfng  13734  subginv  13791  resgrpisgrp  13805  subgintm  13808  0subg  13809  0nsg  13824  qusinv  13846  ghminv  13860  ghmrn  13867  ghmeql  13877  ghmnsgima  13878  kerf1ghm  13884  conjnmz  13889  rngass  13976  rngmneg1  13984  rngmneg2  13985  qusrng  13995  srgideu  14009  srgidmlem  14015  srgpcomp  14027  srg1expzeq1  14032  ringcl  14050  ringideu  14054  ringidmlem  14059  ringnegl  14088  ringnegr  14089  ring1  14096  qusring2  14103  opprringbg  14117  dvdsrd  14132  dvdsr01  14142  isunitd  14144  unitinvcl  14161  unitinvinv  14162  unitnegcl  14168  rhmmul  14202  rhmf1o  14206  nzrunit  14226  lringuplu  14234  subrngintm  14250  subrgsubm  14272  subrgintm  14281  aprsym  14322  scaffng  14347  lmodscaf  14348  lsssn0  14408  lss1d  14421  lssintclm  14422  lspval  14428  lspcl  14429  lspsnid  14445  lspprid1  14449  lspsn  14454  sraval  14475  rspcl  14529  rspssid  14530  rspssp  14532  rnglidlmmgm  14534  rnglidlmsgrp  14535  cnfldneg  14611  zringinvg  14642  expghmap  14645  znzrhfo  14686  znf1o  14689  znhash  14694  znidomb  14696  znrrg  14698  psrbagfi  14712  psrbaglecl  14713  psrbagcon  14714  psraddcl  14723  psr0cl  14724  psrnegcl  14726  psrneg  14730  psr1clfi  14731  mplsubgfilemm  14741  mplsubgfilemcl  14742  baspartn  14803  eltg3i  14809  tgclb  14818  topbas  14820  2basgeng  14835  topcld  14862  0cld  14865  uncld  14866  neif  14894  elnei  14905  0nei  14919  restbasg  14921  iscnp4  14971  cnpnei  14972  cnclima  14976  cncnp  14983  cnrest2r  14990  cndis  14994  lmff  15002  lmtopcnp  15003  txbas  15011  txopn  15018  txcnp  15024  upxp  15025  txdis1cn  15031  cnmpt11  15036  cnmpt21  15044  psmetge0  15084  xmetge0  15118  xmettpos  15123  xmetrtri  15129  metrtri  15130  xblpnfps  15151  xblpnf  15152  blfps  15162  blf  15163  ssblps  15178  ssbl  15179  blbas  15186  metss2  15251  xmettxlem  15262  xmettx  15263  qtopbas  15275  divcnap  15318  cncfss  15336  cdivcncfap  15357  expcncf  15362  cnopnap  15364  maxcncf  15368  mincncf  15369  dedekindeulemuub  15370  dedekindeulemlu  15374  dedekindeu  15376  suplociccex  15378  dedekindicclemuub  15379  dedekindicclemlu  15383  dedekindicclemicc  15385  ivthinclemlopn  15389  ivthinclemuopn  15391  ivthinc  15396  ivthreinc  15398  hoverlt1  15402  ellimc3apf  15413  limcimolemlt  15417  limcimo  15418  limcresi  15419  cnplimclemle  15421  reldvg  15432  dvfgg  15441  dvidlemap  15444  dvidrelem  15445  dvidsslem  15446  dvcjbr  15461  dvcj  15462  dvrecap  15466  dveflem  15479  dvef  15480  elply2  15488  elplyr  15493  plycj  15514  plyreres  15517  reeff1oleme  15525  pilem3  15536  sinq34lt0t  15584  cosq14gt0  15585  coseq0q4123  15587  tangtx  15591  sincosq1eq  15592  cosordlem  15602  logdivlti  15634  relogbval  15704  relogbzcl  15705  nnlogbexp  15712  logbgcd1irr  15720  logbgcd1irraplemexp  15721  logbgcd1irraplemap  15722  wilthlem1  15733  mpodvdsmulf1o  15743  mersenne  15750  perfectlem2  15753  perfect  15754  zabsle1  15757  lgslem1  15758  lgsval  15762  lgsfvalg  15763  lgsfcl2  15764  lgsval2lem  15768  lgscl1  15781  lgsmod  15784  lgsdir2lem5  15790  lgsdir2  15791  lgsdilem2  15794  lgsdi  15795  lgsne0  15796  gausslemma2dlem0c  15809  gausslemma2dlem0h  15814  gausslemma2dlem1a  15816  gausslemma2dlem1f1o  15818  gausslemma2dlem3  15821  lgseisenlem1  15828  lgseisenlem2  15829  lgseisenlem3  15830  lgseisenlem4  15831  lgseisen  15832  lgsquadlem1  15835  lgsquadlem2  15836  lgsquadlem3  15837  lgsquad3  15842  2lgslem3b1  15856  2lgslem3c1  15857  2lgs  15862  2lgsoddprmlem2  15864  2lgsoddprm  15871  2sqlem3  15875  2sqlem8  15881  2sqlem10  15883  structgrssvtx  15922  structgrssiedg  15923  ushgruhgr  15960  uhgrun  15966  incistruhgr  15970  upgrop  15984  upgruhgr  15991  umgrupgr  15992  umgrnloopv  15994  umgredgprv  15995  umgr0e  15998  upgr1edc  16001  umgr1een  16005  upgrun  16006  umgrun  16008  umgrislfupgrdom  16011  upgredg  16024  umgrpredgv  16027  usgrop  16046  usgrausgrien  16049  ausgrumgrien  16050  ausgrusgrien  16051  uspgrupgrushgr  16062  usgrumgr  16064  usgrumgruspgr  16065  usgruspgrben  16066  usgrislfuspgrdom  16070  edgssv2en  16079  usgrf1oedg  16085  usgredg4  16095  usgredg2vlem2  16103  usgredg2v  16104  ushgredgedg  16106  ushgredgedgloop  16108  usgrstrrepeen  16111  usgr0e  16112  uhgr0v0e  16114  uspgr1edc  16120  usgr1e  16121  griedg0ssusgr  16131  subgrprop3  16142  subgruhgredgdm  16150  subuhgr  16152  subupgr  16153  subumgr  16154  subusgr  16155  uhgrspansubgrlem  16156  1loopgrvd2fi  16185  1loopgrvd0fi  16186  1hevtxdg0fi  16187  vdegp1aid  16194  vdegp1bid  16195  wlkm  16219  wlkvtxiedg  16225  wlkvtxiedgg  16226  wlkeq  16234  wlk1walkdom  16239  uspgr2wlkeq  16245  uspgr2wlkeqi  16247  upgr2wlkdc  16257  wlkres  16259  trlreslem  16269  clwwlkccatlem  16280  clwwlkn1loopb  16300  clwwlkext2edg  16302  clwwlknonex2lem1  16317  clwwlknonex2  16319  trlsegvdeglem2  16341  trlsegvdeglem3  16342  eupth2lem3lem4fi  16353  eupth2lemsfi  16358  fnmptd  16461  bj-sels  16569  bj-nnelon  16614  2omap  16654  pw1map  16656  pwle2  16659  pwf1oexmid  16660  pw1nct  16664  nninfall  16674  nninfsellemdc  16675  nninfself  16678  nnnninfex  16687  nninfnfiinf  16688  refeq  16695  isomninnlem  16701  cvgcmp2nlemabs  16703  trilpolemlt1  16712  trirec0  16715  apdifflemf  16717  apdifflemr  16718  apdiff  16719  qdiff  16720  iswomninnlem  16721  iswomni0  16723  ismkvnnlem  16724  reap0  16730  cndcap  16731  gfsumval  16748  gsumgfsumlem  16751  gsumgfsum  16752  gfsumsn  16753  gfsump1  16754