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 )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used 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  3687  elpwd  3697  eqbrtrd  4152  3brtr4d  4162  snelpwi  4351  prelpwi  4354  pwel  4358  ordelon  4528  onin  4531  elelsuc  4554  onsuc  4648  onsucb  4650  onintonm  4664  omsinds  4769  sosng  4848  relssdv  4867  eqbrrdv  4872  eqrelrdv2  4874  relsnopg  4879  breldmg  4987  elrnmptdv  5036  iss  5109  xpimasn  5236  elxp4  5275  elxp5  5276  iotam  5369  funssres  5420  f0rn0  5587  fimadmfo  5624  sefvex  5716  fdmeu  5746  fvun1  5769  eqfnfvd  5809  fvimacnvi  5823  fvimacnv  5824  fvelrn  5839  fmpt3d  5864  fmpt2d  5870  resflem  5872  fmptco  5874  fsn  5880  funopsn  5891  fncofn  5893  ftpg  5899  fconst2g  5930  funfvima3  5952  elabrexg  5964  foeqcnvco  5996  f1eqcocnv  5997  fliftfun  6002  fliftfund  6003  fliftval  6006  riota5f  6065  f1ofveu  6073  f1ocnvd  6292  f1opw2  6296  f1o3d  6298  off  6315  offval2  6318  ofrfval2  6319  offveq  6323  caofref  6327  caofinvl  6328  elxp6  6403  cnvf1olem  6460  f2ndf  6462  f1od2  6471  elmpom  6474  fvn0elsupp  6491  suppfnss  6497  tposf12  6540  smores2  6565  tfrlemisucaccv  6596  tfrlemibfn  6599  tfr1onlemsucaccv  6612  tfr1onlembfn  6615  tfrcllemsucaccv  6625  tfrcllembfn  6628  tfrcl  6635  tfri3  6638  frecabcl  6670  nnsucsssuc  6765  ersym  6819  ertr  6822  swoer  6835  erth  6853  riinerm  6882  qliftfund  6892  eroprf  6902  ecopoverg  6910  th3qlem1  6911  mapfoss  6947  elmapssres  6954  mapss  6973  fdiagfn  6974  ixpssmap2g  7009  mapsnf1o  7019  f1oen4g  7038  f1dom4g  7039  f1dom2g  7042  dom3d  7060  en2prd  7106  dom1oi  7117  pw2f1odclem  7134  fopwdom  7136  mapxpen  7148  nndomo  7165  dif1en  7183  findcard2  7193  findcard2s  7194  diffisn  7197  fimax2gtrilemstep  7205  eqsndc  7210  fientri3  7222  tpfidceq  7237  fiintim  7238  opabfi  7247  f1dmvrnfibi  7258  sbthlemi6  7279  0fsupp  7298  elfir  7307  fifo  7314  2omap  7318  supelti  7342  supsnti  7345  cnvinfex  7358  ordiso2  7375  updjud  7422  djudom  7433  difinfsn  7440  ctssdc  7453  enumctlemm  7454  enumct  7455  nninfninc  7463  enomnilem  7478  fodjuf  7485  ismkvnex  7495  omnimkv  7496  enmkvlem  7501  enwomnilem  7509  nninfdcinf  7511  nninfwlporlem  7513  isnumi  7527  exmidfodomrlemrALT  7555  finacn  7560  djudoml  7575  djudomr  7576  netap  7620  2omotaplemap  7623  2omotaplemst  7624  exmidapne  7626  cc2lem  7632  cc3  7634  ltsopi  7687  pitri3or  7689  ltdcpi  7690  indpi  7709  enqdc  7728  enqdc1  7729  addcmpblnq  7734  mulcanenq  7752  recrecnq  7761  nqtri3or  7763  ltdcnq  7764  ltsonq  7765  ltaddnq  7774  subhalfnqq  7781  archnqq  7784  prarloclemarch2  7786  enq0tr  7801  nqnq0  7808  addcmpblnq0  7810  mulcanenq0ec  7812  nnnq0lem1  7813  nqpnq0nq  7820  nq0m0r  7823  nq02m  7832  prarloclemlt  7860  prarloclemcalc  7869  addlocpr  7903  nqprl  7918  nqpru  7919  addnqprlemrl  7924  addnqprlemru  7925  prmuloclemcalc  7932  mullocprlem  7937  mulnqprlemrl  7940  mulnqprlemru  7941  1idprl  7957  1idpru  7958  ltaddpr  7964  ltexprlemm  7967  ltexprlemopl  7968  ltexprlemopu  7970  ltexprlemdisj  7973  ltexprlemrl  7977  ltexprlemru  7979  addcanprleml  7981  addcanprlemu  7982  addcanprg  7983  prplnqu  7987  recexprlemloc  7998  recexprlem1ssl  8000  recexprlem1ssu  8001  aptiprleml  8006  aptiprlemu  8007  archpr  8010  cauappcvgprlemm  8012  cauappcvgprlemopl  8013  cauappcvgprlemloc  8019  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  cauappcvgprlem1  8026  cauappcvgprlem2  8027  caucvgprlemnkj  8033  caucvgprlemopl  8036  caucvgprlemloc  8042  caucvgprlemladdfu  8044  caucvgprlem2  8047  caucvgprprlemnkltj  8056  caucvgprprlemopl  8064  caucvgprprlemloc  8070  caucvgprprlemexbt  8073  caucvgprprlemaddq  8075  caucvgprprlem2  8077  suplocexprlemmu  8085  suplocexprlemru  8086  suplocexprlemloc  8088  suplocexprlemlub  8091  prsrlem1  8109  0idsr  8134  1idsr  8135  recexgt0sr  8140  archsr  8149  prsradd  8153  caucvgsrlemcau  8160  caucvgsrlembound  8161  caucvgsrlemoffgt1  8166  suplocsrlemb  8173  suplocsrlempr  8174  suplocsrlem  8175  pitonnlem1p1  8213  pitonn  8215  pitoregt0  8216  peano2nnnn  8220  recidpirq  8225  axcaucvglemval  8264  leid  8409  nltled  8447  readdcan  8466  addneintrd  8514  addneintr2d  8515  pncan  8532  subsub2  8554  subsub4  8559  negned  8634  subne0d  8646  subneintrd  8681  subneintr2d  8683  subeq0bd  8706  subdi  8712  gt0add  8901  rimul  8913  rereim  8914  ltmul1a  8919  apreim  8931  apirr  8933  mulap0r  8943  msqge0  8944  mulge0  8947  gt0ap0  8954  ltap  8961  subap0d  8972  recexaplem2  8980  mulap0bad  8987  mulap0bbd  8988  mul0eqap  9000  divrecap  9018  div0ap  9032  div1  9033  recrecap  9039  divdivdivap  9043  ddcanap  9056  rerecclap  9060  div2negap  9065  diveqap1bd  9166  recgt0  9180  prodgt0  9182  lemul1a  9188  recp1lt1  9229  squeeze0  9234  peano2nn  9316  div4p1lem1div2  9559  arch  9560  peano2z  9680  peano2zm  9682  ztri3or  9687  nn0n0n1ge2  9715  zextle  9737  gtndiv  9741  suprzclex  9744  nn0ind-raph  9763  uzid  9936  uzneg  9941  uztric  9944  uz11  9945  eluzp1l  9947  qdivcl  10043  irrmul  10047  irrmulap  10048  rpnegap  10087  negelrpd  10089  ledivge1le  10127  mul2lt0rlt0  10160  mul2lt0rgt0  10161  nn0ledivnn  10168  ltpnf  10182  mnflt  10185  pnfge  10191  mnfle  10194  xrlttr  10197  xrltso  10198  xrlttri3  10199  xrleid  10202  xaddass2  10272  xltadd1  10278  xlt2add  10282  xleaddadd  10289  lincmble  10406  iccf1o  10407  fztri3or  10443  fznlem  10445  fzn  10446  fzsplit2  10455  fzsplit3  10458  fznatpl1  10483  uzsplit  10499  fseq1p1m1  10501  fzm1  10507  fznn0sub2  10535  difelfznle  10542  1fv  10546  fzodcel  10560  fzospliti  10585  fzouzsplit  10588  eluzgtdifelfzo  10615  exfzdc  10659  subfzo0  10661  zsupcllemstep  10662  zsupcl  10664  zssinfcl  10665  infssuzex  10666  infssuzcldc  10668  infssfzcldc  10669  infssfzledc  10670  suprzubdc  10671  nninfdcex  10672  qdcle  10681  exbtwnz  10685  qbtwnrelemcalc  10690  flqlelt  10711  qfraclt1  10715  qfracge0  10716  flqltnz  10722  btwnzge0  10735  flhalf  10737  fldiv4lem1div2uz2  10741  ceiqle  10750  intfracq  10757  mulqmod0  10767  modqge0  10769  modqlt  10770  modqid  10786  modqid0  10787  m1modge3gt1  10808  modqltm1p1mod  10813  q2txmodxeq0  10821  modaddmodlo  10825  modsumfzodifsn  10833  addmodlteq  10835  frecuzrdgtcl  10849  frecuzrdgtclt  10858  uzennn  10873  uzsinds  10881  seqf  10901  seqf2  10905  monoord2  10923  iseqf1olemqk  10944  iseqf1olemjpcl  10945  iseqf1olemqpcl  10946  seq3f1olemqsumkj  10948  seq3f1olemqsum  10950  seq3f1olemstep  10951  seq3f1oleml  10953  seqf1oglem1  10956  ser3le  10974  exp3vallem  10977  exp3val  10978  expp1  10983  expcllem  10987  ltexp2a  11028  leexp2a  11029  resq01  11095  nn0ltexp2  11147  faclbnd  11179  faclbnd2  11180  faclbnd3  11181  bcval5  11201  bcpasc  11204  bcm1n  11207  hashennn  11219  fihasheqf1oi  11226  hashsng  11237  fihashfn  11240  hashun  11245  fihashss  11257  fihashssdif  11259  hashfz  11262  hashxp  11267  hashmap  11268  hashpwfi  11269  fimaxq  11270  sseqn  11279  hashfibclem  11282  hashf1lem2  11286  hashf1  11287  zfz1isolem1  11292  seq3coll  11294  hashdmprop2dom  11296  wrdf  11310  wrdlenge2n0  11340  fstwrdne0  11344  wrdred1hash  11348  ccatvalfn  11369  ccatsymb  11370  ccatlid  11374  ccatrid  11375  ccatrn  11377  ccatalpha  11381  eqs1  11396  ccats1val2  11408  fzowrddc  11419  swrdlen  11424  swrdnd  11431  swrd0g  11432  swrdfv2  11435  swrdwrdsymbg  11436  pfxn0  11460  pfxwrdsymbg  11462  pfxsuff1eqwrdeq  11471  swrdswrd  11477  ccats1pfxeq  11486  ccats1pfxeqrex  11487  wrdind  11494  wrd2ind  11495  swrdccatin1  11497  pfxccatin12lem4  11498  swrdccatin2  11501  pfxccatin12  11505  pfxccat3a  11510  swrdccat3blem  11511  pfxccatid  11513  swrdccatin2d  11516  shftfn  11589  cjth  11611  cjmulrcl  11652  sq01  11660  reim0bd  11710  rerebd  11711  cjrebd  11712  caucvgre  11747  cvg1nlemcxze  11748  cvg1nlemcau  11750  cvg1nlemres  11751  recvguniq  11761  resqrexlemover  11776  resqrexlemdec  11777  resqrexlemgt0  11786  resqrexlemoverl  11787  resqrexlemglsq  11788  rersqrtthlem  11796  sqrtgt0  11800  leabs  11840  absexpzap  11846  absle  11855  recvalap  11863  abstri  11870  abs2dif  11872  amgm2  11884  absne0d  11953  maxleim  11971  maxabslemab  11972  maxabslemlub  11973  maxltsup  11984  zmaxcl  11990  fimaxre2  11993  minmax  11996  rpmincl  12004  bdtrilem  12005  bdtri  12006  xrmaxleim  12010  xrmaxiflemcom  12015  xrmaxltsup  12024  xrmaxadd  12027  xrminmax  12031  xrminrpcl  12040  climconst  12056  climuni  12059  2clim  12067  climcn1  12074  climcn2  12075  reccn2ap  12079  climge0  12091  climle  12100  climsqz  12101  climsqz2  12102  serf0  12118  summodclem3  12147  summodclem2a  12148  fsumcl2lem  12165  sumpr  12180  sumtp  12181  fsum0diaglem  12207  mptfzshft  12209  fsumle  12230  fsumlt  12231  divcnv  12264  trireciplem  12267  expcnvap0  12269  expcnv  12271  explecnv  12272  geosergap  12273  cvgratnnlembern  12290  cvgratnnlemabsle  12294  cvgratnnlemsumlt  12295  cvgratz  12299  cvgratgt0  12300  mertenslemi1  12302  mertenslem2  12303  mertensabs  12304  clim2divap  12307  prodmodclem3  12342  prodmodclem2a  12343  fprodseq  12350  fprodmul  12358  fprodfac  12382  fprodconst  12387  fprodap0  12388  fprodap0f  12403  fprodle  12407  eftcl  12421  ef0lem  12427  efsub  12448  eftlub  12457  eflegeo  12468  tanval2ap  12480  sinadd  12503  cos2t  12517  cos2tsin  12518  sin01bnd  12524  cos01bnd  12525  eirraplem  12544  dvdsval2  12557  dvdsdc  12565  dvds0lem  12568  zdvdsdc  12579  dvdscmulr  12587  dvdsmulcr  12588  fsumdvds  12609  dvdslelemd  12610  divconjdvds  12616  dvdsext  12622  fzm1ndvds  12623  dvdsmod  12629  3dvds  12631  oexpneg  12644  2tp1odd  12651  mulsucdiv2z  12652  2teven  12654  zeo5  12655  opeo  12664  omeo  12665  nn0ob  12675  divalglemnqt  12687  bitsdc  12714  bits0o  12717  bitsfzolem  12721  bitsfzo  12722  bitsmod  12723  bitscmp  12725  bitsinv1lem  12728  gcddvds  12740  dvdslegcd  12741  gcdneg  12759  bezoutlemnewy  12773  bezoutlemstep  12774  bezoutlema  12776  bezoutlemb  12777  bezoutlemmo  12783  bezoutlemle  12785  bezoutlemsup  12786  dfgcd3  12787  bezout  12788  dfgcd2  12791  uzwodc  12814  lcmcllem  12845  lcmneg  12852  lcmgcdlem  12855  lcmdvds  12857  lcmid  12858  3lcm2e6woprm  12864  6lcm4e12  12865  ncoprmgcdne1b  12867  mulgcddvds  12872  divgcdcoprmex  12880  cncongr1  12881  cncongr2  12882  isprm2lem  12894  prmind2  12898  dvdsnprmd  12903  prm2orodd  12904  sqnprm  12914  isprm5lem  12919  rpexp  12931  sqrt2irrlem  12939  oddpwdclemdc  12951  sqrt2irraplemnn  12957  qnumdencoprm  12971  qeqnumdivden  12972  nn0gcdsq  12978  nn0sqrtelqelz  12984  nonsq  12985  phicl2  12992  phibnd  12995  hashdvds  12999  phiprmpw  13000  phimullem  13003  eulerthlemrprm  13007  eulerthlema  13008  eulerthlemth  13010  prmdiveq  13014  hashgcdlem  13016  odzdvds  13024  modprminv  13028  nnnn0modprm0  13034  modprmn0modprm0  13035  pythagtriplem10  13048  pythagtriplem19  13061  pythagtrip  13062  pcpre1  13071  pcpremul  13072  pceu  13074  pcmul  13080  pcdiv  13081  pcqmul  13082  pcqdiv  13086  pcexp  13088  pcdvdsb  13099  pcidlem  13102  pcdvdstr  13106  pcgcd1  13107  pc2dvds  13109  pcprmpw2  13112  difsqpwdvds  13117  pcaddlem  13118  pcadd  13119  pcadd2  13120  pcmpt  13122  pcmptdvds  13124  pcprod  13125  fldivp1  13127  pcfaclem  13128  pcfac  13129  pcbc  13130  qexpz  13131  pockthlem  13135  pockthg  13136  1arithlem4  13145  1arith  13146  1arith2  13147  4sqlem6  13162  4sqlem8  13164  4sqlem9  13165  4sqlem10  13166  4sqexercise1  13177  4sqexercise2  13178  4sqlemsdc  13179  4sqlem11  13180  4sqlem12  13181  4sqlem15  13184  4sqlem16  13185  4sqlem17  13186  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemimin  13249  ballotfilem1c  13251  ballotfilemro  13266  ballotfilemfrcn0  13273  znnen  13289  ennnfonelemk  13291  ennnfonelemkh  13303  ennnfonelemhf1o  13304  ennnfonelemrnh  13307  ennnfonelemfun  13308  ennnfonelemf1  13309  ennnfonelemrn  13310  ennnfonelemnn0  13313  ctinfomlemom  13318  ctiunctlemudc  13328  unct  13333  omctfn  13334  ssnnctlemct  13337  nninfdclemp1  13341  nninfdc  13344  structfung  13369  setsfun  13387  setsfun0  13388  setscom  13392  strslfv3  13398  setsslid  13403  imasaddfnlemg  13635  imasaddvallemg  13636  mgmsscl  13681  plusffng  13685  mgmplusf  13686  mgm0  13689  mgm1  13690  opifismgmdc  13691  gzsumfzval  13711  sgrp1  13726  issgrpd  13727  mndpfo  13751  mndfo  13752  mnd1  13762  0subm  13791  mhmima  13798  grpinvfng  13849  isgrpinv  13859  grpinvid  13865  grpinvf1o  13875  grpinvadd  13883  grpsubf  13884  grpsubsub4  13898  grplactcnv  13907  grp1  13911  grp1inv  13912  qusgrp2  13916  mulgfng  13927  subginv  13984  resgrpisgrp  13998  subgintm  14001  0subg  14002  0nsg  14017  qusinv  14039  ghminv  14053  ghmrn  14060  ghmeql  14070  ghmnsgima  14071  kerf1ghm  14077  conjnmz  14082  gzsumshift  14149  gsumvalfi  14152  gzsumgsum  14155  gsumsncmn  14156  gsump1  14157  gsumf1ofi  14160  gsumsubmclfi  14163  prdsplusgsgrpcl  14190  prdsplusgcl  14192  prdsidlem  14193  prdsinvlem  14196  prdsinvgd  14198  pwsdiagel  14210  pwssnf1o  14211  rngass  14238  rngmneg1  14246  rngmneg2  14247  qusrng  14257  srgideu  14276  srgidmlem  14282  srgpcomp  14294  srg1expzeq1  14299  ringcl  14317  ringideu  14321  ringidmlem  14327  ringnegl  14356  ringnegr  14357  ring1  14364  qusring2  14371  opprringbg  14385  dvdsrd  14401  dvdsr01  14411  isunitd  14413  unitinvcl  14430  unitinvinv  14431  unitnegcl  14437  rhmmul  14471  rhmf1o  14475  nzrunit  14495  lringuplu  14503  subrngintm  14520  subrgsubm  14542  subrgintm  14551  rrgsupp  14574  ringunitap  14593  aprsym  14596  aprnzr  14599  aprlring  14600  drnglring  14607  drngunitap  14608  scaffng  14646  lmodscaf  14647  lsssn0  14707  lss1d  14720  lssintclm  14721  lspval  14727  lspcl  14728  lspsnid  14744  lspprid1  14748  lspsn  14753  sraval  14774  rspcl  14828  rspssid  14829  rspssp  14831  rnglidlmmgm  14833  rnglidlmsgrp  14834  cnfldneg  14910  zringinvg  14939  expghmap  14942  znzrhfo  14983  znf1o  14986  znhash  14991  znidomb  14993  znrrg  14995  psrbagfsupp  15055  psrbagfi  15059  psrbaglecl  15060  psrbagaddclfi  15061  psrbagcon  15062  psraddcl  15071  psr0cl  15072  psrnegcl  15074  psrneg  15078  psr1clfi  15079  mplsubgfilemm  15089  mplsubgfilemcl  15090  baspartn  15151  eltg3i  15157  tgclb  15166  topbas  15168  2basgeng  15183  topcld  15210  0cld  15213  uncld  15214  neif  15242  elnei  15253  0nei  15267  restbasg  15269  iscnp4  15319  cnpnei  15320  cnclima  15324  cncnp  15331  cnrest2r  15338  cndis  15342  lmff  15350  lmtopcnp  15351  txbas  15359  txopn  15366  txcnp  15372  upxp  15373  txdis1cn  15379  cnmpt11  15384  cnmpt21  15392  psmetge0  15432  xmetge0  15466  xmettpos  15471  xmetrtri  15477  metrtri  15478  xblpnfps  15499  xblpnf  15500  blfps  15510  blf  15511  ssblps  15526  ssbl  15527  blbas  15534  metss2  15599  xmettxlem  15610  xmettx  15611  qtopbas  15623  divcnap  15666  cncfss  15684  cdivcncfap  15705  expcncf  15710  cnopnap  15712  maxcncf  15716  mincncf  15717  dedekindeulemuub  15718  dedekindeulemlu  15722  dedekindeu  15724  suplociccex  15726  dedekindicclemuub  15727  dedekindicclemlu  15731  dedekindicclemicc  15733  ivthinclemlopn  15737  ivthinclemuopn  15739  ivthinc  15744  ivthreinc  15746  hoverlt1  15750  ellimc3apf  15761  limcimolemlt  15765  limcimo  15766  limcresi  15767  cnplimclemle  15769  reldvg  15780  dvfgg  15789  dvidlemap  15792  dvidrelem  15793  dvidsslem  15794  dvcjbr  15809  dvcj  15810  dvrecap  15814  dveflem  15827  dvef  15828  elply2  15836  elplyr  15841  plycj  15862  plyreres  15865  reeff1oleme  15873  pilem3  15884  sinq34lt0t  15932  cosq14gt0  15933  coseq0q4123  15935  tangtx  15939  sincosq1eq  15940  cosordlem  15950  logdivlti  15982  relogbval  16053  relogbzcl  16054  nnlogbexp  16061  logbgcd1irr  16069  logbgcd1irraplemexp  16070  logbgcd1irraplemap  16071  birthdaylem2  16088  birthdaylem3  16089  pellexlem1  16091  pellexlem3  16093  wilthlem1  16094  mpodvdsmulf1o  16104  mersenne  16111  perfectlem2  16114  perfect  16115  zabsle1  16118  lgslem1  16119  lgsval  16123  lgsfvalg  16124  lgsfcl2  16125  lgsval2lem  16129  lgscl1  16142  lgsmod  16145  lgsdir2lem5  16151  lgsdir2  16152  lgsdilem2  16155  lgsdi  16156  lgsne0  16157  gausslemma2dlem0c  16170  gausslemma2dlem0h  16175  gausslemma2dlem1a  16177  gausslemma2dlem1f1o  16179  gausslemma2dlem3  16182  lgseisenlem1  16189  lgseisenlem2  16190  lgseisenlem3  16191  lgseisenlem4  16192  lgseisen  16193  lgsquadlem1  16196  lgsquadlem2  16197  lgsquadlem3  16198  lgsquad3  16203  2lgslem3b1  16217  2lgslem3c1  16218  2lgs  16223  2lgsoddprmlem2  16225  2lgsoddprm  16232  2sqlem3  16236  2sqlem8  16242  2sqlem10  16244  structgrssvtx  16283  structgrssiedg  16284  ushgruhgr  16321  uhgrun  16327  incistruhgr  16331  upgrop  16345  upgruhgr  16352  umgrupgr  16353  umgrnloopv  16355  umgredgprv  16356  umgr0e  16359  upgr1edc  16362  umgr1een  16366  upgrun  16367  umgrun  16369  umgrislfupgrdom  16372  upgredg  16385  umgrpredgv  16388  usgrop  16407  usgrausgrien  16410  ausgrumgrien  16411  ausgrusgrien  16412  uspgrupgrushgr  16423  usgrumgr  16425  usgrumgruspgr  16426  usgruspgrben  16427  usgrislfuspgrdom  16431  edgssv2en  16440  usgrf1oedg  16446  usgredg4  16456  usgredg2vlem2  16464  usgredg2v  16465  ushgredgedg  16467  ushgredgedgloop  16469  usgrstrrepeen  16472  usgr0e  16473  uhgr0v0e  16475  uspgr1edc  16481  usgr1e  16482  griedg0ssusgr  16492  subgrprop3  16503  subgruhgredgdm  16511  subuhgr  16513  subupgr  16514  subumgr  16515  subusgr  16516  uhgrspansubgrlem  16517  1loopgrvd2fi  16546  1loopgrvd0fi  16547  1hevtxdg0fi  16548  vdegp1aid  16555  vdegp1bid  16556  wlkm  16580  wlkvtxiedg  16586  wlkvtxiedgg  16587  wlkeq  16595  wlk1walkdom  16600  uspgr2wlkeq  16606  uspgr2wlkeqi  16608  upgr2wlkdc  16618  wlkres  16620  trlreslem  16630  clwwlkccatlem  16641  clwwlkn1loopb  16661  clwwlkext2edg  16663  clwwlknonex2lem1  16678  clwwlknonex2  16680  trlsegvdeglem2  16702  trlsegvdeglem3  16703  eupth2lem3lem4fi  16714  eupth2lemsfi  16719  fnmptd  16832  bj-sels  16940  bj-nnelon  16985  pw1map  17025  pwle2  17028  pwf1oexmid  17029  pw1nct  17033  stnot  17039  nninfall  17052  nninfsellemdc  17053  nninfself  17056  nnnninfex  17065  nninfnfiinf  17066  refeq  17073  isomninnlem  17079  cvgcmp2nlemabs  17081  trilpolemlt1  17090  trirec0  17093  apdifflemf  17095  apdifflemr  17096  apdiff  17097  qdiff  17098  iswomninnlem  17099  iswomni0  17101  ismkvnnlem  17102  reap0  17108  cndcap  17109