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  714  pm4.55dc  947  mpbir2and  953  pm3.12dc  967  mpbir3and  1207  pm5.15dc  1434  eqeltrd  2309  eqnetrd  2436  3netr4d  2445  r19.30dc  2690  raleqtrrdv  2750  rexeqtrrdv  2751  sbcne12g  3155  eqsstrd  3273  3sstr4d  3282  eqbrtrd  4130  3brtr4d  4140  snelpwi  4326  prelpwi  4329  pwel  4333  ordelon  4503  onin  4506  elelsuc  4529  onsuc  4622  onsucb  4624  onintonm  4638  omsinds  4743  sosng  4822  relssdv  4841  eqbrrdv  4846  eqrelrdv2  4848  relsnopg  4853  breldmg  4961  elrnmptdv  5010  iss  5083  xpimasn  5210  elxp4  5249  elxp5  5250  iotam  5343  funssres  5394  f0rn0  5561  fimadmfo  5598  sefvex  5690  fdmeu  5719  fvun1  5742  eqfnfvd  5777  fvimacnvi  5791  fvimacnv  5792  fvelrn  5807  fmpt3d  5832  fmpt2d  5838  resflem  5840  fmptco  5842  fsn  5848  funopsn  5859  fncofn  5861  ftpg  5867  fconst2g  5898  funfvima3  5919  elabrexg  5930  foeqcnvco  5962  f1eqcocnv  5963  fliftfun  5968  fliftfund  5969  fliftval  5972  riota5f  6029  f1ofveu  6037  f1ocnvd  6256  f1opw2  6260  off  6278  offval2  6281  ofrfval2  6282  offveq  6286  caofref  6290  caofinvl  6291  elxp6  6362  cnvf1olem  6419  f2ndf  6421  f1od2  6430  elmpom  6433  fvn0elsupp  6450  suppfnss  6456  tposf12  6499  smores2  6524  tfrlemisucaccv  6555  tfrlemibfn  6558  tfr1onlemsucaccv  6571  tfr1onlembfn  6574  tfrcllemsucaccv  6584  tfrcllembfn  6587  tfrcl  6594  tfri3  6597  frecabcl  6629  nnsucsssuc  6724  ersym  6778  ertr  6781  swoer  6794  erth  6812  riinerm  6841  qliftfund  6851  eroprf  6861  ecopoverg  6869  th3qlem1  6870  elmapssres  6906  mapss  6925  fdiagfn  6926  ixpssmap2g  6961  mapsnf1o  6971  f1oen4g  6990  f1dom4g  6991  f1dom2g  6994  dom3d  7012  en2prd  7058  dom1oi  7069  pw2f1odclem  7086  fopwdom  7088  mapxpen  7100  nndomo  7117  dif1en  7135  findcard2  7145  findcard2s  7146  diffisn  7149  fimax2gtrilemstep  7157  eqsndc  7162  fientri3  7174  tpfidceq  7189  fiintim  7190  opabfi  7199  f1dmvrnfibi  7210  sbthlemi6  7231  0fsupp  7250  elfir  7259  fifo  7266  2omap  7268  supelti  7292  supsnti  7295  cnvinfex  7308  ordiso2  7325  updjud  7372  djudom  7383  difinfsn  7390  ctssdc  7403  enumctlemm  7404  enumct  7405  nninfninc  7413  enomnilem  7428  fodjuf  7435  ismkvnex  7445  omnimkv  7446  enmkvlem  7451  enwomnilem  7459  nninfdcinf  7461  nninfwlporlem  7463  isnumi  7477  exmidfodomrlemrALT  7505  finacn  7510  djudoml  7525  djudomr  7526  netap  7564  2omotaplemap  7567  2omotaplemst  7568  exmidapne  7570  cc2lem  7576  cc3  7578  ltsopi  7631  pitri3or  7633  ltdcpi  7634  indpi  7653  enqdc  7672  enqdc1  7673  addcmpblnq  7678  mulcanenq  7696  recrecnq  7705  nqtri3or  7707  ltdcnq  7708  ltsonq  7709  ltaddnq  7718  subhalfnqq  7725  archnqq  7728  prarloclemarch2  7730  enq0tr  7745  nqnq0  7752  addcmpblnq0  7754  mulcanenq0ec  7756  nnnq0lem1  7757  nqpnq0nq  7764  nq0m0r  7767  nq02m  7776  prarloclemlt  7804  prarloclemcalc  7813  addlocpr  7847  nqprl  7862  nqpru  7863  addnqprlemrl  7868  addnqprlemru  7869  prmuloclemcalc  7876  mullocprlem  7881  mulnqprlemrl  7884  mulnqprlemru  7885  1idprl  7901  1idpru  7902  ltaddpr  7908  ltexprlemm  7911  ltexprlemopl  7912  ltexprlemopu  7914  ltexprlemdisj  7917  ltexprlemrl  7921  ltexprlemru  7923  addcanprleml  7925  addcanprlemu  7926  addcanprg  7927  prplnqu  7931  recexprlemloc  7942  recexprlem1ssl  7944  recexprlem1ssu  7945  aptiprleml  7950  aptiprlemu  7951  archpr  7954  cauappcvgprlemm  7956  cauappcvgprlemopl  7957  cauappcvgprlemloc  7963  cauappcvgprlemladdfu  7965  cauappcvgprlemladdfl  7966  cauappcvgprlem1  7970  cauappcvgprlem2  7971  caucvgprlemnkj  7977  caucvgprlemopl  7980  caucvgprlemloc  7986  caucvgprlemladdfu  7988  caucvgprlem2  7991  caucvgprprlemnkltj  8000  caucvgprprlemopl  8008  caucvgprprlemloc  8014  caucvgprprlemexbt  8017  caucvgprprlemaddq  8019  caucvgprprlem2  8021  suplocexprlemmu  8029  suplocexprlemru  8030  suplocexprlemloc  8032  suplocexprlemlub  8035  prsrlem1  8053  0idsr  8078  1idsr  8079  recexgt0sr  8084  archsr  8093  prsradd  8097  caucvgsrlemcau  8104  caucvgsrlembound  8105  caucvgsrlemoffgt1  8110  suplocsrlemb  8117  suplocsrlempr  8118  suplocsrlem  8119  pitonnlem1p1  8157  pitonn  8159  pitoregt0  8160  peano2nnnn  8164  recidpirq  8169  axcaucvglemval  8208  leid  8353  nltled  8390  readdcan  8409  addneintrd  8457  addneintr2d  8458  pncan  8475  subsub2  8497  subsub4  8502  negned  8577  subne0d  8589  subneintrd  8624  subneintr2d  8626  subeq0bd  8648  subdi  8654  gt0add  8843  rimul  8855  rereim  8856  ltmul1a  8861  apreim  8873  apirr  8875  mulap0r  8885  msqge0  8886  mulge0  8889  gt0ap0  8896  ltap  8903  subap0d  8914  recexaplem2  8922  mulap0bad  8929  mulap0bbd  8930  mul0eqap  8940  divrecap  8958  div0ap  8972  div1  8973  recrecap  8979  divdivdivap  8983  ddcanap  8996  rerecclap  9000  div2negap  9005  diveqap1bd  9106  recgt0  9120  prodgt0  9122  lemul1a  9128  recp1lt1  9169  squeeze0  9174  peano2nn  9245  div4p1lem1div2  9488  arch  9489  peano2z  9609  peano2zm  9611  ztri3or  9616  nn0n0n1ge2  9644  zextle  9665  gtndiv  9669  suprzclex  9672  nn0ind-raph  9691  uzid  9864  uzneg  9869  uztric  9872  uz11  9873  eluzp1l  9875  qdivcl  9971  irrmul  9975  irrmulap  9976  rpnegap  10015  negelrpd  10017  ledivge1le  10055  mul2lt0rlt0  10088  mul2lt0rgt0  10089  nn0ledivnn  10096  ltpnf  10109  mnflt  10112  pnfge  10118  mnfle  10121  xrlttr  10124  xrltso  10125  xrlttri3  10126  xrleid  10129  xaddass2  10199  xltadd1  10205  xlt2add  10209  xleaddadd  10216  lincmble  10333  iccf1o  10334  fztri3or  10369  fznlem  10371  fzn  10372  fzsplit2  10380  fznatpl1  10406  uzsplit  10422  fseq1p1m1  10424  fzm1  10430  fznn0sub2  10458  difelfznle  10465  1fv  10469  fzodcel  10483  fzospliti  10508  fzouzsplit  10511  eluzgtdifelfzo  10538  exfzdc  10582  subfzo0  10584  zsupcllemstep  10585  zsupcl  10587  zssinfcl  10588  infssuzex  10589  infssuzcldc  10591  suprzubdc  10592  nninfdcex  10593  qdcle  10602  exbtwnz  10606  qbtwnrelemcalc  10611  flqlelt  10632  qfraclt1  10636  qfracge0  10637  flqltnz  10643  btwnzge0  10656  flhalf  10658  fldiv4lem1div2uz2  10662  ceiqle  10671  intfracq  10678  mulqmod0  10688  modqge0  10690  modqlt  10691  modqid  10707  modqid0  10708  m1modge3gt1  10729  modqltm1p1mod  10734  q2txmodxeq0  10742  modaddmodlo  10746  modsumfzodifsn  10754  addmodlteq  10756  frecuzrdgtcl  10770  frecuzrdgtclt  10779  uzennn  10794  uzsinds  10802  seqf  10822  seqf2  10826  monoord2  10844  iseqf1olemqk  10865  iseqf1olemjpcl  10866  iseqf1olemqpcl  10867  seq3f1olemqsumkj  10869  seq3f1olemqsum  10871  seq3f1olemstep  10872  seq3f1oleml  10874  seqf1oglem1  10877  ser3le  10895  exp3vallem  10898  exp3val  10899  expp1  10904  expcllem  10908  ltexp2a  10949  leexp2a  10950  nn0ltexp2  11067  faclbnd  11099  faclbnd2  11100  faclbnd3  11101  bcval5  11121  bcpasc  11124  hashennn  11138  fihasheqf1oi  11145  hashsng  11156  fihashfn  11159  hashun  11164  fihashss  11176  fihashssdif  11178  hashfz  11181  hashxp  11186  fimaxq  11187  sseqn  11196  hashfibclem  11199  zfz1isolem1  11205  seq3coll  11207  hashdmprop2dom  11209  wrdf  11223  wrdlenge2n0  11253  fstwrdne0  11257  wrdred1hash  11261  ccatvalfn  11282  ccatsymb  11283  ccatlid  11287  ccatrid  11288  ccatrn  11290  ccatalpha  11294  eqs1  11309  ccats1val2  11321  fzowrddc  11332  swrdlen  11337  swrdnd  11344  swrd0g  11345  swrdfv2  11348  swrdwrdsymbg  11349  pfxn0  11373  pfxwrdsymbg  11375  pfxsuff1eqwrdeq  11384  swrdswrd  11390  ccats1pfxeq  11399  ccats1pfxeqrex  11400  wrdind  11407  wrd2ind  11408  swrdccatin1  11410  pfxccatin12lem4  11411  swrdccatin2  11414  pfxccatin12  11418  pfxccat3a  11423  swrdccat3blem  11424  pfxccatid  11426  swrdccatin2d  11429  shftfn  11502  cjth  11524  cjmulrcl  11565  reim0bd  11622  rerebd  11623  cjrebd  11624  caucvgre  11659  cvg1nlemcxze  11660  cvg1nlemcau  11662  cvg1nlemres  11663  recvguniq  11673  resqrexlemover  11688  resqrexlemdec  11689  resqrexlemgt0  11698  resqrexlemoverl  11699  resqrexlemglsq  11700  rersqrtthlem  11708  sqrtgt0  11712  leabs  11752  absexpzap  11758  absle  11767  recvalap  11775  abstri  11782  abs2dif  11784  amgm2  11796  absne0d  11865  maxleim  11883  maxabslemab  11884  maxabslemlub  11885  maxltsup  11896  zmaxcl  11902  fimaxre2  11905  minmax  11908  rpmincl  11916  bdtrilem  11917  bdtri  11918  xrmaxleim  11922  xrmaxiflemcom  11927  xrmaxltsup  11936  xrmaxadd  11939  xrminmax  11943  xrminrpcl  11952  climconst  11968  climuni  11971  2clim  11979  climcn1  11986  climcn2  11987  reccn2ap  11991  climge0  12003  climle  12012  climsqz  12013  climsqz2  12014  serf0  12030  summodclem3  12059  summodclem2a  12060  fsumcl2lem  12077  sumpr  12092  sumtp  12093  fsum0diaglem  12119  mptfzshft  12121  fsumle  12142  fsumlt  12143  divcnv  12176  trireciplem  12179  expcnvap0  12181  expcnv  12183  explecnv  12184  geosergap  12185  cvgratnnlembern  12202  cvgratnnlemabsle  12206  cvgratnnlemsumlt  12207  cvgratz  12211  cvgratgt0  12212  mertenslemi1  12214  mertenslem2  12215  mertensabs  12216  clim2divap  12219  prodmodclem3  12254  prodmodclem2a  12255  fprodseq  12262  fprodmul  12270  fprodfac  12294  fprodconst  12299  fprodap0  12300  fprodap0f  12315  fprodle  12319  eftcl  12333  ef0lem  12339  efsub  12360  eftlub  12369  eflegeo  12380  tanval2ap  12392  sinadd  12415  cos2t  12429  cos2tsin  12430  sin01bnd  12436  cos01bnd  12437  eirraplem  12456  dvdsval2  12469  dvdsdc  12477  dvds0lem  12480  zdvdsdc  12491  dvdscmulr  12499  dvdsmulcr  12500  fsumdvds  12521  dvdslelemd  12522  divconjdvds  12528  dvdsext  12534  fzm1ndvds  12535  dvdsmod  12541  3dvds  12543  oexpneg  12556  2tp1odd  12563  mulsucdiv2z  12564  2teven  12566  zeo5  12567  opeo  12576  omeo  12577  nn0ob  12587  divalglemnqt  12599  bitsdc  12626  bits0o  12629  bitsfzolem  12633  bitsfzo  12634  bitsmod  12635  bitscmp  12637  bitsinv1lem  12640  gcddvds  12652  dvdslegcd  12653  gcdneg  12671  bezoutlemnewy  12685  bezoutlemstep  12686  bezoutlema  12688  bezoutlemb  12689  bezoutlemmo  12695  bezoutlemle  12697  bezoutlemsup  12698  dfgcd3  12699  bezout  12700  dfgcd2  12703  uzwodc  12726  lcmcllem  12757  lcmneg  12764  lcmgcdlem  12767  lcmdvds  12769  lcmid  12770  3lcm2e6woprm  12776  6lcm4e12  12777  ncoprmgcdne1b  12779  mulgcddvds  12784  divgcdcoprmex  12792  cncongr1  12793  cncongr2  12794  isprm2lem  12806  prmind2  12810  dvdsnprmd  12815  prm2orodd  12816  sqnprm  12826  isprm5lem  12831  rpexp  12843  sqrt2irrlem  12851  oddpwdclemdc  12863  sqrt2irraplemnn  12869  qnumdencoprm  12883  qeqnumdivden  12884  nn0gcdsq  12890  nn0sqrtelqelz  12896  nonsq  12897  phicl2  12904  phibnd  12907  hashdvds  12911  phiprmpw  12912  phimullem  12915  eulerthlemrprm  12919  eulerthlema  12920  eulerthlemth  12922  prmdiveq  12926  hashgcdlem  12928  odzdvds  12936  modprminv  12940  nnnn0modprm0  12946  modprmn0modprm0  12947  pythagtriplem10  12960  pythagtriplem19  12973  pythagtrip  12974  pcpre1  12983  pcpremul  12984  pceu  12986  pcmul  12992  pcdiv  12993  pcqmul  12994  pcqdiv  12998  pcexp  13000  pcdvdsb  13011  pcidlem  13014  pcdvdstr  13018  pcgcd1  13019  pc2dvds  13021  pcprmpw2  13024  difsqpwdvds  13029  pcaddlem  13030  pcadd  13031  pcadd2  13032  pcmpt  13034  pcmptdvds  13036  pcprod  13037  fldivp1  13039  pcfaclem  13040  pcfac  13041  pcbc  13042  qexpz  13043  pockthlem  13047  pockthg  13048  1arithlem4  13057  1arith  13058  1arith2  13059  4sqlem6  13074  4sqlem8  13076  4sqlem9  13077  4sqlem10  13078  4sqexercise1  13089  4sqexercise2  13090  4sqlemsdc  13091  4sqlem11  13092  4sqlem12  13093  4sqlem15  13096  4sqlem16  13097  4sqlem17  13098  znnen  13138  ennnfonelemk  13140  ennnfonelemkh  13152  ennnfonelemhf1o  13153  ennnfonelemrnh  13156  ennnfonelemfun  13157  ennnfonelemf1  13158  ennnfonelemrn  13159  ennnfonelemnn0  13162  ctinfomlemom  13167  ctiunctlemudc  13177  unct  13182  omctfn  13183  ssnnctlemct  13186  nninfdclemp1  13190  nninfdc  13193  structfung  13218  setsfun  13236  setsfun0  13237  setscom  13241  strslfv3  13247  setsslid  13252  pwsdiagel  13499  pwssnf1o  13500  imasaddfnlemg  13516  imasaddvallemg  13517  mgmsscl  13563  plusffng  13567  mgmplusf  13568  mgm0  13571  mgm1  13572  opifismgmdc  13573  gsumfzval  13593  gsumprval  13601  sgrp1  13613  issgrpd  13614  prdsplusgsgrpcl  13616  mndpfo  13640  mndfo  13641  prdsplusgcl  13648  prdsidlem  13649  mnd1  13657  0subm  13686  mhmima  13693  grpinvfng  13746  isgrpinv  13756  grpinvid  13762  grpinvf1o  13772  grpinvadd  13780  grpsubf  13781  grpsubsub4  13795  grplactcnv  13804  grp1  13808  grp1inv  13809  prdsinvlem  13810  prdsinvgd  13812  qusgrp2  13819  mulgfng  13830  subginv  13887  resgrpisgrp  13901  subgintm  13904  0subg  13905  0nsg  13920  qusinv  13942  ghminv  13956  ghmrn  13963  ghmeql  13973  ghmnsgima  13974  kerf1ghm  13980  conjnmz  13985  rngass  14072  rngmneg1  14080  rngmneg2  14081  qusrng  14091  srgideu  14105  srgidmlem  14111  srgpcomp  14123  srg1expzeq1  14128  ringcl  14146  ringideu  14150  ringidmlem  14155  ringnegl  14184  ringnegr  14185  ring1  14192  qusring2  14199  opprringbg  14213  dvdsrd  14228  dvdsr01  14238  isunitd  14240  unitinvcl  14257  unitinvinv  14258  unitnegcl  14264  rhmmul  14298  rhmf1o  14302  nzrunit  14322  lringuplu  14330  subrngintm  14346  subrgsubm  14368  subrgintm  14377  rrgsupp  14400  aprsym  14419  scaffng  14444  lmodscaf  14445  lsssn0  14505  lss1d  14518  lssintclm  14519  lspval  14525  lspcl  14526  lspsnid  14542  lspprid1  14546  lspsn  14551  sraval  14572  rspcl  14626  rspssid  14627  rspssp  14629  rnglidlmmgm  14631  rnglidlmsgrp  14632  cnfldneg  14708  zringinvg  14739  expghmap  14742  znzrhfo  14783  znf1o  14786  znhash  14791  znidomb  14793  znrrg  14795  psrbagfsupp  14806  psrbagfi  14810  psrbaglecl  14811  psrbagaddclfi  14812  psrbagcon  14813  psraddcl  14822  psr0cl  14823  psrnegcl  14825  psrneg  14829  psr1clfi  14830  mplsubgfilemm  14840  mplsubgfilemcl  14841  baspartn  14902  eltg3i  14908  tgclb  14917  topbas  14919  2basgeng  14934  topcld  14961  0cld  14964  uncld  14965  neif  14993  elnei  15004  0nei  15018  restbasg  15020  iscnp4  15070  cnpnei  15071  cnclima  15075  cncnp  15082  cnrest2r  15089  cndis  15093  lmff  15101  lmtopcnp  15102  txbas  15110  txopn  15117  txcnp  15123  upxp  15124  txdis1cn  15130  cnmpt11  15135  cnmpt21  15143  psmetge0  15183  xmetge0  15217  xmettpos  15222  xmetrtri  15228  metrtri  15229  xblpnfps  15250  xblpnf  15251  blfps  15261  blf  15262  ssblps  15277  ssbl  15278  blbas  15285  metss2  15350  xmettxlem  15361  xmettx  15362  qtopbas  15374  divcnap  15417  cncfss  15435  cdivcncfap  15456  expcncf  15461  cnopnap  15463  maxcncf  15467  mincncf  15468  dedekindeulemuub  15469  dedekindeulemlu  15473  dedekindeu  15475  suplociccex  15477  dedekindicclemuub  15478  dedekindicclemlu  15482  dedekindicclemicc  15484  ivthinclemlopn  15488  ivthinclemuopn  15490  ivthinc  15495  ivthreinc  15497  hoverlt1  15501  ellimc3apf  15512  limcimolemlt  15516  limcimo  15517  limcresi  15518  cnplimclemle  15520  reldvg  15531  dvfgg  15540  dvidlemap  15543  dvidrelem  15544  dvidsslem  15545  dvcjbr  15560  dvcj  15561  dvrecap  15565  dveflem  15578  dvef  15579  elply2  15587  elplyr  15592  plycj  15613  plyreres  15616  reeff1oleme  15624  pilem3  15635  sinq34lt0t  15683  cosq14gt0  15684  coseq0q4123  15686  tangtx  15690  sincosq1eq  15691  cosordlem  15701  logdivlti  15733  relogbval  15803  relogbzcl  15804  nnlogbexp  15811  logbgcd1irr  15819  logbgcd1irraplemexp  15820  logbgcd1irraplemap  15821  pellexlem1  15832  pellexlem3  15834  wilthlem1  15835  mpodvdsmulf1o  15845  mersenne  15852  perfectlem2  15855  perfect  15856  zabsle1  15859  lgslem1  15860  lgsval  15864  lgsfvalg  15865  lgsfcl2  15866  lgsval2lem  15870  lgscl1  15883  lgsmod  15886  lgsdir2lem5  15892  lgsdir2  15893  lgsdilem2  15896  lgsdi  15897  lgsne0  15898  gausslemma2dlem0c  15911  gausslemma2dlem0h  15916  gausslemma2dlem1a  15918  gausslemma2dlem1f1o  15920  gausslemma2dlem3  15923  lgseisenlem1  15930  lgseisenlem2  15931  lgseisenlem3  15932  lgseisenlem4  15933  lgseisen  15934  lgsquadlem1  15937  lgsquadlem2  15938  lgsquadlem3  15939  lgsquad3  15944  2lgslem3b1  15958  2lgslem3c1  15959  2lgs  15964  2lgsoddprmlem2  15966  2lgsoddprm  15973  2sqlem3  15977  2sqlem8  15983  2sqlem10  15985  structgrssvtx  16024  structgrssiedg  16025  ushgruhgr  16062  uhgrun  16068  incistruhgr  16072  upgrop  16086  upgruhgr  16093  umgrupgr  16094  umgrnloopv  16096  umgredgprv  16097  umgr0e  16100  upgr1edc  16103  umgr1een  16107  upgrun  16108  umgrun  16110  umgrislfupgrdom  16113  upgredg  16126  umgrpredgv  16129  usgrop  16148  usgrausgrien  16151  ausgrumgrien  16152  ausgrusgrien  16153  uspgrupgrushgr  16164  usgrumgr  16166  usgrumgruspgr  16167  usgruspgrben  16168  usgrislfuspgrdom  16172  edgssv2en  16181  usgrf1oedg  16187  usgredg4  16197  usgredg2vlem2  16205  usgredg2v  16206  ushgredgedg  16208  ushgredgedgloop  16210  usgrstrrepeen  16213  usgr0e  16214  uhgr0v0e  16216  uspgr1edc  16222  usgr1e  16223  griedg0ssusgr  16233  subgrprop3  16244  subgruhgredgdm  16252  subuhgr  16254  subupgr  16255  subumgr  16256  subusgr  16257  uhgrspansubgrlem  16258  1loopgrvd2fi  16287  1loopgrvd0fi  16288  1hevtxdg0fi  16289  vdegp1aid  16296  vdegp1bid  16297  wlkm  16321  wlkvtxiedg  16327  wlkvtxiedgg  16328  wlkeq  16336  wlk1walkdom  16341  uspgr2wlkeq  16347  uspgr2wlkeqi  16349  upgr2wlkdc  16359  wlkres  16361  trlreslem  16371  clwwlkccatlem  16382  clwwlkn1loopb  16402  clwwlkext2edg  16404  clwwlknonex2lem1  16419  clwwlknonex2  16421  trlsegvdeglem2  16443  trlsegvdeglem3  16444  eupth2lem3lem4fi  16455  eupth2lemsfi  16460  fnmptd  16563  bj-sels  16671  bj-nnelon  16716  pw1map  16756  pwle2  16759  pwf1oexmid  16760  pw1nct  16764  nninfall  16774  nninfsellemdc  16775  nninfself  16778  nnnninfex  16787  nninfnfiinf  16788  refeq  16795  isomninnlem  16801  cvgcmp2nlemabs  16803  trilpolemlt1  16812  trirec0  16815  apdifflemf  16817  apdifflemr  16818  apdiff  16819  qdiff  16820  iswomninnlem  16821  iswomni0  16823  ismkvnnlem  16824  reap0  16830  cndcap  16831  gfsumval  16848  gsumgfsumlem  16851  gsumgfsum  16852  gfsumsn  16853  gfsump1  16854