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  718  pm4.55dc  951  mpbir2and  957  pm3.12dc  971  mpbir3and  1211  pm5.15dc  1438  eqeltrd  2315  eqnetrd  2444  3netr4d  2453  r19.30dc  2698  raleqtrrdv  2759  rexeqtrrdv  2760  sbcne12g  3165  eqsstrd  3284  3sstr4d  3293  ifeqeqxdc  3684  eqbrtrd  4147  3brtr4d  4157  snelpwi  4346  prelpwi  4349  pwel  4353  ordelon  4523  onin  4526  elelsuc  4549  onsuc  4643  onsucb  4645  onintonm  4659  omsinds  4764  sosng  4843  relssdv  4862  eqbrrdv  4867  eqrelrdv2  4869  relsnopg  4874  breldmg  4982  elrnmptdv  5031  iss  5104  xpimasn  5231  elxp4  5270  elxp5  5271  iotam  5364  funssres  5415  f0rn0  5582  fimadmfo  5619  sefvex  5711  fdmeu  5740  fvun1  5763  eqfnfvd  5800  fvimacnvi  5814  fvimacnv  5815  fvelrn  5830  fmpt3d  5855  fmpt2d  5861  resflem  5863  fmptco  5865  fsn  5871  funopsn  5882  fncofn  5884  ftpg  5890  fconst2g  5921  funfvima3  5942  elabrexg  5954  foeqcnvco  5986  f1eqcocnv  5987  fliftfun  5992  fliftfund  5993  fliftval  5996  riota5f  6055  f1ofveu  6063  f1ocnvd  6282  f1opw2  6286  f1o3d  6288  off  6305  offval2  6308  ofrfval2  6309  offveq  6313  caofref  6317  caofinvl  6318  elxp6  6393  cnvf1olem  6450  f2ndf  6452  f1od2  6461  elmpom  6464  fvn0elsupp  6481  suppfnss  6487  tposf12  6530  smores2  6555  tfrlemisucaccv  6586  tfrlemibfn  6589  tfr1onlemsucaccv  6602  tfr1onlembfn  6605  tfrcllemsucaccv  6615  tfrcllembfn  6618  tfrcl  6625  tfri3  6628  frecabcl  6660  nnsucsssuc  6755  ersym  6809  ertr  6812  swoer  6825  erth  6843  riinerm  6872  qliftfund  6882  eroprf  6892  ecopoverg  6900  th3qlem1  6901  mapfoss  6937  elmapssres  6944  mapss  6963  fdiagfn  6964  ixpssmap2g  6999  mapsnf1o  7009  f1oen4g  7028  f1dom4g  7029  f1dom2g  7032  dom3d  7050  en2prd  7096  dom1oi  7107  pw2f1odclem  7124  fopwdom  7126  mapxpen  7138  nndomo  7155  dif1en  7173  findcard2  7183  findcard2s  7184  diffisn  7187  fimax2gtrilemstep  7195  eqsndc  7200  fientri3  7212  tpfidceq  7227  fiintim  7228  opabfi  7237  f1dmvrnfibi  7248  sbthlemi6  7269  0fsupp  7288  elfir  7297  fifo  7304  2omap  7308  supelti  7332  supsnti  7335  cnvinfex  7348  ordiso2  7365  updjud  7412  djudom  7423  difinfsn  7430  ctssdc  7443  enumctlemm  7444  enumct  7445  nninfninc  7453  enomnilem  7468  fodjuf  7475  ismkvnex  7485  omnimkv  7486  enmkvlem  7491  enwomnilem  7499  nninfdcinf  7501  nninfwlporlem  7503  isnumi  7517  exmidfodomrlemrALT  7545  finacn  7550  djudoml  7565  djudomr  7566  netap  7610  2omotaplemap  7613  2omotaplemst  7614  exmidapne  7616  cc2lem  7622  cc3  7624  ltsopi  7677  pitri3or  7679  ltdcpi  7680  indpi  7699  enqdc  7718  enqdc1  7719  addcmpblnq  7724  mulcanenq  7742  recrecnq  7751  nqtri3or  7753  ltdcnq  7754  ltsonq  7755  ltaddnq  7764  subhalfnqq  7771  archnqq  7774  prarloclemarch2  7776  enq0tr  7791  nqnq0  7798  addcmpblnq0  7800  mulcanenq0ec  7802  nnnq0lem1  7803  nqpnq0nq  7810  nq0m0r  7813  nq02m  7822  prarloclemlt  7850  prarloclemcalc  7859  addlocpr  7893  nqprl  7908  nqpru  7909  addnqprlemrl  7914  addnqprlemru  7915  prmuloclemcalc  7922  mullocprlem  7927  mulnqprlemrl  7930  mulnqprlemru  7931  1idprl  7947  1idpru  7948  ltaddpr  7954  ltexprlemm  7957  ltexprlemopl  7958  ltexprlemopu  7960  ltexprlemdisj  7963  ltexprlemrl  7967  ltexprlemru  7969  addcanprleml  7971  addcanprlemu  7972  addcanprg  7973  prplnqu  7977  recexprlemloc  7988  recexprlem1ssl  7990  recexprlem1ssu  7991  aptiprleml  7996  aptiprlemu  7997  archpr  8000  cauappcvgprlemm  8002  cauappcvgprlemopl  8003  cauappcvgprlemloc  8009  cauappcvgprlemladdfu  8011  cauappcvgprlemladdfl  8012  cauappcvgprlem1  8016  cauappcvgprlem2  8017  caucvgprlemnkj  8023  caucvgprlemopl  8026  caucvgprlemloc  8032  caucvgprlemladdfu  8034  caucvgprlem2  8037  caucvgprprlemnkltj  8046  caucvgprprlemopl  8054  caucvgprprlemloc  8060  caucvgprprlemexbt  8063  caucvgprprlemaddq  8065  caucvgprprlem2  8067  suplocexprlemmu  8075  suplocexprlemru  8076  suplocexprlemloc  8078  suplocexprlemlub  8081  prsrlem1  8099  0idsr  8124  1idsr  8125  recexgt0sr  8130  archsr  8139  prsradd  8143  caucvgsrlemcau  8150  caucvgsrlembound  8151  caucvgsrlemoffgt1  8156  suplocsrlemb  8163  suplocsrlempr  8164  suplocsrlem  8165  pitonnlem1p1  8203  pitonn  8205  pitoregt0  8206  peano2nnnn  8210  recidpirq  8215  axcaucvglemval  8254  leid  8399  nltled  8437  readdcan  8456  addneintrd  8504  addneintr2d  8505  pncan  8522  subsub2  8544  subsub4  8549  negned  8624  subne0d  8636  subneintrd  8671  subneintr2d  8673  subeq0bd  8696  subdi  8702  gt0add  8891  rimul  8903  rereim  8904  ltmul1a  8909  apreim  8921  apirr  8923  mulap0r  8933  msqge0  8934  mulge0  8937  gt0ap0  8944  ltap  8951  subap0d  8962  recexaplem2  8970  mulap0bad  8977  mulap0bbd  8978  mul0eqap  8990  divrecap  9008  div0ap  9022  div1  9023  recrecap  9029  divdivdivap  9033  ddcanap  9046  rerecclap  9050  div2negap  9055  diveqap1bd  9156  recgt0  9170  prodgt0  9172  lemul1a  9178  recp1lt1  9219  squeeze0  9224  peano2nn  9295  div4p1lem1div2  9538  arch  9539  peano2z  9659  peano2zm  9661  ztri3or  9666  nn0n0n1ge2  9694  zextle  9716  gtndiv  9720  suprzclex  9723  nn0ind-raph  9742  uzid  9915  uzneg  9920  uztric  9923  uz11  9924  eluzp1l  9926  qdivcl  10022  irrmul  10026  irrmulap  10027  rpnegap  10066  negelrpd  10068  ledivge1le  10106  mul2lt0rlt0  10139  mul2lt0rgt0  10140  nn0ledivnn  10147  ltpnf  10161  mnflt  10164  pnfge  10170  mnfle  10173  xrlttr  10176  xrltso  10177  xrlttri3  10178  xrleid  10181  xaddass2  10251  xltadd1  10257  xlt2add  10261  xleaddadd  10268  lincmble  10385  iccf1o  10386  fztri3or  10422  fznlem  10424  fzn  10425  fzsplit2  10433  fzsplit3  10436  fznatpl1  10461  uzsplit  10477  fseq1p1m1  10479  fzm1  10485  fznn0sub2  10513  difelfznle  10520  1fv  10524  fzodcel  10538  fzospliti  10563  fzouzsplit  10566  eluzgtdifelfzo  10593  exfzdc  10637  subfzo0  10639  zsupcllemstep  10640  zsupcl  10642  zssinfcl  10643  infssuzex  10644  infssuzcldc  10646  infssfzcldc  10647  infssfzledc  10648  suprzubdc  10649  nninfdcex  10650  qdcle  10659  exbtwnz  10663  qbtwnrelemcalc  10668  flqlelt  10689  qfraclt1  10693  qfracge0  10694  flqltnz  10700  btwnzge0  10713  flhalf  10715  fldiv4lem1div2uz2  10719  ceiqle  10728  intfracq  10735  mulqmod0  10745  modqge0  10747  modqlt  10748  modqid  10764  modqid0  10765  m1modge3gt1  10786  modqltm1p1mod  10791  q2txmodxeq0  10799  modaddmodlo  10803  modsumfzodifsn  10811  addmodlteq  10813  frecuzrdgtcl  10827  frecuzrdgtclt  10836  uzennn  10851  uzsinds  10859  seqf  10879  seqf2  10883  monoord2  10901  iseqf1olemqk  10922  iseqf1olemjpcl  10923  iseqf1olemqpcl  10924  seq3f1olemqsumkj  10926  seq3f1olemqsum  10928  seq3f1olemstep  10929  seq3f1oleml  10931  seqf1oglem1  10934  ser3le  10952  exp3vallem  10955  exp3val  10956  expp1  10961  expcllem  10965  ltexp2a  11006  leexp2a  11007  resq01  11073  nn0ltexp2  11125  faclbnd  11157  faclbnd2  11158  faclbnd3  11159  bcval5  11179  bcpasc  11182  bcm1n  11185  hashennn  11197  fihasheqf1oi  11204  hashsng  11215  fihashfn  11218  hashun  11223  fihashss  11235  fihashssdif  11237  hashfz  11240  hashxp  11245  hashmap  11246  hashpwfi  11247  fimaxq  11248  sseqn  11257  hashfibclem  11260  hashf1lem2  11264  hashf1  11265  zfz1isolem1  11270  seq3coll  11272  hashdmprop2dom  11274  wrdf  11288  wrdlenge2n0  11318  fstwrdne0  11322  wrdred1hash  11326  ccatvalfn  11347  ccatsymb  11348  ccatlid  11352  ccatrid  11353  ccatrn  11355  ccatalpha  11359  eqs1  11374  ccats1val2  11386  fzowrddc  11397  swrdlen  11402  swrdnd  11409  swrd0g  11410  swrdfv2  11413  swrdwrdsymbg  11414  pfxn0  11438  pfxwrdsymbg  11440  pfxsuff1eqwrdeq  11449  swrdswrd  11455  ccats1pfxeq  11464  ccats1pfxeqrex  11465  wrdind  11472  wrd2ind  11473  swrdccatin1  11475  pfxccatin12lem4  11476  swrdccatin2  11479  pfxccatin12  11483  pfxccat3a  11488  swrdccat3blem  11489  pfxccatid  11491  swrdccatin2d  11494  shftfn  11567  cjth  11589  cjmulrcl  11630  sq01  11638  reim0bd  11688  rerebd  11689  cjrebd  11690  caucvgre  11725  cvg1nlemcxze  11726  cvg1nlemcau  11728  cvg1nlemres  11729  recvguniq  11739  resqrexlemover  11754  resqrexlemdec  11755  resqrexlemgt0  11764  resqrexlemoverl  11765  resqrexlemglsq  11766  rersqrtthlem  11774  sqrtgt0  11778  leabs  11818  absexpzap  11824  absle  11833  recvalap  11841  abstri  11848  abs2dif  11850  amgm2  11862  absne0d  11931  maxleim  11949  maxabslemab  11950  maxabslemlub  11951  maxltsup  11962  zmaxcl  11968  fimaxre2  11971  minmax  11974  rpmincl  11982  bdtrilem  11983  bdtri  11984  xrmaxleim  11988  xrmaxiflemcom  11993  xrmaxltsup  12002  xrmaxadd  12005  xrminmax  12009  xrminrpcl  12018  climconst  12034  climuni  12037  2clim  12045  climcn1  12052  climcn2  12053  reccn2ap  12057  climge0  12069  climle  12078  climsqz  12079  climsqz2  12080  serf0  12096  summodclem3  12125  summodclem2a  12126  fsumcl2lem  12143  sumpr  12158  sumtp  12159  fsum0diaglem  12185  mptfzshft  12187  fsumle  12208  fsumlt  12209  divcnv  12242  trireciplem  12245  expcnvap0  12247  expcnv  12249  explecnv  12250  geosergap  12251  cvgratnnlembern  12268  cvgratnnlemabsle  12272  cvgratnnlemsumlt  12273  cvgratz  12277  cvgratgt0  12278  mertenslemi1  12280  mertenslem2  12281  mertensabs  12282  clim2divap  12285  prodmodclem3  12320  prodmodclem2a  12321  fprodseq  12328  fprodmul  12336  fprodfac  12360  fprodconst  12365  fprodap0  12366  fprodap0f  12381  fprodle  12385  eftcl  12399  ef0lem  12405  efsub  12426  eftlub  12435  eflegeo  12446  tanval2ap  12458  sinadd  12481  cos2t  12495  cos2tsin  12496  sin01bnd  12502  cos01bnd  12503  eirraplem  12522  dvdsval2  12535  dvdsdc  12543  dvds0lem  12546  zdvdsdc  12557  dvdscmulr  12565  dvdsmulcr  12566  fsumdvds  12587  dvdslelemd  12588  divconjdvds  12594  dvdsext  12600  fzm1ndvds  12601  dvdsmod  12607  3dvds  12609  oexpneg  12622  2tp1odd  12629  mulsucdiv2z  12630  2teven  12632  zeo5  12633  opeo  12642  omeo  12643  nn0ob  12653  divalglemnqt  12665  bitsdc  12692  bits0o  12695  bitsfzolem  12699  bitsfzo  12700  bitsmod  12701  bitscmp  12703  bitsinv1lem  12706  gcddvds  12718  dvdslegcd  12719  gcdneg  12737  bezoutlemnewy  12751  bezoutlemstep  12752  bezoutlema  12754  bezoutlemb  12755  bezoutlemmo  12761  bezoutlemle  12763  bezoutlemsup  12764  dfgcd3  12765  bezout  12766  dfgcd2  12769  uzwodc  12792  lcmcllem  12823  lcmneg  12830  lcmgcdlem  12833  lcmdvds  12835  lcmid  12836  3lcm2e6woprm  12842  6lcm4e12  12843  ncoprmgcdne1b  12845  mulgcddvds  12850  divgcdcoprmex  12858  cncongr1  12859  cncongr2  12860  isprm2lem  12872  prmind2  12876  dvdsnprmd  12881  prm2orodd  12882  sqnprm  12892  isprm5lem  12897  rpexp  12909  sqrt2irrlem  12917  oddpwdclemdc  12929  sqrt2irraplemnn  12935  qnumdencoprm  12949  qeqnumdivden  12950  nn0gcdsq  12956  nn0sqrtelqelz  12962  nonsq  12963  phicl2  12970  phibnd  12973  hashdvds  12977  phiprmpw  12978  phimullem  12981  eulerthlemrprm  12985  eulerthlema  12986  eulerthlemth  12988  prmdiveq  12992  hashgcdlem  12994  odzdvds  13002  modprminv  13006  nnnn0modprm0  13012  modprmn0modprm0  13013  pythagtriplem10  13026  pythagtriplem19  13039  pythagtrip  13040  pcpre1  13049  pcpremul  13050  pceu  13052  pcmul  13058  pcdiv  13059  pcqmul  13060  pcqdiv  13064  pcexp  13066  pcdvdsb  13077  pcidlem  13080  pcdvdstr  13084  pcgcd1  13085  pc2dvds  13087  pcprmpw2  13090  difsqpwdvds  13095  pcaddlem  13096  pcadd  13097  pcadd2  13098  pcmpt  13100  pcmptdvds  13102  pcprod  13103  fldivp1  13105  pcfaclem  13106  pcfac  13107  pcbc  13108  qexpz  13109  pockthlem  13113  pockthg  13114  1arithlem4  13123  1arith  13124  1arith2  13125  4sqlem6  13140  4sqlem8  13142  4sqlem9  13143  4sqlem10  13144  4sqexercise1  13155  4sqexercise2  13156  4sqlemsdc  13157  4sqlem11  13158  4sqlem12  13159  4sqlem15  13162  4sqlem16  13163  4sqlem17  13164  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemimin  13227  ballotfilem1c  13229  ballotfilemro  13244  ballotfilemfrcn0  13251  znnen  13267  ennnfonelemk  13269  ennnfonelemkh  13281  ennnfonelemhf1o  13282  ennnfonelemrnh  13285  ennnfonelemfun  13286  ennnfonelemf1  13287  ennnfonelemrn  13288  ennnfonelemnn0  13291  ctinfomlemom  13296  ctiunctlemudc  13306  unct  13311  omctfn  13312  ssnnctlemct  13315  nninfdclemp1  13319  nninfdc  13322  structfung  13347  setsfun  13365  setsfun0  13366  setscom  13370  strslfv3  13376  setsslid  13381  imasaddfnlemg  13612  imasaddvallemg  13613  mgmsscl  13658  plusffng  13662  mgmplusf  13663  mgm0  13666  mgm1  13667  opifismgmdc  13668  gzsumfzval  13688  sgrp1  13703  issgrpd  13704  mndpfo  13728  mndfo  13729  mnd1  13739  0subm  13768  mhmima  13775  grpinvfng  13826  isgrpinv  13836  grpinvid  13842  grpinvf1o  13852  grpinvadd  13860  grpsubf  13861  grpsubsub4  13875  grplactcnv  13884  grp1  13888  grp1inv  13889  qusgrp2  13893  mulgfng  13904  subginv  13961  resgrpisgrp  13975  subgintm  13978  0subg  13979  0nsg  13994  qusinv  14016  ghminv  14030  ghmrn  14037  ghmeql  14047  ghmnsgima  14048  kerf1ghm  14054  conjnmz  14059  gzsumshift  14126  gsumvalfi  14129  gzsumgsum  14132  gsumsncmn  14133  gsump1  14134  gsumf1ofi  14137  gsumsubmclfi  14140  prdsplusgsgrpcl  14167  prdsplusgcl  14169  prdsidlem  14170  prdsinvlem  14173  prdsinvgd  14175  pwsdiagel  14187  pwssnf1o  14188  rngass  14213  rngmneg1  14221  rngmneg2  14222  qusrng  14232  srgideu  14250  srgidmlem  14256  srgpcomp  14268  srg1expzeq1  14273  ringcl  14291  ringideu  14295  ringidmlem  14300  ringnegl  14329  ringnegr  14330  ring1  14337  qusring2  14344  opprringbg  14358  dvdsrd  14374  dvdsr01  14384  isunitd  14386  unitinvcl  14403  unitinvinv  14404  unitnegcl  14410  rhmmul  14444  rhmf1o  14448  nzrunit  14468  lringuplu  14476  subrngintm  14493  subrgsubm  14515  subrgintm  14524  rrgsupp  14547  ringunitap  14566  aprsym  14569  aprnzr  14572  aprlring  14573  drnglring  14580  drngunitap  14581  scaffng  14618  lmodscaf  14619  lsssn0  14679  lss1d  14692  lssintclm  14693  lspval  14699  lspcl  14700  lspsnid  14716  lspprid1  14720  lspsn  14725  sraval  14746  rspcl  14800  rspssid  14801  rspssp  14803  rnglidlmmgm  14805  rnglidlmsgrp  14806  cnfldneg  14882  zringinvg  14911  expghmap  14914  znzrhfo  14955  znf1o  14958  znhash  14963  znidomb  14965  znrrg  14967  psrbagfsupp  14978  psrbagfi  14982  psrbaglecl  14983  psrbagaddclfi  14984  psrbagcon  14985  psraddcl  14994  psr0cl  14995  psrnegcl  14997  psrneg  15001  psr1clfi  15002  mplsubgfilemm  15012  mplsubgfilemcl  15013  baspartn  15074  eltg3i  15080  tgclb  15089  topbas  15091  2basgeng  15106  topcld  15133  0cld  15136  uncld  15137  neif  15165  elnei  15176  0nei  15190  restbasg  15192  iscnp4  15242  cnpnei  15243  cnclima  15247  cncnp  15254  cnrest2r  15261  cndis  15265  lmff  15273  lmtopcnp  15274  txbas  15282  txopn  15289  txcnp  15295  upxp  15296  txdis1cn  15302  cnmpt11  15307  cnmpt21  15315  psmetge0  15355  xmetge0  15389  xmettpos  15394  xmetrtri  15400  metrtri  15401  xblpnfps  15422  xblpnf  15423  blfps  15433  blf  15434  ssblps  15449  ssbl  15450  blbas  15457  metss2  15522  xmettxlem  15533  xmettx  15534  qtopbas  15546  divcnap  15589  cncfss  15607  cdivcncfap  15628  expcncf  15633  cnopnap  15635  maxcncf  15639  mincncf  15640  dedekindeulemuub  15641  dedekindeulemlu  15645  dedekindeu  15647  suplociccex  15649  dedekindicclemuub  15650  dedekindicclemlu  15654  dedekindicclemicc  15656  ivthinclemlopn  15660  ivthinclemuopn  15662  ivthinc  15667  ivthreinc  15669  hoverlt1  15673  ellimc3apf  15684  limcimolemlt  15688  limcimo  15689  limcresi  15690  cnplimclemle  15692  reldvg  15703  dvfgg  15712  dvidlemap  15715  dvidrelem  15716  dvidsslem  15717  dvcjbr  15732  dvcj  15733  dvrecap  15737  dveflem  15750  dvef  15751  elply2  15759  elplyr  15764  plycj  15785  plyreres  15788  reeff1oleme  15796  pilem3  15807  sinq34lt0t  15855  cosq14gt0  15856  coseq0q4123  15858  tangtx  15862  sincosq1eq  15863  cosordlem  15873  logdivlti  15905  relogbval  15976  relogbzcl  15977  nnlogbexp  15984  logbgcd1irr  15992  logbgcd1irraplemexp  15993  logbgcd1irraplemap  15994  pellexlem1  16005  pellexlem3  16007  wilthlem1  16008  mpodvdsmulf1o  16018  mersenne  16025  perfectlem2  16028  perfect  16029  zabsle1  16032  lgslem1  16033  lgsval  16037  lgsfvalg  16038  lgsfcl2  16039  lgsval2lem  16043  lgscl1  16056  lgsmod  16059  lgsdir2lem5  16065  lgsdir2  16066  lgsdilem2  16069  lgsdi  16070  lgsne0  16071  gausslemma2dlem0c  16084  gausslemma2dlem0h  16089  gausslemma2dlem1a  16091  gausslemma2dlem1f1o  16093  gausslemma2dlem3  16096  lgseisenlem1  16103  lgseisenlem2  16104  lgseisenlem3  16105  lgseisenlem4  16106  lgseisen  16107  lgsquadlem1  16110  lgsquadlem2  16111  lgsquadlem3  16112  lgsquad3  16117  2lgslem3b1  16131  2lgslem3c1  16132  2lgs  16137  2lgsoddprmlem2  16139  2lgsoddprm  16146  2sqlem3  16150  2sqlem8  16156  2sqlem10  16158  structgrssvtx  16197  structgrssiedg  16198  ushgruhgr  16235  uhgrun  16241  incistruhgr  16245  upgrop  16259  upgruhgr  16266  umgrupgr  16267  umgrnloopv  16269  umgredgprv  16270  umgr0e  16273  upgr1edc  16276  umgr1een  16280  upgrun  16281  umgrun  16283  umgrislfupgrdom  16286  upgredg  16299  umgrpredgv  16302  usgrop  16321  usgrausgrien  16324  ausgrumgrien  16325  ausgrusgrien  16326  uspgrupgrushgr  16337  usgrumgr  16339  usgrumgruspgr  16340  usgruspgrben  16341  usgrislfuspgrdom  16345  edgssv2en  16354  usgrf1oedg  16360  usgredg4  16370  usgredg2vlem2  16378  usgredg2v  16379  ushgredgedg  16381  ushgredgedgloop  16383  usgrstrrepeen  16386  usgr0e  16387  uhgr0v0e  16389  uspgr1edc  16395  usgr1e  16396  griedg0ssusgr  16406  subgrprop3  16417  subgruhgredgdm  16425  subuhgr  16427  subupgr  16428  subumgr  16429  subusgr  16430  uhgrspansubgrlem  16431  1loopgrvd2fi  16460  1loopgrvd0fi  16461  1hevtxdg0fi  16462  vdegp1aid  16469  vdegp1bid  16470  wlkm  16494  wlkvtxiedg  16500  wlkvtxiedgg  16501  wlkeq  16509  wlk1walkdom  16514  uspgr2wlkeq  16520  uspgr2wlkeqi  16522  upgr2wlkdc  16532  wlkres  16534  trlreslem  16544  clwwlkccatlem  16555  clwwlkn1loopb  16575  clwwlkext2edg  16577  clwwlknonex2lem1  16592  clwwlknonex2  16594  trlsegvdeglem2  16616  trlsegvdeglem3  16617  eupth2lem3lem4fi  16628  eupth2lemsfi  16633  fnmptd  16746  bj-sels  16854  bj-nnelon  16899  pw1map  16939  pwle2  16942  pwf1oexmid  16943  pw1nct  16947  nninfall  16957  nninfsellemdc  16958  nninfself  16961  nnnninfex  16970  nninfnfiinf  16971  refeq  16978  isomninnlem  16984  cvgcmp2nlemabs  16986  trilpolemlt1  16995  trirec0  16998  apdifflemf  17000  apdifflemr  17001  apdiff  17002  qdiff  17003  iswomninnlem  17004  iswomni0  17006  ismkvnnlem  17007  reap0  17013  cndcap  17014