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  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  11120  wrdlenge2n0  11150  fstwrdne0  11154  wrdred1hash  11158  ccatvalfn  11179  ccatsymb  11180  ccatlid  11184  ccatrid  11185  ccatrn  11187  ccatalpha  11191  eqs1  11206  ccats1val2  11218  fzowrddc  11229  swrdlen  11234  swrdnd  11241  swrd0g  11242  swrdfv2  11245  swrdwrdsymbg  11246  pfxn0  11270  pfxwrdsymbg  11272  pfxsuff1eqwrdeq  11281  swrdswrd  11287  ccats1pfxeq  11296  ccats1pfxeqrex  11297  wrdind  11304  wrd2ind  11305  swrdccatin1  11307  pfxccatin12lem4  11308  swrdccatin2  11311  pfxccatin12  11315  pfxccat3a  11320  swrdccat3blem  11321  pfxccatid  11323  swrdccatin2d  11326  shftfn  11386  cjth  11408  cjmulrcl  11449  reim0bd  11506  rerebd  11507  cjrebd  11508  caucvgre  11543  cvg1nlemcxze  11544  cvg1nlemcau  11546  cvg1nlemres  11547  recvguniq  11557  resqrexlemover  11572  resqrexlemdec  11573  resqrexlemgt0  11582  resqrexlemoverl  11583  resqrexlemglsq  11584  rersqrtthlem  11592  sqrtgt0  11596  leabs  11636  absexpzap  11642  absle  11651  recvalap  11659  abstri  11666  abs2dif  11668  amgm2  11680  absne0d  11749  maxleim  11767  maxabslemab  11768  maxabslemlub  11769  maxltsup  11780  zmaxcl  11786  fimaxre2  11789  minmax  11792  rpmincl  11800  bdtrilem  11801  bdtri  11802  xrmaxleim  11806  xrmaxiflemcom  11811  xrmaxltsup  11820  xrmaxadd  11823  xrminmax  11827  xrminrpcl  11836  climconst  11852  climuni  11855  2clim  11863  climcn1  11870  climcn2  11871  reccn2ap  11875  climge0  11887  climle  11896  climsqz  11897  climsqz2  11898  serf0  11914  summodclem3  11943  summodclem2a  11944  fsumcl2lem  11961  sumpr  11976  sumtp  11977  fsum0diaglem  12003  mptfzshft  12005  fsumle  12026  fsumlt  12027  divcnv  12060  trireciplem  12063  expcnvap0  12065  expcnv  12067  explecnv  12068  geosergap  12069  cvgratnnlembern  12086  cvgratnnlemabsle  12090  cvgratnnlemsumlt  12091  cvgratz  12095  cvgratgt0  12096  mertenslemi1  12098  mertenslem2  12099  mertensabs  12100  clim2divap  12103  prodmodclem3  12138  prodmodclem2a  12139  fprodseq  12146  fprodmul  12154  fprodfac  12178  fprodconst  12183  fprodap0  12184  fprodap0f  12199  fprodle  12203  eftcl  12217  ef0lem  12223  efsub  12244  eftlub  12253  eflegeo  12264  tanval2ap  12276  sinadd  12299  cos2t  12313  cos2tsin  12314  sin01bnd  12320  cos01bnd  12321  eirraplem  12340  dvdsval2  12353  dvdsdc  12361  dvds0lem  12364  zdvdsdc  12375  dvdscmulr  12383  dvdsmulcr  12384  fsumdvds  12405  dvdslelemd  12406  divconjdvds  12412  dvdsext  12418  fzm1ndvds  12419  dvdsmod  12425  3dvds  12427  oexpneg  12440  2tp1odd  12447  mulsucdiv2z  12448  2teven  12450  zeo5  12451  opeo  12460  omeo  12461  nn0ob  12471  divalglemnqt  12483  bitsdc  12510  bits0o  12513  bitsfzolem  12517  bitsfzo  12518  bitsmod  12519  bitscmp  12521  bitsinv1lem  12524  gcddvds  12536  dvdslegcd  12537  gcdneg  12555  bezoutlemnewy  12569  bezoutlemstep  12570  bezoutlema  12572  bezoutlemb  12573  bezoutlemmo  12579  bezoutlemle  12581  bezoutlemsup  12582  dfgcd3  12583  bezout  12584  dfgcd2  12587  uzwodc  12610  lcmcllem  12641  lcmneg  12648  lcmgcdlem  12651  lcmdvds  12653  lcmid  12654  3lcm2e6woprm  12660  6lcm4e12  12661  ncoprmgcdne1b  12663  mulgcddvds  12668  divgcdcoprmex  12676  cncongr1  12677  cncongr2  12678  isprm2lem  12690  prmind2  12694  dvdsnprmd  12699  prm2orodd  12700  sqnprm  12710  isprm5lem  12715  rpexp  12727  sqrt2irrlem  12735  oddpwdclemdc  12747  sqrt2irraplemnn  12753  qnumdencoprm  12767  qeqnumdivden  12768  nn0gcdsq  12774  nn0sqrtelqelz  12780  nonsq  12781  phicl2  12788  phibnd  12791  hashdvds  12795  phiprmpw  12796  phimullem  12799  eulerthlemrprm  12803  eulerthlema  12804  eulerthlemth  12806  prmdiveq  12810  hashgcdlem  12812  odzdvds  12820  modprminv  12824  nnnn0modprm0  12830  modprmn0modprm0  12831  pythagtriplem10  12844  pythagtriplem19  12857  pythagtrip  12858  pcpre1  12867  pcpremul  12868  pceu  12870  pcmul  12876  pcdiv  12877  pcqmul  12878  pcqdiv  12882  pcexp  12884  pcdvdsb  12895  pcidlem  12898  pcdvdstr  12902  pcgcd1  12903  pc2dvds  12905  pcprmpw2  12908  difsqpwdvds  12913  pcaddlem  12914  pcadd  12915  pcadd2  12916  pcmpt  12918  pcmptdvds  12920  pcprod  12921  fldivp1  12923  pcfaclem  12924  pcfac  12925  pcbc  12926  qexpz  12927  pockthlem  12931  pockthg  12932  1arithlem4  12941  1arith  12942  1arith2  12943  4sqlem6  12958  4sqlem8  12960  4sqlem9  12961  4sqlem10  12962  4sqexercise1  12973  4sqexercise2  12974  4sqlemsdc  12975  4sqlem11  12976  4sqlem12  12977  4sqlem15  12980  4sqlem16  12981  4sqlem17  12982  znnen  13021  ennnfonelemk  13023  ennnfonelemkh  13035  ennnfonelemhf1o  13036  ennnfonelemrnh  13039  ennnfonelemfun  13040  ennnfonelemf1  13041  ennnfonelemrn  13042  ennnfonelemnn0  13045  ctinfomlemom  13050  ctiunctlemudc  13060  unct  13065  omctfn  13066  ssnnctlemct  13069  nninfdclemp1  13073  nninfdc  13076  structfung  13101  setsfun  13119  setsfun0  13120  setscom  13124  strslfv3  13130  setsslid  13135  pwsdiagel  13382  pwssnf1o  13383  imasaddfnlemg  13399  imasaddvallemg  13400  mgmsscl  13446  plusffng  13450  mgmplusf  13451  mgm0  13454  mgm1  13455  opifismgmdc  13456  gsumfzval  13476  gsumprval  13484  sgrp1  13496  issgrpd  13497  prdsplusgsgrpcl  13499  mndpfo  13523  mndfo  13524  prdsplusgcl  13531  prdsidlem  13532  mnd1  13540  0subm  13569  mhmima  13576  grpinvfng  13629  isgrpinv  13639  grpinvid  13645  grpinvf1o  13655  grpinvadd  13663  grpsubf  13664  grpsubsub4  13678  grplactcnv  13687  grp1  13691  grp1inv  13692  prdsinvlem  13693  prdsinvgd  13695  qusgrp2  13702  mulgfng  13713  subginv  13770  resgrpisgrp  13784  subgintm  13787  0subg  13788  0nsg  13803  qusinv  13825  ghminv  13839  ghmrn  13846  ghmeql  13856  ghmnsgima  13857  kerf1ghm  13863  conjnmz  13868  rngass  13955  rngmneg1  13963  rngmneg2  13964  qusrng  13974  srgideu  13988  srgidmlem  13994  srgpcomp  14006  srg1expzeq1  14011  ringcl  14029  ringideu  14033  ringidmlem  14038  ringnegl  14067  ringnegr  14068  ring1  14075  qusring2  14082  opprringbg  14096  dvdsrd  14111  dvdsr01  14121  isunitd  14123  unitinvcl  14140  unitinvinv  14141  unitnegcl  14147  rhmmul  14181  rhmf1o  14185  nzrunit  14205  lringuplu  14213  subrngintm  14229  subrgsubm  14251  subrgintm  14260  aprsym  14301  scaffng  14326  lmodscaf  14327  lsssn0  14387  lss1d  14400  lssintclm  14401  lspval  14407  lspcl  14408  lspsnid  14424  lspprid1  14428  lspsn  14433  sraval  14454  rspcl  14508  rspssid  14509  rspssp  14511  rnglidlmmgm  14513  rnglidlmsgrp  14514  cnfldneg  14590  zringinvg  14621  expghmap  14624  znzrhfo  14665  znf1o  14668  znhash  14673  znidomb  14675  znrrg  14677  psrbagfi  14690  psraddcl  14697  psr0cl  14698  psrnegcl  14700  psrneg  14704  psr1clfi  14705  mplsubgfilemm  14715  mplsubgfilemcl  14716  baspartn  14777  eltg3i  14783  tgclb  14792  topbas  14794  2basgeng  14809  topcld  14836  0cld  14839  uncld  14840  neif  14868  elnei  14879  0nei  14893  restbasg  14895  iscnp4  14945  cnpnei  14946  cnclima  14950  cncnp  14957  cnrest2r  14964  cndis  14968  lmff  14976  lmtopcnp  14977  txbas  14985  txopn  14992  txcnp  14998  upxp  14999  txdis1cn  15005  cnmpt11  15010  cnmpt21  15018  psmetge0  15058  xmetge0  15092  xmettpos  15097  xmetrtri  15103  metrtri  15104  xblpnfps  15125  xblpnf  15126  blfps  15136  blf  15137  ssblps  15152  ssbl  15153  blbas  15160  metss2  15225  xmettxlem  15236  xmettx  15237  qtopbas  15249  divcnap  15292  cncfss  15310  cdivcncfap  15331  expcncf  15336  cnopnap  15338  maxcncf  15342  mincncf  15343  dedekindeulemuub  15344  dedekindeulemlu  15348  dedekindeu  15350  suplociccex  15352  dedekindicclemuub  15353  dedekindicclemlu  15357  dedekindicclemicc  15359  ivthinclemlopn  15363  ivthinclemuopn  15365  ivthinc  15370  ivthreinc  15372  hoverlt1  15376  ellimc3apf  15387  limcimolemlt  15391  limcimo  15392  limcresi  15393  cnplimclemle  15395  reldvg  15406  dvfgg  15415  dvidlemap  15418  dvidrelem  15419  dvidsslem  15420  dvcjbr  15435  dvcj  15436  dvrecap  15440  dveflem  15453  dvef  15454  elply2  15462  elplyr  15467  plycj  15488  plyreres  15491  reeff1oleme  15499  pilem3  15510  sinq34lt0t  15558  cosq14gt0  15559  coseq0q4123  15561  tangtx  15565  sincosq1eq  15566  cosordlem  15576  logdivlti  15608  relogbval  15678  relogbzcl  15679  nnlogbexp  15686  logbgcd1irr  15694  logbgcd1irraplemexp  15695  logbgcd1irraplemap  15696  wilthlem1  15707  mpodvdsmulf1o  15717  mersenne  15724  perfectlem2  15727  perfect  15728  zabsle1  15731  lgslem1  15732  lgsval  15736  lgsfvalg  15737  lgsfcl2  15738  lgsval2lem  15742  lgscl1  15755  lgsmod  15758  lgsdir2lem5  15764  lgsdir2  15765  lgsdilem2  15768  lgsdi  15769  lgsne0  15770  gausslemma2dlem0c  15783  gausslemma2dlem0h  15788  gausslemma2dlem1a  15790  gausslemma2dlem1f1o  15792  gausslemma2dlem3  15795  lgseisenlem1  15802  lgseisenlem2  15803  lgseisenlem3  15804  lgseisenlem4  15805  lgseisen  15806  lgsquadlem1  15809  lgsquadlem2  15810  lgsquadlem3  15811  lgsquad3  15816  2lgslem3b1  15830  2lgslem3c1  15831  2lgs  15836  2lgsoddprmlem2  15838  2lgsoddprm  15845  2sqlem3  15849  2sqlem8  15855  2sqlem10  15857  structgrssvtx  15896  structgrssiedg  15897  ushgruhgr  15934  uhgrun  15940  incistruhgr  15944  upgrop  15958  upgruhgr  15965  umgrupgr  15966  umgrnloopv  15968  umgredgprv  15969  umgr0e  15972  upgr1edc  15975  umgr1een  15979  upgrun  15980  umgrun  15982  umgrislfupgrdom  15985  upgredg  15998  umgrpredgv  16001  usgrop  16020  usgrausgrien  16023  ausgrumgrien  16024  ausgrusgrien  16025  uspgrupgrushgr  16036  usgrumgr  16038  usgrumgruspgr  16039  usgruspgrben  16040  usgrislfuspgrdom  16044  edgssv2en  16053  usgrf1oedg  16059  usgredg4  16069  usgredg2vlem2  16077  usgredg2v  16078  ushgredgedg  16080  ushgredgedgloop  16082  usgrstrrepeen  16085  usgr0e  16086  uhgr0v0e  16088  uspgr1edc  16094  usgr1e  16095  griedg0ssusgr  16105  subgrprop3  16116  subgruhgredgdm  16124  subuhgr  16126  subupgr  16127  subumgr  16128  subusgr  16129  uhgrspansubgrlem  16130  1loopgrvd2fi  16159  1loopgrvd0fi  16160  1hevtxdg0fi  16161  vdegp1aid  16168  vdegp1bid  16169  wlkm  16193  wlkvtxiedg  16199  wlkvtxiedgg  16200  wlkeq  16208  wlk1walkdom  16213  uspgr2wlkeq  16219  uspgr2wlkeqi  16221  upgr2wlkdc  16231  wlkres  16233  trlreslem  16243  clwwlkccatlem  16254  clwwlkn1loopb  16274  clwwlkext2edg  16276  clwwlknonex2lem1  16291  clwwlknonex2  16293  trlsegvdeglem2  16315  trlsegvdeglem3  16316  eupth2lem3lem4fi  16327  eupth2lemsfi  16332  fnmptd  16421  bj-sels  16530  bj-nnelon  16575  2omap  16615  pw1map  16617  pwle2  16620  pwf1oexmid  16621  pw1nct  16625  nninfall  16632  nninfsellemdc  16633  nninfself  16636  nnnninfex  16645  nninfnfiinf  16646  refeq  16653  isomninnlem  16655  cvgcmp2nlemabs  16657  trilpolemlt1  16666  trirec0  16669  apdifflemf  16671  apdifflemr  16672  apdiff  16673  iswomninnlem  16674  iswomni0  16676  ismkvnnlem  16677  reap0  16683  cndcap  16684  gfsumval  16701  gsumgfsumlem  16704  gsumgfsum  16705  gfsumsn  16706  gfsump1  16707