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  711  pm4.55dc  944  mpbir2and  950  pm3.12dc  964  mpbir3and  1204  pm5.15dc  1431  eqeltrd  2306  eqnetrd  2424  3netr4d  2433  r19.30dc  2678  raleqtrrdv  2738  rexeqtrrdv  2739  sbcne12g  3143  eqsstrd  3261  3sstr4d  3270  eqbrtrd  4108  3brtr4d  4118  snelpwi  4301  prelpwi  4304  pwel  4308  ordelon  4478  onin  4481  elelsuc  4504  onsuc  4597  onsucb  4599  onintonm  4613  omsinds  4718  sosng  4797  relssdv  4816  eqbrrdv  4821  eqrelrdv2  4823  relsnopg  4828  breldmg  4935  elrnmptdv  4984  iss  5057  xpimasn  5183  elxp4  5222  elxp5  5223  iotam  5316  funssres  5366  f0rn0  5528  fimadmfo  5565  sefvex  5656  fdmeu  5685  fvun1  5708  eqfnfvd  5743  fvimacnvi  5757  fvimacnv  5758  fvelrn  5774  fmpt3d  5799  fmpt2d  5805  resflem  5807  fmptco  5809  fsn  5815  funopsn  5825  fncofn  5827  ftpg  5833  fconst2g  5864  funfvima3  5883  elabrexg  5894  foeqcnvco  5926  f1eqcocnv  5927  fliftfun  5932  fliftfund  5933  fliftval  5936  riota5f  5993  f1ofveu  6001  f1ocnvd  6220  f1opw2  6224  off  6243  offval2  6246  ofrfval2  6247  offveq  6251  caofref  6255  caofinvl  6256  elxp6  6327  cnvf1olem  6384  f2ndf  6386  f1od2  6395  elmpom  6398  tposf12  6430  smores2  6455  tfrlemisucaccv  6486  tfrlemibfn  6489  tfr1onlemsucaccv  6502  tfr1onlembfn  6505  tfrcllemsucaccv  6515  tfrcllembfn  6518  tfrcl  6525  tfri3  6528  frecabcl  6560  nnsucsssuc  6655  ersym  6709  ertr  6712  swoer  6725  erth  6743  riinerm  6772  qliftfund  6782  eroprf  6792  ecopoverg  6800  th3qlem1  6801  elmapssres  6837  mapss  6855  fdiagfn  6856  ixpssmap2g  6891  mapsnf1o  6901  f1oen4g  6920  f1dom4g  6921  f1dom2g  6924  dom3d  6942  en2prd  6987  dom1oi  6998  pw2f1odclem  7015  fopwdom  7017  mapxpen  7029  nndomo  7045  dif1en  7063  findcard2  7073  findcard2s  7074  diffisn  7077  fimax2gtrilemstep  7085  eqsndc  7090  fientri3  7102  tpfidceq  7117  fiintim  7118  opabfi  7126  f1dmvrnfibi  7137  sbthlemi6  7155  elfir  7166  fifo  7173  supelti  7195  supsnti  7198  cnvinfex  7211  ordiso2  7228  updjud  7275  djudom  7286  difinfsn  7293  ctssdc  7306  enumctlemm  7307  enumct  7308  nninfninc  7316  enomnilem  7331  fodjuf  7338  ismkvnex  7348  omnimkv  7349  enmkvlem  7354  enwomnilem  7362  nninfdcinf  7364  nninfwlporlem  7366  isnumi  7380  exmidfodomrlemrALT  7407  finacn  7412  djudoml  7427  djudomr  7428  netap  7466  2omotaplemap  7469  2omotaplemst  7470  exmidapne  7472  cc2lem  7478  cc3  7480  ltsopi  7533  pitri3or  7535  ltdcpi  7536  indpi  7555  enqdc  7574  enqdc1  7575  addcmpblnq  7580  mulcanenq  7598  recrecnq  7607  nqtri3or  7609  ltdcnq  7610  ltsonq  7611  ltaddnq  7620  subhalfnqq  7627  archnqq  7630  prarloclemarch2  7632  enq0tr  7647  nqnq0  7654  addcmpblnq0  7656  mulcanenq0ec  7658  nnnq0lem1  7659  nqpnq0nq  7666  nq0m0r  7669  nq02m  7678  prarloclemlt  7706  prarloclemcalc  7715  addlocpr  7749  nqprl  7764  nqpru  7765  addnqprlemrl  7770  addnqprlemru  7771  prmuloclemcalc  7778  mullocprlem  7783  mulnqprlemrl  7786  mulnqprlemru  7787  1idprl  7803  1idpru  7804  ltaddpr  7810  ltexprlemm  7813  ltexprlemopl  7814  ltexprlemopu  7816  ltexprlemdisj  7819  ltexprlemrl  7823  ltexprlemru  7825  addcanprleml  7827  addcanprlemu  7828  addcanprg  7829  prplnqu  7833  recexprlemloc  7844  recexprlem1ssl  7846  recexprlem1ssu  7847  aptiprleml  7852  aptiprlemu  7853  archpr  7856  cauappcvgprlemm  7858  cauappcvgprlemopl  7859  cauappcvgprlemloc  7865  cauappcvgprlemladdfu  7867  cauappcvgprlemladdfl  7868  cauappcvgprlem1  7872  cauappcvgprlem2  7873  caucvgprlemnkj  7879  caucvgprlemopl  7882  caucvgprlemloc  7888  caucvgprlemladdfu  7890  caucvgprlem2  7893  caucvgprprlemnkltj  7902  caucvgprprlemopl  7910  caucvgprprlemloc  7916  caucvgprprlemexbt  7919  caucvgprprlemaddq  7921  caucvgprprlem2  7923  suplocexprlemmu  7931  suplocexprlemru  7932  suplocexprlemloc  7934  suplocexprlemlub  7937  prsrlem1  7955  0idsr  7980  1idsr  7981  recexgt0sr  7986  archsr  7995  prsradd  7999  caucvgsrlemcau  8006  caucvgsrlembound  8007  caucvgsrlemoffgt1  8012  suplocsrlemb  8019  suplocsrlempr  8020  suplocsrlem  8021  pitonnlem1p1  8059  pitonn  8061  pitoregt0  8062  peano2nnnn  8066  recidpirq  8071  axcaucvglemval  8110  leid  8256  nltled  8293  readdcan  8312  addneintrd  8360  addneintr2d  8361  pncan  8378  subsub2  8400  subsub4  8405  negned  8480  subne0d  8492  subneintrd  8527  subneintr2d  8529  subeq0bd  8551  subdi  8557  gt0add  8746  rimul  8758  rereim  8759  ltmul1a  8764  apreim  8776  apirr  8778  mulap0r  8788  msqge0  8789  mulge0  8792  gt0ap0  8799  ltap  8806  subap0d  8817  recexaplem2  8825  mulap0bad  8832  mulap0bbd  8833  mul0eqap  8843  divrecap  8861  div0ap  8875  div1  8876  recrecap  8882  divdivdivap  8886  ddcanap  8899  rerecclap  8903  div2negap  8908  diveqap1bd  9009  recgt0  9023  prodgt0  9025  lemul1a  9031  recp1lt1  9072  squeeze0  9077  peano2nn  9148  div4p1lem1div2  9391  arch  9392  peano2z  9508  peano2zm  9510  ztri3or  9515  nn0n0n1ge2  9543  zextle  9564  gtndiv  9568  suprzclex  9571  nn0ind-raph  9590  uzid  9763  uzneg  9768  uztric  9771  uz11  9772  eluzp1l  9774  qdivcl  9870  irrmul  9874  irrmulap  9875  rpnegap  9914  negelrpd  9916  ledivge1le  9954  mul2lt0rlt0  9987  mul2lt0rgt0  9988  nn0ledivnn  9995  ltpnf  10008  mnflt  10011  pnfge  10017  mnfle  10020  xrlttr  10023  xrltso  10024  xrlttri3  10025  xrleid  10028  xaddass2  10098  xltadd1  10104  xlt2add  10108  xleaddadd  10115  iccf1o  10232  fztri3or  10267  fznlem  10269  fzn  10270  fzsplit2  10278  fznatpl1  10304  uzsplit  10320  fseq1p1m1  10322  fzm1  10328  fznn0sub2  10356  difelfznle  10363  1fv  10367  fzodcel  10381  fzospliti  10406  fzouzsplit  10409  eluzgtdifelfzo  10435  exfzdc  10479  subfzo0  10481  zsupcllemstep  10482  zsupcl  10484  zssinfcl  10485  infssuzex  10486  infssuzcldc  10488  suprzubdc  10489  nninfdcex  10490  qdcle  10499  exbtwnz  10503  qbtwnrelemcalc  10508  flqlelt  10529  qfraclt1  10533  qfracge0  10534  flqltnz  10540  btwnzge0  10553  flhalf  10555  fldiv4lem1div2uz2  10559  ceiqle  10568  intfracq  10575  mulqmod0  10585  modqge0  10587  modqlt  10588  modqid  10604  modqid0  10605  m1modge3gt1  10626  modqltm1p1mod  10631  q2txmodxeq0  10639  modaddmodlo  10643  modsumfzodifsn  10651  addmodlteq  10653  frecuzrdgtcl  10667  frecuzrdgtclt  10676  uzennn  10691  uzsinds  10699  seqf  10719  seqf2  10723  monoord2  10741  iseqf1olemqk  10762  iseqf1olemjpcl  10763  iseqf1olemqpcl  10764  seq3f1olemqsumkj  10766  seq3f1olemqsum  10768  seq3f1olemstep  10769  seq3f1oleml  10771  seqf1oglem1  10774  ser3le  10792  exp3vallem  10795  exp3val  10796  expp1  10801  expcllem  10805  ltexp2a  10846  leexp2a  10847  nn0ltexp2  10964  faclbnd  10996  faclbnd2  10997  faclbnd3  10998  bcval5  11018  bcpasc  11021  hashennn  11035  fihasheqf1oi  11042  hashsng  11053  fihashfn  11056  hashun  11061  fihashss  11073  fihashssdif  11075  hashfz  11078  hashxp  11083  fimaxq  11084  zfz1isolem1  11097  seq3coll  11099  hashdmprop2dom  11101  wrdf  11112  wrdlenge2n0  11142  fstwrdne0  11146  wrdred1hash  11150  ccatvalfn  11171  ccatsymb  11172  ccatlid  11176  ccatrid  11177  ccatrn  11179  ccatalpha  11183  eqs1  11198  ccats1val2  11210  fzowrddc  11221  swrdlen  11226  swrdnd  11233  swrd0g  11234  swrdfv2  11237  swrdwrdsymbg  11238  pfxn0  11262  pfxwrdsymbg  11264  pfxsuff1eqwrdeq  11273  swrdswrd  11279  ccats1pfxeq  11288  ccats1pfxeqrex  11289  wrdind  11296  wrd2ind  11297  swrdccatin1  11299  pfxccatin12lem4  11300  swrdccatin2  11303  pfxccatin12  11307  pfxccat3a  11312  swrdccat3blem  11313  pfxccatid  11315  swrdccatin2d  11318  shftfn  11378  cjth  11400  cjmulrcl  11441  reim0bd  11498  rerebd  11499  cjrebd  11500  caucvgre  11535  cvg1nlemcxze  11536  cvg1nlemcau  11538  cvg1nlemres  11539  recvguniq  11549  resqrexlemover  11564  resqrexlemdec  11565  resqrexlemgt0  11574  resqrexlemoverl  11575  resqrexlemglsq  11576  rersqrtthlem  11584  sqrtgt0  11588  leabs  11628  absexpzap  11634  absle  11643  recvalap  11651  abstri  11658  abs2dif  11660  amgm2  11672  absne0d  11741  maxleim  11759  maxabslemab  11760  maxabslemlub  11761  maxltsup  11772  zmaxcl  11778  fimaxre2  11781  minmax  11784  rpmincl  11792  bdtrilem  11793  bdtri  11794  xrmaxleim  11798  xrmaxiflemcom  11803  xrmaxltsup  11812  xrmaxadd  11815  xrminmax  11819  xrminrpcl  11828  climconst  11844  climuni  11847  2clim  11855  climcn1  11862  climcn2  11863  reccn2ap  11867  climge0  11879  climle  11888  climsqz  11889  climsqz2  11890  serf0  11906  summodclem3  11934  summodclem2a  11935  fsumcl2lem  11952  sumpr  11967  sumtp  11968  fsum0diaglem  11994  mptfzshft  11996  fsumle  12017  fsumlt  12018  divcnv  12051  trireciplem  12054  expcnvap0  12056  expcnv  12058  explecnv  12059  geosergap  12060  cvgratnnlembern  12077  cvgratnnlemabsle  12081  cvgratnnlemsumlt  12082  cvgratz  12086  cvgratgt0  12087  mertenslemi1  12089  mertenslem2  12090  mertensabs  12091  clim2divap  12094  prodmodclem3  12129  prodmodclem2a  12130  fprodseq  12137  fprodmul  12145  fprodfac  12169  fprodconst  12174  fprodap0  12175  fprodap0f  12190  fprodle  12194  eftcl  12208  ef0lem  12214  efsub  12235  eftlub  12244  eflegeo  12255  tanval2ap  12267  sinadd  12290  cos2t  12304  cos2tsin  12305  sin01bnd  12311  cos01bnd  12312  eirraplem  12331  dvdsval2  12344  dvdsdc  12352  dvds0lem  12355  zdvdsdc  12366  dvdscmulr  12374  dvdsmulcr  12375  fsumdvds  12396  dvdslelemd  12397  divconjdvds  12403  dvdsext  12409  fzm1ndvds  12410  dvdsmod  12416  3dvds  12418  oexpneg  12431  2tp1odd  12438  mulsucdiv2z  12439  2teven  12441  zeo5  12442  opeo  12451  omeo  12452  nn0ob  12462  divalglemnqt  12474  bitsdc  12501  bits0o  12504  bitsfzolem  12508  bitsfzo  12509  bitsmod  12510  bitscmp  12512  bitsinv1lem  12515  gcddvds  12527  dvdslegcd  12528  gcdneg  12546  bezoutlemnewy  12560  bezoutlemstep  12561  bezoutlema  12563  bezoutlemb  12564  bezoutlemmo  12570  bezoutlemle  12572  bezoutlemsup  12573  dfgcd3  12574  bezout  12575  dfgcd2  12578  uzwodc  12601  lcmcllem  12632  lcmneg  12639  lcmgcdlem  12642  lcmdvds  12644  lcmid  12645  3lcm2e6woprm  12651  6lcm4e12  12652  ncoprmgcdne1b  12654  mulgcddvds  12659  divgcdcoprmex  12667  cncongr1  12668  cncongr2  12669  isprm2lem  12681  prmind2  12685  dvdsnprmd  12690  prm2orodd  12691  sqnprm  12701  isprm5lem  12706  rpexp  12718  sqrt2irrlem  12726  oddpwdclemdc  12738  sqrt2irraplemnn  12744  qnumdencoprm  12758  qeqnumdivden  12759  nn0gcdsq  12765  nn0sqrtelqelz  12771  nonsq  12772  phicl2  12779  phibnd  12782  hashdvds  12786  phiprmpw  12787  phimullem  12790  eulerthlemrprm  12794  eulerthlema  12795  eulerthlemth  12797  prmdiveq  12801  hashgcdlem  12803  odzdvds  12811  modprminv  12815  nnnn0modprm0  12821  modprmn0modprm0  12822  pythagtriplem10  12835  pythagtriplem19  12848  pythagtrip  12849  pcpre1  12858  pcpremul  12859  pceu  12861  pcmul  12867  pcdiv  12868  pcqmul  12869  pcqdiv  12873  pcexp  12875  pcdvdsb  12886  pcidlem  12889  pcdvdstr  12893  pcgcd1  12894  pc2dvds  12896  pcprmpw2  12899  difsqpwdvds  12904  pcaddlem  12905  pcadd  12906  pcadd2  12907  pcmpt  12909  pcmptdvds  12911  pcprod  12912  fldivp1  12914  pcfaclem  12915  pcfac  12916  pcbc  12917  qexpz  12918  pockthlem  12922  pockthg  12923  1arithlem4  12932  1arith  12933  1arith2  12934  4sqlem6  12949  4sqlem8  12951  4sqlem9  12952  4sqlem10  12953  4sqexercise1  12964  4sqexercise2  12965  4sqlemsdc  12966  4sqlem11  12967  4sqlem12  12968  4sqlem15  12971  4sqlem16  12972  4sqlem17  12973  znnen  13012  ennnfonelemk  13014  ennnfonelemkh  13026  ennnfonelemhf1o  13027  ennnfonelemrnh  13030  ennnfonelemfun  13031  ennnfonelemf1  13032  ennnfonelemrn  13033  ennnfonelemnn0  13036  ctinfomlemom  13041  ctiunctlemudc  13051  unct  13056  omctfn  13057  ssnnctlemct  13060  nninfdclemp1  13064  nninfdc  13067  structfung  13092  setsfun  13110  setsfun0  13111  setscom  13115  strslfv3  13121  setsslid  13126  pwsdiagel  13373  pwssnf1o  13374  imasaddfnlemg  13390  imasaddvallemg  13391  mgmsscl  13437  plusffng  13441  mgmplusf  13442  mgm0  13445  mgm1  13446  opifismgmdc  13447  gsumfzval  13467  gsumprval  13475  sgrp1  13487  issgrpd  13488  prdsplusgsgrpcl  13490  mndpfo  13514  mndfo  13515  prdsplusgcl  13522  prdsidlem  13523  mnd1  13531  0subm  13560  mhmima  13567  grpinvfng  13620  isgrpinv  13630  grpinvid  13636  grpinvf1o  13646  grpinvadd  13654  grpsubf  13655  grpsubsub4  13669  grplactcnv  13678  grp1  13682  grp1inv  13683  prdsinvlem  13684  prdsinvgd  13686  qusgrp2  13693  mulgfng  13704  subginv  13761  resgrpisgrp  13775  subgintm  13778  0subg  13779  0nsg  13794  qusinv  13816  ghminv  13830  ghmrn  13837  ghmeql  13847  ghmnsgima  13848  kerf1ghm  13854  conjnmz  13859  rngass  13945  rngmneg1  13953  rngmneg2  13954  qusrng  13964  srgideu  13978  srgidmlem  13984  srgpcomp  13996  srg1expzeq1  14001  ringcl  14019  ringideu  14023  ringidmlem  14028  ringnegl  14057  ringnegr  14058  ring1  14065  qusring2  14072  opprringbg  14086  dvdsrd  14101  dvdsr01  14111  isunitd  14113  unitinvcl  14130  unitinvinv  14131  unitnegcl  14137  rhmmul  14171  rhmf1o  14175  nzrunit  14195  lringuplu  14203  subrngintm  14219  subrgsubm  14241  subrgintm  14250  aprsym  14291  scaffng  14316  lmodscaf  14317  lsssn0  14377  lss1d  14390  lssintclm  14391  lspval  14397  lspcl  14398  lspsnid  14414  lspprid1  14418  lspsn  14423  sraval  14444  rspcl  14498  rspssid  14499  rspssp  14501  rnglidlmmgm  14503  rnglidlmsgrp  14504  cnfldneg  14580  zringinvg  14611  expghmap  14614  znzrhfo  14655  znf1o  14658  znhash  14663  znidomb  14665  znrrg  14667  psrbagfi  14680  psraddcl  14687  psr0cl  14688  psrnegcl  14690  psrneg  14694  psr1clfi  14695  mplsubgfilemm  14705  mplsubgfilemcl  14706  baspartn  14767  eltg3i  14773  tgclb  14782  topbas  14784  2basgeng  14799  topcld  14826  0cld  14829  uncld  14830  neif  14858  elnei  14869  0nei  14883  restbasg  14885  iscnp4  14935  cnpnei  14936  cnclima  14940  cncnp  14947  cnrest2r  14954  cndis  14958  lmff  14966  lmtopcnp  14967  txbas  14975  txopn  14982  txcnp  14988  upxp  14989  txdis1cn  14995  cnmpt11  15000  cnmpt21  15008  psmetge0  15048  xmetge0  15082  xmettpos  15087  xmetrtri  15093  metrtri  15094  xblpnfps  15115  xblpnf  15116  blfps  15126  blf  15127  ssblps  15142  ssbl  15143  blbas  15150  metss2  15215  xmettxlem  15226  xmettx  15227  qtopbas  15239  divcnap  15282  cncfss  15300  cdivcncfap  15321  expcncf  15326  cnopnap  15328  maxcncf  15332  mincncf  15333  dedekindeulemuub  15334  dedekindeulemlu  15338  dedekindeu  15340  suplociccex  15342  dedekindicclemuub  15343  dedekindicclemlu  15347  dedekindicclemicc  15349  ivthinclemlopn  15353  ivthinclemuopn  15355  ivthinc  15360  ivthreinc  15362  hoverlt1  15366  ellimc3apf  15377  limcimolemlt  15381  limcimo  15382  limcresi  15383  cnplimclemle  15385  reldvg  15396  dvfgg  15405  dvidlemap  15408  dvidrelem  15409  dvidsslem  15410  dvcjbr  15425  dvcj  15426  dvrecap  15430  dveflem  15443  dvef  15444  elply2  15452  elplyr  15457  plycj  15478  plyreres  15481  reeff1oleme  15489  pilem3  15500  sinq34lt0t  15548  cosq14gt0  15549  coseq0q4123  15551  tangtx  15555  sincosq1eq  15556  cosordlem  15566  logdivlti  15598  relogbval  15668  relogbzcl  15669  nnlogbexp  15676  logbgcd1irr  15684  logbgcd1irraplemexp  15685  logbgcd1irraplemap  15686  wilthlem1  15697  mpodvdsmulf1o  15707  mersenne  15714  perfectlem2  15717  perfect  15718  zabsle1  15721  lgslem1  15722  lgsval  15726  lgsfvalg  15727  lgsfcl2  15728  lgsval2lem  15732  lgscl1  15745  lgsmod  15748  lgsdir2lem5  15754  lgsdir2  15755  lgsdilem2  15758  lgsdi  15759  lgsne0  15760  gausslemma2dlem0c  15773  gausslemma2dlem0h  15778  gausslemma2dlem1a  15780  gausslemma2dlem1f1o  15782  gausslemma2dlem3  15785  lgseisenlem1  15792  lgseisenlem2  15793  lgseisenlem3  15794  lgseisenlem4  15795  lgseisen  15796  lgsquadlem1  15799  lgsquadlem2  15800  lgsquadlem3  15801  lgsquad3  15806  2lgslem3b1  15820  2lgslem3c1  15821  2lgs  15826  2lgsoddprmlem2  15828  2lgsoddprm  15835  2sqlem3  15839  2sqlem8  15845  2sqlem10  15847  structgrssvtx  15886  structgrssiedg  15887  ushgruhgr  15924  uhgrun  15930  incistruhgr  15934  upgrop  15948  upgruhgr  15955  umgrupgr  15956  umgrnloopv  15958  umgredgprv  15959  umgr0e  15962  upgr1edc  15965  umgr1een  15969  upgrun  15970  umgrun  15972  umgrislfupgrdom  15975  upgredg  15988  umgrpredgv  15991  usgrop  16010  usgrausgrien  16013  ausgrumgrien  16014  ausgrusgrien  16015  uspgrupgrushgr  16026  usgrumgr  16028  usgrumgruspgr  16029  usgruspgrben  16030  usgrislfuspgrdom  16034  edgssv2en  16043  usgrf1oedg  16049  usgredg4  16059  usgredg2vlem2  16067  usgredg2v  16068  ushgredgedg  16070  ushgredgedgloop  16072  usgrstrrepeen  16075  usgr0e  16076  uhgr0v0e  16078  uspgr1edc  16084  usgr1e  16085  griedg0ssusgr  16095  1loopgrvd2fi  16116  1loopgrvd0fi  16117  1hevtxdg0fi  16118  vdegp1aid  16125  vdegp1bid  16126  wlkm  16150  wlkvtxiedg  16156  wlkvtxiedgg  16157  wlkeq  16165  wlk1walkdom  16170  uspgr2wlkeq  16176  uspgr2wlkeqi  16178  upgr2wlkdc  16186  wlkres  16188  trlreslem  16198  clwwlkccatlem  16209  clwwlkn1loopb  16229  clwwlkext2edg  16231  clwwlknonex2lem1  16246  clwwlknonex2  16248  fnmptd  16350  bj-sels  16459  bj-nnelon  16504  2omap  16544  pw1map  16546  pwle2  16549  pwf1oexmid  16550  pw1nct  16554  nninfall  16561  nninfsellemdc  16562  nninfself  16565  nnnninfex  16574  nninfnfiinf  16575  refeq  16582  isomninnlem  16584  cvgcmp2nlemabs  16586  trilpolemlt1  16595  trirec0  16598  apdifflemf  16600  apdifflemr  16601  apdiff  16602  iswomninnlem  16603  iswomni0  16605  ismkvnnlem  16606  reap0  16612  cndcap  16613  gfsumval  16630  gsumgfsumlem  16633  gsumgfsum  16634