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  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  5829  fncofn  5831  ftpg  5837  fconst2g  5868  funfvima3  5887  elabrexg  5898  foeqcnvco  5930  f1eqcocnv  5931  fliftfun  5936  fliftfund  5937  fliftval  5940  riota5f  5997  f1ofveu  6005  f1ocnvd  6224  f1opw2  6228  off  6247  offval2  6250  ofrfval2  6251  offveq  6255  caofref  6259  caofinvl  6260  elxp6  6331  cnvf1olem  6388  f2ndf  6390  f1od2  6399  elmpom  6402  tposf12  6434  smores2  6459  tfrlemisucaccv  6490  tfrlemibfn  6493  tfr1onlemsucaccv  6506  tfr1onlembfn  6509  tfrcllemsucaccv  6519  tfrcllembfn  6522  tfrcl  6529  tfri3  6532  frecabcl  6564  nnsucsssuc  6659  ersym  6713  ertr  6716  swoer  6729  erth  6747  riinerm  6776  qliftfund  6786  eroprf  6796  ecopoverg  6804  th3qlem1  6805  elmapssres  6841  mapss  6859  fdiagfn  6860  ixpssmap2g  6895  mapsnf1o  6905  f1oen4g  6924  f1dom4g  6925  f1dom2g  6928  dom3d  6946  en2prd  6991  dom1oi  7002  pw2f1odclem  7019  fopwdom  7021  mapxpen  7033  nndomo  7049  dif1en  7067  findcard2  7077  findcard2s  7078  diffisn  7081  fimax2gtrilemstep  7089  eqsndc  7094  fientri3  7106  tpfidceq  7121  fiintim  7122  opabfi  7131  f1dmvrnfibi  7142  sbthlemi6  7160  elfir  7171  fifo  7178  supelti  7200  supsnti  7203  cnvinfex  7216  ordiso2  7233  updjud  7280  djudom  7291  difinfsn  7298  ctssdc  7311  enumctlemm  7312  enumct  7313  nninfninc  7321  enomnilem  7336  fodjuf  7343  ismkvnex  7353  omnimkv  7354  enmkvlem  7359  enwomnilem  7367  nninfdcinf  7369  nninfwlporlem  7371  isnumi  7385  exmidfodomrlemrALT  7413  finacn  7418  djudoml  7433  djudomr  7434  netap  7472  2omotaplemap  7475  2omotaplemst  7476  exmidapne  7478  cc2lem  7484  cc3  7486  ltsopi  7539  pitri3or  7541  ltdcpi  7542  indpi  7561  enqdc  7580  enqdc1  7581  addcmpblnq  7586  mulcanenq  7604  recrecnq  7613  nqtri3or  7615  ltdcnq  7616  ltsonq  7617  ltaddnq  7626  subhalfnqq  7633  archnqq  7636  prarloclemarch2  7638  enq0tr  7653  nqnq0  7660  addcmpblnq0  7662  mulcanenq0ec  7664  nnnq0lem1  7665  nqpnq0nq  7672  nq0m0r  7675  nq02m  7684  prarloclemlt  7712  prarloclemcalc  7721  addlocpr  7755  nqprl  7770  nqpru  7771  addnqprlemrl  7776  addnqprlemru  7777  prmuloclemcalc  7784  mullocprlem  7789  mulnqprlemrl  7792  mulnqprlemru  7793  1idprl  7809  1idpru  7810  ltaddpr  7816  ltexprlemm  7819  ltexprlemopl  7820  ltexprlemopu  7822  ltexprlemdisj  7825  ltexprlemrl  7829  ltexprlemru  7831  addcanprleml  7833  addcanprlemu  7834  addcanprg  7835  prplnqu  7839  recexprlemloc  7850  recexprlem1ssl  7852  recexprlem1ssu  7853  aptiprleml  7858  aptiprlemu  7859  archpr  7862  cauappcvgprlemm  7864  cauappcvgprlemopl  7865  cauappcvgprlemloc  7871  cauappcvgprlemladdfu  7873  cauappcvgprlemladdfl  7874  cauappcvgprlem1  7878  cauappcvgprlem2  7879  caucvgprlemnkj  7885  caucvgprlemopl  7888  caucvgprlemloc  7894  caucvgprlemladdfu  7896  caucvgprlem2  7899  caucvgprprlemnkltj  7908  caucvgprprlemopl  7916  caucvgprprlemloc  7922  caucvgprprlemexbt  7925  caucvgprprlemaddq  7927  caucvgprprlem2  7929  suplocexprlemmu  7937  suplocexprlemru  7938  suplocexprlemloc  7940  suplocexprlemlub  7943  prsrlem1  7961  0idsr  7986  1idsr  7987  recexgt0sr  7992  archsr  8001  prsradd  8005  caucvgsrlemcau  8012  caucvgsrlembound  8013  caucvgsrlemoffgt1  8018  suplocsrlemb  8025  suplocsrlempr  8026  suplocsrlem  8027  pitonnlem1p1  8065  pitonn  8067  pitoregt0  8068  peano2nnnn  8072  recidpirq  8077  axcaucvglemval  8116  leid  8262  nltled  8299  readdcan  8318  addneintrd  8366  addneintr2d  8367  pncan  8384  subsub2  8406  subsub4  8411  negned  8486  subne0d  8498  subneintrd  8533  subneintr2d  8535  subeq0bd  8557  subdi  8563  gt0add  8752  rimul  8764  rereim  8765  ltmul1a  8770  apreim  8782  apirr  8784  mulap0r  8794  msqge0  8795  mulge0  8798  gt0ap0  8805  ltap  8812  subap0d  8823  recexaplem2  8831  mulap0bad  8838  mulap0bbd  8839  mul0eqap  8849  divrecap  8867  div0ap  8881  div1  8882  recrecap  8888  divdivdivap  8892  ddcanap  8905  rerecclap  8909  div2negap  8914  diveqap1bd  9015  recgt0  9029  prodgt0  9031  lemul1a  9037  recp1lt1  9078  squeeze0  9083  peano2nn  9154  div4p1lem1div2  9397  arch  9398  peano2z  9514  peano2zm  9516  ztri3or  9521  nn0n0n1ge2  9549  zextle  9570  gtndiv  9574  suprzclex  9577  nn0ind-raph  9596  uzid  9769  uzneg  9774  uztric  9777  uz11  9778  eluzp1l  9780  qdivcl  9876  irrmul  9880  irrmulap  9881  rpnegap  9920  negelrpd  9922  ledivge1le  9960  mul2lt0rlt0  9993  mul2lt0rgt0  9994  nn0ledivnn  10001  ltpnf  10014  mnflt  10017  pnfge  10023  mnfle  10026  xrlttr  10029  xrltso  10030  xrlttri3  10031  xrleid  10034  xaddass2  10104  xltadd1  10110  xlt2add  10114  xleaddadd  10121  iccf1o  10238  fztri3or  10273  fznlem  10275  fzn  10276  fzsplit2  10284  fznatpl1  10310  uzsplit  10326  fseq1p1m1  10328  fzm1  10334  fznn0sub2  10362  difelfznle  10369  1fv  10373  fzodcel  10387  fzospliti  10412  fzouzsplit  10415  eluzgtdifelfzo  10441  exfzdc  10485  subfzo0  10487  zsupcllemstep  10488  zsupcl  10490  zssinfcl  10491  infssuzex  10492  infssuzcldc  10494  suprzubdc  10495  nninfdcex  10496  qdcle  10505  exbtwnz  10509  qbtwnrelemcalc  10514  flqlelt  10535  qfraclt1  10539  qfracge0  10540  flqltnz  10546  btwnzge0  10559  flhalf  10561  fldiv4lem1div2uz2  10565  ceiqle  10574  intfracq  10581  mulqmod0  10591  modqge0  10593  modqlt  10594  modqid  10610  modqid0  10611  m1modge3gt1  10632  modqltm1p1mod  10637  q2txmodxeq0  10645  modaddmodlo  10649  modsumfzodifsn  10657  addmodlteq  10659  frecuzrdgtcl  10673  frecuzrdgtclt  10682  uzennn  10697  uzsinds  10705  seqf  10725  seqf2  10729  monoord2  10747  iseqf1olemqk  10768  iseqf1olemjpcl  10769  iseqf1olemqpcl  10770  seq3f1olemqsumkj  10772  seq3f1olemqsum  10774  seq3f1olemstep  10775  seq3f1oleml  10777  seqf1oglem1  10780  ser3le  10798  exp3vallem  10801  exp3val  10802  expp1  10807  expcllem  10811  ltexp2a  10852  leexp2a  10853  nn0ltexp2  10970  faclbnd  11002  faclbnd2  11003  faclbnd3  11004  bcval5  11024  bcpasc  11027  hashennn  11041  fihasheqf1oi  11048  hashsng  11059  fihashfn  11062  hashun  11067  fihashss  11079  fihashssdif  11081  hashfz  11084  hashxp  11089  fimaxq  11090  zfz1isolem1  11103  seq3coll  11105  hashdmprop2dom  11107  wrdf  11118  wrdlenge2n0  11148  fstwrdne0  11152  wrdred1hash  11156  ccatvalfn  11177  ccatsymb  11178  ccatlid  11182  ccatrid  11183  ccatrn  11185  ccatalpha  11189  eqs1  11204  ccats1val2  11216  fzowrddc  11227  swrdlen  11232  swrdnd  11239  swrd0g  11240  swrdfv2  11243  swrdwrdsymbg  11244  pfxn0  11268  pfxwrdsymbg  11270  pfxsuff1eqwrdeq  11279  swrdswrd  11285  ccats1pfxeq  11294  ccats1pfxeqrex  11295  wrdind  11302  wrd2ind  11303  swrdccatin1  11305  pfxccatin12lem4  11306  swrdccatin2  11309  pfxccatin12  11313  pfxccat3a  11318  swrdccat3blem  11319  pfxccatid  11321  swrdccatin2d  11324  shftfn  11384  cjth  11406  cjmulrcl  11447  reim0bd  11504  rerebd  11505  cjrebd  11506  caucvgre  11541  cvg1nlemcxze  11542  cvg1nlemcau  11544  cvg1nlemres  11545  recvguniq  11555  resqrexlemover  11570  resqrexlemdec  11571  resqrexlemgt0  11580  resqrexlemoverl  11581  resqrexlemglsq  11582  rersqrtthlem  11590  sqrtgt0  11594  leabs  11634  absexpzap  11640  absle  11649  recvalap  11657  abstri  11664  abs2dif  11666  amgm2  11678  absne0d  11747  maxleim  11765  maxabslemab  11766  maxabslemlub  11767  maxltsup  11778  zmaxcl  11784  fimaxre2  11787  minmax  11790  rpmincl  11798  bdtrilem  11799  bdtri  11800  xrmaxleim  11804  xrmaxiflemcom  11809  xrmaxltsup  11818  xrmaxadd  11821  xrminmax  11825  xrminrpcl  11834  climconst  11850  climuni  11853  2clim  11861  climcn1  11868  climcn2  11869  reccn2ap  11873  climge0  11885  climle  11894  climsqz  11895  climsqz2  11896  serf0  11912  summodclem3  11940  summodclem2a  11941  fsumcl2lem  11958  sumpr  11973  sumtp  11974  fsum0diaglem  12000  mptfzshft  12002  fsumle  12023  fsumlt  12024  divcnv  12057  trireciplem  12060  expcnvap0  12062  expcnv  12064  explecnv  12065  geosergap  12066  cvgratnnlembern  12083  cvgratnnlemabsle  12087  cvgratnnlemsumlt  12088  cvgratz  12092  cvgratgt0  12093  mertenslemi1  12095  mertenslem2  12096  mertensabs  12097  clim2divap  12100  prodmodclem3  12135  prodmodclem2a  12136  fprodseq  12143  fprodmul  12151  fprodfac  12175  fprodconst  12180  fprodap0  12181  fprodap0f  12196  fprodle  12200  eftcl  12214  ef0lem  12220  efsub  12241  eftlub  12250  eflegeo  12261  tanval2ap  12273  sinadd  12296  cos2t  12310  cos2tsin  12311  sin01bnd  12317  cos01bnd  12318  eirraplem  12337  dvdsval2  12350  dvdsdc  12358  dvds0lem  12361  zdvdsdc  12372  dvdscmulr  12380  dvdsmulcr  12381  fsumdvds  12402  dvdslelemd  12403  divconjdvds  12409  dvdsext  12415  fzm1ndvds  12416  dvdsmod  12422  3dvds  12424  oexpneg  12437  2tp1odd  12444  mulsucdiv2z  12445  2teven  12447  zeo5  12448  opeo  12457  omeo  12458  nn0ob  12468  divalglemnqt  12480  bitsdc  12507  bits0o  12510  bitsfzolem  12514  bitsfzo  12515  bitsmod  12516  bitscmp  12518  bitsinv1lem  12521  gcddvds  12533  dvdslegcd  12534  gcdneg  12552  bezoutlemnewy  12566  bezoutlemstep  12567  bezoutlema  12569  bezoutlemb  12570  bezoutlemmo  12576  bezoutlemle  12578  bezoutlemsup  12579  dfgcd3  12580  bezout  12581  dfgcd2  12584  uzwodc  12607  lcmcllem  12638  lcmneg  12645  lcmgcdlem  12648  lcmdvds  12650  lcmid  12651  3lcm2e6woprm  12657  6lcm4e12  12658  ncoprmgcdne1b  12660  mulgcddvds  12665  divgcdcoprmex  12673  cncongr1  12674  cncongr2  12675  isprm2lem  12687  prmind2  12691  dvdsnprmd  12696  prm2orodd  12697  sqnprm  12707  isprm5lem  12712  rpexp  12724  sqrt2irrlem  12732  oddpwdclemdc  12744  sqrt2irraplemnn  12750  qnumdencoprm  12764  qeqnumdivden  12765  nn0gcdsq  12771  nn0sqrtelqelz  12777  nonsq  12778  phicl2  12785  phibnd  12788  hashdvds  12792  phiprmpw  12793  phimullem  12796  eulerthlemrprm  12800  eulerthlema  12801  eulerthlemth  12803  prmdiveq  12807  hashgcdlem  12809  odzdvds  12817  modprminv  12821  nnnn0modprm0  12827  modprmn0modprm0  12828  pythagtriplem10  12841  pythagtriplem19  12854  pythagtrip  12855  pcpre1  12864  pcpremul  12865  pceu  12867  pcmul  12873  pcdiv  12874  pcqmul  12875  pcqdiv  12879  pcexp  12881  pcdvdsb  12892  pcidlem  12895  pcdvdstr  12899  pcgcd1  12900  pc2dvds  12902  pcprmpw2  12905  difsqpwdvds  12910  pcaddlem  12911  pcadd  12912  pcadd2  12913  pcmpt  12915  pcmptdvds  12917  pcprod  12918  fldivp1  12920  pcfaclem  12921  pcfac  12922  pcbc  12923  qexpz  12924  pockthlem  12928  pockthg  12929  1arithlem4  12938  1arith  12939  1arith2  12940  4sqlem6  12955  4sqlem8  12957  4sqlem9  12958  4sqlem10  12959  4sqexercise1  12970  4sqexercise2  12971  4sqlemsdc  12972  4sqlem11  12973  4sqlem12  12974  4sqlem15  12977  4sqlem16  12978  4sqlem17  12979  znnen  13018  ennnfonelemk  13020  ennnfonelemkh  13032  ennnfonelemhf1o  13033  ennnfonelemrnh  13036  ennnfonelemfun  13037  ennnfonelemf1  13038  ennnfonelemrn  13039  ennnfonelemnn0  13042  ctinfomlemom  13047  ctiunctlemudc  13057  unct  13062  omctfn  13063  ssnnctlemct  13066  nninfdclemp1  13070  nninfdc  13073  structfung  13098  setsfun  13116  setsfun0  13117  setscom  13121  strslfv3  13127  setsslid  13132  pwsdiagel  13379  pwssnf1o  13380  imasaddfnlemg  13396  imasaddvallemg  13397  mgmsscl  13443  plusffng  13447  mgmplusf  13448  mgm0  13451  mgm1  13452  opifismgmdc  13453  gsumfzval  13473  gsumprval  13481  sgrp1  13493  issgrpd  13494  prdsplusgsgrpcl  13496  mndpfo  13520  mndfo  13521  prdsplusgcl  13528  prdsidlem  13529  mnd1  13537  0subm  13566  mhmima  13573  grpinvfng  13626  isgrpinv  13636  grpinvid  13642  grpinvf1o  13652  grpinvadd  13660  grpsubf  13661  grpsubsub4  13675  grplactcnv  13684  grp1  13688  grp1inv  13689  prdsinvlem  13690  prdsinvgd  13692  qusgrp2  13699  mulgfng  13710  subginv  13767  resgrpisgrp  13781  subgintm  13784  0subg  13785  0nsg  13800  qusinv  13822  ghminv  13836  ghmrn  13843  ghmeql  13853  ghmnsgima  13854  kerf1ghm  13860  conjnmz  13865  rngass  13951  rngmneg1  13959  rngmneg2  13960  qusrng  13970  srgideu  13984  srgidmlem  13990  srgpcomp  14002  srg1expzeq1  14007  ringcl  14025  ringideu  14029  ringidmlem  14034  ringnegl  14063  ringnegr  14064  ring1  14071  qusring2  14078  opprringbg  14092  dvdsrd  14107  dvdsr01  14117  isunitd  14119  unitinvcl  14136  unitinvinv  14137  unitnegcl  14143  rhmmul  14177  rhmf1o  14181  nzrunit  14201  lringuplu  14209  subrngintm  14225  subrgsubm  14247  subrgintm  14256  aprsym  14297  scaffng  14322  lmodscaf  14323  lsssn0  14383  lss1d  14396  lssintclm  14397  lspval  14403  lspcl  14404  lspsnid  14420  lspprid1  14424  lspsn  14429  sraval  14450  rspcl  14504  rspssid  14505  rspssp  14507  rnglidlmmgm  14509  rnglidlmsgrp  14510  cnfldneg  14586  zringinvg  14617  expghmap  14620  znzrhfo  14661  znf1o  14664  znhash  14669  znidomb  14671  znrrg  14673  psrbagfi  14686  psraddcl  14693  psr0cl  14694  psrnegcl  14696  psrneg  14700  psr1clfi  14701  mplsubgfilemm  14711  mplsubgfilemcl  14712  baspartn  14773  eltg3i  14779  tgclb  14788  topbas  14790  2basgeng  14805  topcld  14832  0cld  14835  uncld  14836  neif  14864  elnei  14875  0nei  14889  restbasg  14891  iscnp4  14941  cnpnei  14942  cnclima  14946  cncnp  14953  cnrest2r  14960  cndis  14964  lmff  14972  lmtopcnp  14973  txbas  14981  txopn  14988  txcnp  14994  upxp  14995  txdis1cn  15001  cnmpt11  15006  cnmpt21  15014  psmetge0  15054  xmetge0  15088  xmettpos  15093  xmetrtri  15099  metrtri  15100  xblpnfps  15121  xblpnf  15122  blfps  15132  blf  15133  ssblps  15148  ssbl  15149  blbas  15156  metss2  15221  xmettxlem  15232  xmettx  15233  qtopbas  15245  divcnap  15288  cncfss  15306  cdivcncfap  15327  expcncf  15332  cnopnap  15334  maxcncf  15338  mincncf  15339  dedekindeulemuub  15340  dedekindeulemlu  15344  dedekindeu  15346  suplociccex  15348  dedekindicclemuub  15349  dedekindicclemlu  15353  dedekindicclemicc  15355  ivthinclemlopn  15359  ivthinclemuopn  15361  ivthinc  15366  ivthreinc  15368  hoverlt1  15372  ellimc3apf  15383  limcimolemlt  15387  limcimo  15388  limcresi  15389  cnplimclemle  15391  reldvg  15402  dvfgg  15411  dvidlemap  15414  dvidrelem  15415  dvidsslem  15416  dvcjbr  15431  dvcj  15432  dvrecap  15436  dveflem  15449  dvef  15450  elply2  15458  elplyr  15463  plycj  15484  plyreres  15487  reeff1oleme  15495  pilem3  15506  sinq34lt0t  15554  cosq14gt0  15555  coseq0q4123  15557  tangtx  15561  sincosq1eq  15562  cosordlem  15572  logdivlti  15604  relogbval  15674  relogbzcl  15675  nnlogbexp  15682  logbgcd1irr  15690  logbgcd1irraplemexp  15691  logbgcd1irraplemap  15692  wilthlem1  15703  mpodvdsmulf1o  15713  mersenne  15720  perfectlem2  15723  perfect  15724  zabsle1  15727  lgslem1  15728  lgsval  15732  lgsfvalg  15733  lgsfcl2  15734  lgsval2lem  15738  lgscl1  15751  lgsmod  15754  lgsdir2lem5  15760  lgsdir2  15761  lgsdilem2  15764  lgsdi  15765  lgsne0  15766  gausslemma2dlem0c  15779  gausslemma2dlem0h  15784  gausslemma2dlem1a  15786  gausslemma2dlem1f1o  15788  gausslemma2dlem3  15791  lgseisenlem1  15798  lgseisenlem2  15799  lgseisenlem3  15800  lgseisenlem4  15801  lgseisen  15802  lgsquadlem1  15805  lgsquadlem2  15806  lgsquadlem3  15807  lgsquad3  15812  2lgslem3b1  15826  2lgslem3c1  15827  2lgs  15832  2lgsoddprmlem2  15834  2lgsoddprm  15841  2sqlem3  15845  2sqlem8  15851  2sqlem10  15853  structgrssvtx  15892  structgrssiedg  15893  ushgruhgr  15930  uhgrun  15936  incistruhgr  15940  upgrop  15954  upgruhgr  15961  umgrupgr  15962  umgrnloopv  15964  umgredgprv  15965  umgr0e  15968  upgr1edc  15971  umgr1een  15975  upgrun  15976  umgrun  15978  umgrislfupgrdom  15981  upgredg  15994  umgrpredgv  15997  usgrop  16016  usgrausgrien  16019  ausgrumgrien  16020  ausgrusgrien  16021  uspgrupgrushgr  16032  usgrumgr  16034  usgrumgruspgr  16035  usgruspgrben  16036  usgrislfuspgrdom  16040  edgssv2en  16049  usgrf1oedg  16055  usgredg4  16065  usgredg2vlem2  16073  usgredg2v  16074  ushgredgedg  16076  ushgredgedgloop  16078  usgrstrrepeen  16081  usgr0e  16082  uhgr0v0e  16084  uspgr1edc  16090  usgr1e  16091  griedg0ssusgr  16101  subgrprop3  16112  subgruhgredgdm  16120  subuhgr  16122  subupgr  16123  subumgr  16124  subusgr  16125  uhgrspansubgrlem  16126  1loopgrvd2fi  16155  1loopgrvd0fi  16156  1hevtxdg0fi  16157  vdegp1aid  16164  vdegp1bid  16165  wlkm  16189  wlkvtxiedg  16195  wlkvtxiedgg  16196  wlkeq  16204  wlk1walkdom  16209  uspgr2wlkeq  16215  uspgr2wlkeqi  16217  upgr2wlkdc  16227  wlkres  16229  trlreslem  16239  clwwlkccatlem  16250  clwwlkn1loopb  16270  clwwlkext2edg  16272  clwwlknonex2lem1  16287  clwwlknonex2  16289  trlsegvdeglem2  16311  trlsegvdeglem3  16312  fnmptd  16400  bj-sels  16509  bj-nnelon  16554  2omap  16594  pw1map  16596  pwle2  16599  pwf1oexmid  16600  pw1nct  16604  nninfall  16611  nninfsellemdc  16612  nninfself  16615  nnnninfex  16624  nninfnfiinf  16625  refeq  16632  isomninnlem  16634  cvgcmp2nlemabs  16636  trilpolemlt1  16645  trirec0  16648  apdifflemf  16650  apdifflemr  16651  apdiff  16652  iswomninnlem  16653  iswomni0  16655  ismkvnnlem  16656  reap0  16662  cndcap  16663  gfsumval  16680  gsumgfsumlem  16683  gsumgfsum  16684