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  2311  eqnetrd  2438  3netr4d  2447  r19.30dc  2692  raleqtrrdv  2753  rexeqtrrdv  2754  sbcne12g  3158  eqsstrd  3276  3sstr4d  3285  eqbrtrd  4133  3brtr4d  4143  snelpwi  4329  prelpwi  4332  pwel  4336  ordelon  4506  onin  4509  elelsuc  4532  onsuc  4625  onsucb  4627  onintonm  4641  omsinds  4746  sosng  4825  relssdv  4844  eqbrrdv  4849  eqrelrdv2  4851  relsnopg  4856  breldmg  4964  elrnmptdv  5013  iss  5086  xpimasn  5213  elxp4  5252  elxp5  5253  iotam  5346  funssres  5397  f0rn0  5564  fimadmfo  5601  sefvex  5693  fdmeu  5722  fvun1  5745  eqfnfvd  5780  fvimacnvi  5794  fvimacnv  5795  fvelrn  5810  fmpt3d  5835  fmpt2d  5841  resflem  5843  fmptco  5845  fsn  5851  funopsn  5862  fncofn  5864  ftpg  5870  fconst2g  5901  funfvima3  5922  elabrexg  5933  foeqcnvco  5965  f1eqcocnv  5966  fliftfun  5971  fliftfund  5972  fliftval  5975  riota5f  6032  f1ofveu  6040  f1ocnvd  6259  f1opw2  6263  off  6281  offval2  6284  ofrfval2  6285  offveq  6289  caofref  6293  caofinvl  6294  elxp6  6365  cnvf1olem  6422  f2ndf  6424  f1od2  6433  elmpom  6436  fvn0elsupp  6453  suppfnss  6459  tposf12  6502  smores2  6527  tfrlemisucaccv  6558  tfrlemibfn  6561  tfr1onlemsucaccv  6574  tfr1onlembfn  6577  tfrcllemsucaccv  6587  tfrcllembfn  6590  tfrcl  6597  tfri3  6600  frecabcl  6632  nnsucsssuc  6727  ersym  6781  ertr  6784  swoer  6797  erth  6815  riinerm  6844  qliftfund  6854  eroprf  6864  ecopoverg  6872  th3qlem1  6873  elmapssres  6909  mapss  6928  fdiagfn  6929  ixpssmap2g  6964  mapsnf1o  6974  f1oen4g  6993  f1dom4g  6994  f1dom2g  6997  dom3d  7015  en2prd  7061  dom1oi  7072  pw2f1odclem  7089  fopwdom  7091  mapxpen  7103  nndomo  7120  dif1en  7138  findcard2  7148  findcard2s  7149  diffisn  7152  fimax2gtrilemstep  7160  eqsndc  7165  fientri3  7177  tpfidceq  7192  fiintim  7193  opabfi  7202  f1dmvrnfibi  7213  sbthlemi6  7234  0fsupp  7253  elfir  7262  fifo  7269  2omap  7271  supelti  7295  supsnti  7298  cnvinfex  7311  ordiso2  7328  updjud  7375  djudom  7386  difinfsn  7393  ctssdc  7406  enumctlemm  7407  enumct  7408  nninfninc  7416  enomnilem  7431  fodjuf  7438  ismkvnex  7448  omnimkv  7449  enmkvlem  7454  enwomnilem  7462  nninfdcinf  7464  nninfwlporlem  7466  isnumi  7480  exmidfodomrlemrALT  7508  finacn  7513  djudoml  7528  djudomr  7529  netap  7573  2omotaplemap  7576  2omotaplemst  7577  exmidapne  7579  cc2lem  7585  cc3  7587  ltsopi  7640  pitri3or  7642  ltdcpi  7643  indpi  7662  enqdc  7681  enqdc1  7682  addcmpblnq  7687  mulcanenq  7705  recrecnq  7714  nqtri3or  7716  ltdcnq  7717  ltsonq  7718  ltaddnq  7727  subhalfnqq  7734  archnqq  7737  prarloclemarch2  7739  enq0tr  7754  nqnq0  7761  addcmpblnq0  7763  mulcanenq0ec  7765  nnnq0lem1  7766  nqpnq0nq  7773  nq0m0r  7776  nq02m  7785  prarloclemlt  7813  prarloclemcalc  7822  addlocpr  7856  nqprl  7871  nqpru  7872  addnqprlemrl  7877  addnqprlemru  7878  prmuloclemcalc  7885  mullocprlem  7890  mulnqprlemrl  7893  mulnqprlemru  7894  1idprl  7910  1idpru  7911  ltaddpr  7917  ltexprlemm  7920  ltexprlemopl  7921  ltexprlemopu  7923  ltexprlemdisj  7926  ltexprlemrl  7930  ltexprlemru  7932  addcanprleml  7934  addcanprlemu  7935  addcanprg  7936  prplnqu  7940  recexprlemloc  7951  recexprlem1ssl  7953  recexprlem1ssu  7954  aptiprleml  7959  aptiprlemu  7960  archpr  7963  cauappcvgprlemm  7965  cauappcvgprlemopl  7966  cauappcvgprlemloc  7972  cauappcvgprlemladdfu  7974  cauappcvgprlemladdfl  7975  cauappcvgprlem1  7979  cauappcvgprlem2  7980  caucvgprlemnkj  7986  caucvgprlemopl  7989  caucvgprlemloc  7995  caucvgprlemladdfu  7997  caucvgprlem2  8000  caucvgprprlemnkltj  8009  caucvgprprlemopl  8017  caucvgprprlemloc  8023  caucvgprprlemexbt  8026  caucvgprprlemaddq  8028  caucvgprprlem2  8030  suplocexprlemmu  8038  suplocexprlemru  8039  suplocexprlemloc  8041  suplocexprlemlub  8044  prsrlem1  8062  0idsr  8087  1idsr  8088  recexgt0sr  8093  archsr  8102  prsradd  8106  caucvgsrlemcau  8113  caucvgsrlembound  8114  caucvgsrlemoffgt1  8119  suplocsrlemb  8126  suplocsrlempr  8127  suplocsrlem  8128  pitonnlem1p1  8166  pitonn  8168  pitoregt0  8169  peano2nnnn  8173  recidpirq  8178  axcaucvglemval  8217  leid  8362  nltled  8399  readdcan  8418  addneintrd  8466  addneintr2d  8467  pncan  8484  subsub2  8506  subsub4  8511  negned  8586  subne0d  8598  subneintrd  8633  subneintr2d  8635  subeq0bd  8657  subdi  8663  gt0add  8852  rimul  8864  rereim  8865  ltmul1a  8870  apreim  8882  apirr  8884  mulap0r  8894  msqge0  8895  mulge0  8898  gt0ap0  8905  ltap  8912  subap0d  8923  recexaplem2  8931  mulap0bad  8938  mulap0bbd  8939  mul0eqap  8949  divrecap  8967  div0ap  8981  div1  8982  recrecap  8988  divdivdivap  8992  ddcanap  9005  rerecclap  9009  div2negap  9014  diveqap1bd  9115  recgt0  9129  prodgt0  9131  lemul1a  9137  recp1lt1  9178  squeeze0  9183  peano2nn  9254  div4p1lem1div2  9497  arch  9498  peano2z  9618  peano2zm  9620  ztri3or  9625  nn0n0n1ge2  9653  zextle  9675  gtndiv  9679  suprzclex  9682  nn0ind-raph  9701  uzid  9874  uzneg  9879  uztric  9882  uz11  9883  eluzp1l  9885  qdivcl  9981  irrmul  9985  irrmulap  9986  rpnegap  10025  negelrpd  10027  ledivge1le  10065  mul2lt0rlt0  10098  mul2lt0rgt0  10099  nn0ledivnn  10106  ltpnf  10119  mnflt  10122  pnfge  10128  mnfle  10131  xrlttr  10134  xrltso  10135  xrlttri3  10136  xrleid  10139  xaddass2  10209  xltadd1  10215  xlt2add  10219  xleaddadd  10226  lincmble  10343  iccf1o  10344  fztri3or  10379  fznlem  10381  fzn  10382  fzsplit2  10390  fznatpl1  10417  uzsplit  10433  fseq1p1m1  10435  fzm1  10441  fznn0sub2  10469  difelfznle  10476  1fv  10480  fzodcel  10494  fzospliti  10519  fzouzsplit  10522  eluzgtdifelfzo  10549  exfzdc  10593  subfzo0  10595  zsupcllemstep  10596  zsupcl  10598  zssinfcl  10599  infssuzex  10600  infssuzcldc  10602  suprzubdc  10603  nninfdcex  10604  qdcle  10613  exbtwnz  10617  qbtwnrelemcalc  10622  flqlelt  10643  qfraclt1  10647  qfracge0  10648  flqltnz  10654  btwnzge0  10667  flhalf  10669  fldiv4lem1div2uz2  10673  ceiqle  10682  intfracq  10689  mulqmod0  10699  modqge0  10701  modqlt  10702  modqid  10718  modqid0  10719  m1modge3gt1  10740  modqltm1p1mod  10745  q2txmodxeq0  10753  modaddmodlo  10757  modsumfzodifsn  10765  addmodlteq  10767  frecuzrdgtcl  10781  frecuzrdgtclt  10790  uzennn  10805  uzsinds  10813  seqf  10833  seqf2  10837  monoord2  10855  iseqf1olemqk  10876  iseqf1olemjpcl  10877  iseqf1olemqpcl  10878  seq3f1olemqsumkj  10880  seq3f1olemqsum  10882  seq3f1olemstep  10883  seq3f1oleml  10885  seqf1oglem1  10888  ser3le  10906  exp3vallem  10909  exp3val  10910  expp1  10915  expcllem  10919  ltexp2a  10960  leexp2a  10961  resq01  11027  nn0ltexp2  11079  faclbnd  11111  faclbnd2  11112  faclbnd3  11113  bcval5  11133  bcpasc  11136  bcm1n  11139  hashennn  11151  fihasheqf1oi  11158  hashsng  11169  fihashfn  11172  hashun  11177  fihashss  11189  fihashssdif  11191  hashfz  11194  hashxp  11199  hashmap  11200  hashpwfi  11201  fimaxq  11202  sseqn  11211  hashfibclem  11214  zfz1isolem1  11220  seq3coll  11222  hashdmprop2dom  11224  wrdf  11238  wrdlenge2n0  11268  fstwrdne0  11272  wrdred1hash  11276  ccatvalfn  11297  ccatsymb  11298  ccatlid  11302  ccatrid  11303  ccatrn  11305  ccatalpha  11309  eqs1  11324  ccats1val2  11336  fzowrddc  11347  swrdlen  11352  swrdnd  11359  swrd0g  11360  swrdfv2  11363  swrdwrdsymbg  11364  pfxn0  11388  pfxwrdsymbg  11390  pfxsuff1eqwrdeq  11399  swrdswrd  11405  ccats1pfxeq  11414  ccats1pfxeqrex  11415  wrdind  11422  wrd2ind  11423  swrdccatin1  11425  pfxccatin12lem4  11426  swrdccatin2  11429  pfxccatin12  11433  pfxccat3a  11438  swrdccat3blem  11439  pfxccatid  11441  swrdccatin2d  11444  shftfn  11517  cjth  11539  cjmulrcl  11580  reim0bd  11637  rerebd  11638  cjrebd  11639  caucvgre  11674  cvg1nlemcxze  11675  cvg1nlemcau  11677  cvg1nlemres  11678  recvguniq  11688  resqrexlemover  11703  resqrexlemdec  11704  resqrexlemgt0  11713  resqrexlemoverl  11714  resqrexlemglsq  11715  rersqrtthlem  11723  sqrtgt0  11727  leabs  11767  absexpzap  11773  absle  11782  recvalap  11790  abstri  11797  abs2dif  11799  amgm2  11811  absne0d  11880  maxleim  11898  maxabslemab  11899  maxabslemlub  11900  maxltsup  11911  zmaxcl  11917  fimaxre2  11920  minmax  11923  rpmincl  11931  bdtrilem  11932  bdtri  11933  xrmaxleim  11937  xrmaxiflemcom  11942  xrmaxltsup  11951  xrmaxadd  11954  xrminmax  11958  xrminrpcl  11967  climconst  11983  climuni  11986  2clim  11994  climcn1  12001  climcn2  12002  reccn2ap  12006  climge0  12018  climle  12027  climsqz  12028  climsqz2  12029  serf0  12045  summodclem3  12074  summodclem2a  12075  fsumcl2lem  12092  sumpr  12107  sumtp  12108  fsum0diaglem  12134  mptfzshft  12136  fsumle  12157  fsumlt  12158  divcnv  12191  trireciplem  12194  expcnvap0  12196  expcnv  12198  explecnv  12199  geosergap  12200  cvgratnnlembern  12217  cvgratnnlemabsle  12221  cvgratnnlemsumlt  12222  cvgratz  12226  cvgratgt0  12227  mertenslemi1  12229  mertenslem2  12230  mertensabs  12231  clim2divap  12234  prodmodclem3  12269  prodmodclem2a  12270  fprodseq  12277  fprodmul  12285  fprodfac  12309  fprodconst  12314  fprodap0  12315  fprodap0f  12330  fprodle  12334  eftcl  12348  ef0lem  12354  efsub  12375  eftlub  12384  eflegeo  12395  tanval2ap  12407  sinadd  12430  cos2t  12444  cos2tsin  12445  sin01bnd  12451  cos01bnd  12452  eirraplem  12471  dvdsval2  12484  dvdsdc  12492  dvds0lem  12495  zdvdsdc  12506  dvdscmulr  12514  dvdsmulcr  12515  fsumdvds  12536  dvdslelemd  12537  divconjdvds  12543  dvdsext  12549  fzm1ndvds  12550  dvdsmod  12556  3dvds  12558  oexpneg  12571  2tp1odd  12578  mulsucdiv2z  12579  2teven  12581  zeo5  12582  opeo  12591  omeo  12592  nn0ob  12602  divalglemnqt  12614  bitsdc  12641  bits0o  12644  bitsfzolem  12648  bitsfzo  12649  bitsmod  12650  bitscmp  12652  bitsinv1lem  12655  gcddvds  12667  dvdslegcd  12668  gcdneg  12686  bezoutlemnewy  12700  bezoutlemstep  12701  bezoutlema  12703  bezoutlemb  12704  bezoutlemmo  12710  bezoutlemle  12712  bezoutlemsup  12713  dfgcd3  12714  bezout  12715  dfgcd2  12718  uzwodc  12741  lcmcllem  12772  lcmneg  12779  lcmgcdlem  12782  lcmdvds  12784  lcmid  12785  3lcm2e6woprm  12791  6lcm4e12  12792  ncoprmgcdne1b  12794  mulgcddvds  12799  divgcdcoprmex  12807  cncongr1  12808  cncongr2  12809  isprm2lem  12821  prmind2  12825  dvdsnprmd  12830  prm2orodd  12831  sqnprm  12841  isprm5lem  12846  rpexp  12858  sqrt2irrlem  12866  oddpwdclemdc  12878  sqrt2irraplemnn  12884  qnumdencoprm  12898  qeqnumdivden  12899  nn0gcdsq  12905  nn0sqrtelqelz  12911  nonsq  12912  phicl2  12919  phibnd  12922  hashdvds  12926  phiprmpw  12927  phimullem  12930  eulerthlemrprm  12934  eulerthlema  12935  eulerthlemth  12937  prmdiveq  12941  hashgcdlem  12943  odzdvds  12951  modprminv  12955  nnnn0modprm0  12961  modprmn0modprm0  12962  pythagtriplem10  12975  pythagtriplem19  12988  pythagtrip  12989  pcpre1  12998  pcpremul  12999  pceu  13001  pcmul  13007  pcdiv  13008  pcqmul  13009  pcqdiv  13013  pcexp  13015  pcdvdsb  13026  pcidlem  13029  pcdvdstr  13033  pcgcd1  13034  pc2dvds  13036  pcprmpw2  13039  difsqpwdvds  13044  pcaddlem  13045  pcadd  13046  pcadd2  13047  pcmpt  13049  pcmptdvds  13051  pcprod  13052  fldivp1  13054  pcfaclem  13055  pcfac  13056  pcbc  13057  qexpz  13058  pockthlem  13062  pockthg  13063  1arithlem4  13072  1arith  13073  1arith2  13074  4sqlem6  13089  4sqlem8  13091  4sqlem9  13092  4sqlem10  13093  4sqexercise1  13104  4sqexercise2  13105  4sqlemsdc  13106  4sqlem11  13107  4sqlem12  13108  4sqlem15  13111  4sqlem16  13112  4sqlem17  13113  ballotfilemfc0  13157  ballotfilemfcc  13158  znnen  13170  ennnfonelemk  13172  ennnfonelemkh  13184  ennnfonelemhf1o  13185  ennnfonelemrnh  13188  ennnfonelemfun  13189  ennnfonelemf1  13190  ennnfonelemrn  13191  ennnfonelemnn0  13194  ctinfomlemom  13199  ctiunctlemudc  13209  unct  13214  omctfn  13215  ssnnctlemct  13218  nninfdclemp1  13222  nninfdc  13225  structfung  13250  setsfun  13268  setsfun0  13269  setscom  13273  strslfv3  13279  setsslid  13284  pwsdiagel  13531  pwssnf1o  13532  imasaddfnlemg  13548  imasaddvallemg  13549  mgmsscl  13595  plusffng  13599  mgmplusf  13600  mgm0  13603  mgm1  13604  opifismgmdc  13605  gsumfzval  13625  gsumprval  13633  sgrp1  13645  issgrpd  13646  prdsplusgsgrpcl  13648  mndpfo  13672  mndfo  13673  prdsplusgcl  13680  prdsidlem  13681  mnd1  13689  0subm  13718  mhmima  13725  grpinvfng  13778  isgrpinv  13788  grpinvid  13794  grpinvf1o  13804  grpinvadd  13812  grpsubf  13813  grpsubsub4  13827  grplactcnv  13836  grp1  13840  grp1inv  13841  prdsinvlem  13842  prdsinvgd  13844  qusgrp2  13851  mulgfng  13862  subginv  13919  resgrpisgrp  13933  subgintm  13936  0subg  13937  0nsg  13952  qusinv  13974  ghminv  13988  ghmrn  13995  ghmeql  14005  ghmnsgima  14006  kerf1ghm  14012  conjnmz  14017  rngass  14104  rngmneg1  14112  rngmneg2  14113  qusrng  14123  srgideu  14137  srgidmlem  14143  srgpcomp  14155  srg1expzeq1  14160  ringcl  14178  ringideu  14182  ringidmlem  14187  ringnegl  14216  ringnegr  14217  ring1  14224  qusring2  14231  opprringbg  14245  dvdsrd  14261  dvdsr01  14271  isunitd  14273  unitinvcl  14290  unitinvinv  14291  unitnegcl  14297  rhmmul  14331  rhmf1o  14335  nzrunit  14355  lringuplu  14363  subrngintm  14380  subrgsubm  14402  subrgintm  14411  rrgsupp  14434  ringunitap  14453  aprsym  14456  aprnzr  14459  aprlring  14460  drnglring  14467  drngunitap  14468  scaffng  14506  lmodscaf  14507  lsssn0  14567  lss1d  14580  lssintclm  14581  lspval  14587  lspcl  14588  lspsnid  14604  lspprid1  14608  lspsn  14613  sraval  14634  rspcl  14688  rspssid  14689  rspssp  14691  rnglidlmmgm  14693  rnglidlmsgrp  14694  cnfldneg  14770  zringinvg  14801  expghmap  14804  znzrhfo  14845  znf1o  14848  znhash  14853  znidomb  14855  znrrg  14857  psrbagfsupp  14868  psrbagfi  14872  psrbaglecl  14873  psrbagaddclfi  14874  psrbagcon  14875  psraddcl  14884  psr0cl  14885  psrnegcl  14887  psrneg  14891  psr1clfi  14892  mplsubgfilemm  14902  mplsubgfilemcl  14903  baspartn  14964  eltg3i  14970  tgclb  14979  topbas  14981  2basgeng  14996  topcld  15023  0cld  15026  uncld  15027  neif  15055  elnei  15066  0nei  15080  restbasg  15082  iscnp4  15132  cnpnei  15133  cnclima  15137  cncnp  15144  cnrest2r  15151  cndis  15155  lmff  15163  lmtopcnp  15164  txbas  15172  txopn  15179  txcnp  15185  upxp  15186  txdis1cn  15192  cnmpt11  15197  cnmpt21  15205  psmetge0  15245  xmetge0  15279  xmettpos  15284  xmetrtri  15290  metrtri  15291  xblpnfps  15312  xblpnf  15313  blfps  15323  blf  15324  ssblps  15339  ssbl  15340  blbas  15347  metss2  15412  xmettxlem  15423  xmettx  15424  qtopbas  15436  divcnap  15479  cncfss  15497  cdivcncfap  15518  expcncf  15523  cnopnap  15525  maxcncf  15529  mincncf  15530  dedekindeulemuub  15531  dedekindeulemlu  15535  dedekindeu  15537  suplociccex  15539  dedekindicclemuub  15540  dedekindicclemlu  15544  dedekindicclemicc  15546  ivthinclemlopn  15550  ivthinclemuopn  15552  ivthinc  15557  ivthreinc  15559  hoverlt1  15563  ellimc3apf  15574  limcimolemlt  15578  limcimo  15579  limcresi  15580  cnplimclemle  15582  reldvg  15593  dvfgg  15602  dvidlemap  15605  dvidrelem  15606  dvidsslem  15607  dvcjbr  15622  dvcj  15623  dvrecap  15627  dveflem  15640  dvef  15641  elply2  15649  elplyr  15654  plycj  15675  plyreres  15678  reeff1oleme  15686  pilem3  15697  sinq34lt0t  15745  cosq14gt0  15746  coseq0q4123  15748  tangtx  15752  sincosq1eq  15753  cosordlem  15763  logdivlti  15795  relogbval  15865  relogbzcl  15866  nnlogbexp  15873  logbgcd1irr  15881  logbgcd1irraplemexp  15882  logbgcd1irraplemap  15883  pellexlem1  15894  pellexlem3  15896  wilthlem1  15897  mpodvdsmulf1o  15907  mersenne  15914  perfectlem2  15917  perfect  15918  zabsle1  15921  lgslem1  15922  lgsval  15926  lgsfvalg  15927  lgsfcl2  15928  lgsval2lem  15932  lgscl1  15945  lgsmod  15948  lgsdir2lem5  15954  lgsdir2  15955  lgsdilem2  15958  lgsdi  15959  lgsne0  15960  gausslemma2dlem0c  15973  gausslemma2dlem0h  15978  gausslemma2dlem1a  15980  gausslemma2dlem1f1o  15982  gausslemma2dlem3  15985  lgseisenlem1  15992  lgseisenlem2  15993  lgseisenlem3  15994  lgseisenlem4  15995  lgseisen  15996  lgsquadlem1  15999  lgsquadlem2  16000  lgsquadlem3  16001  lgsquad3  16006  2lgslem3b1  16020  2lgslem3c1  16021  2lgs  16026  2lgsoddprmlem2  16028  2lgsoddprm  16035  2sqlem3  16039  2sqlem8  16045  2sqlem10  16047  structgrssvtx  16086  structgrssiedg  16087  ushgruhgr  16124  uhgrun  16130  incistruhgr  16134  upgrop  16148  upgruhgr  16155  umgrupgr  16156  umgrnloopv  16158  umgredgprv  16159  umgr0e  16162  upgr1edc  16165  umgr1een  16169  upgrun  16170  umgrun  16172  umgrislfupgrdom  16175  upgredg  16188  umgrpredgv  16191  usgrop  16210  usgrausgrien  16213  ausgrumgrien  16214  ausgrusgrien  16215  uspgrupgrushgr  16226  usgrumgr  16228  usgrumgruspgr  16229  usgruspgrben  16230  usgrislfuspgrdom  16234  edgssv2en  16243  usgrf1oedg  16249  usgredg4  16259  usgredg2vlem2  16267  usgredg2v  16268  ushgredgedg  16270  ushgredgedgloop  16272  usgrstrrepeen  16275  usgr0e  16276  uhgr0v0e  16278  uspgr1edc  16284  usgr1e  16285  griedg0ssusgr  16295  subgrprop3  16306  subgruhgredgdm  16314  subuhgr  16316  subupgr  16317  subumgr  16318  subusgr  16319  uhgrspansubgrlem  16320  1loopgrvd2fi  16349  1loopgrvd0fi  16350  1hevtxdg0fi  16351  vdegp1aid  16358  vdegp1bid  16359  wlkm  16383  wlkvtxiedg  16389  wlkvtxiedgg  16390  wlkeq  16398  wlk1walkdom  16403  uspgr2wlkeq  16409  uspgr2wlkeqi  16411  upgr2wlkdc  16421  wlkres  16423  trlreslem  16433  clwwlkccatlem  16444  clwwlkn1loopb  16464  clwwlkext2edg  16466  clwwlknonex2lem1  16481  clwwlknonex2  16483  trlsegvdeglem2  16505  trlsegvdeglem3  16506  eupth2lem3lem4fi  16517  eupth2lemsfi  16522  fnmptd  16625  bj-sels  16733  bj-nnelon  16778  pw1map  16818  pwle2  16821  pwf1oexmid  16822  pw1nct  16826  nninfall  16836  nninfsellemdc  16837  nninfself  16840  nnnninfex  16849  nninfnfiinf  16850  refeq  16857  isomninnlem  16863  cvgcmp2nlemabs  16865  trilpolemlt1  16874  trirec0  16877  apdifflemf  16879  apdifflemr  16880  apdiff  16881  qdiff  16882  iswomninnlem  16883  iswomni0  16885  ismkvnnlem  16886  reap0  16892  cndcap  16893  trimul0or  16894  gfsumval  16911  gsumgfsumlem  16914  gsumgfsum  16915  gfsumsn  16916  gfsump1  16917