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  3159  eqsstrd  3278  3sstr4d  3287  ifeqeqxdc  3673  eqbrtrd  4136  3brtr4d  4146  snelpwi  4332  prelpwi  4335  pwel  4339  ordelon  4509  onin  4512  elelsuc  4535  onsuc  4628  onsucb  4630  onintonm  4644  omsinds  4749  sosng  4828  relssdv  4847  eqbrrdv  4852  eqrelrdv2  4854  relsnopg  4859  breldmg  4967  elrnmptdv  5016  iss  5089  xpimasn  5216  elxp4  5255  elxp5  5256  iotam  5349  funssres  5400  f0rn0  5567  fimadmfo  5604  sefvex  5696  fdmeu  5725  fvun1  5748  eqfnfvd  5783  fvimacnvi  5797  fvimacnv  5798  fvelrn  5813  fmpt3d  5838  fmpt2d  5844  resflem  5846  fmptco  5848  fsn  5854  funopsn  5865  fncofn  5867  ftpg  5873  fconst2g  5904  funfvima3  5925  elabrexg  5937  foeqcnvco  5969  f1eqcocnv  5970  fliftfun  5975  fliftfund  5976  fliftval  5979  riota5f  6038  f1ofveu  6046  f1ocnvd  6265  f1opw2  6269  f1o3d  6271  off  6288  offval2  6291  ofrfval2  6292  offveq  6296  caofref  6300  caofinvl  6301  elxp6  6376  cnvf1olem  6433  f2ndf  6435  f1od2  6444  elmpom  6447  fvn0elsupp  6464  suppfnss  6470  tposf12  6513  smores2  6538  tfrlemisucaccv  6569  tfrlemibfn  6572  tfr1onlemsucaccv  6585  tfr1onlembfn  6588  tfrcllemsucaccv  6598  tfrcllembfn  6601  tfrcl  6608  tfri3  6611  frecabcl  6643  nnsucsssuc  6738  ersym  6792  ertr  6795  swoer  6808  erth  6826  riinerm  6855  qliftfund  6865  eroprf  6875  ecopoverg  6883  th3qlem1  6884  elmapssres  6920  mapss  6939  fdiagfn  6940  ixpssmap2g  6975  mapsnf1o  6985  f1oen4g  7004  f1dom4g  7005  f1dom2g  7008  dom3d  7026  en2prd  7072  dom1oi  7083  pw2f1odclem  7100  fopwdom  7102  mapxpen  7114  nndomo  7131  dif1en  7149  findcard2  7159  findcard2s  7160  diffisn  7163  fimax2gtrilemstep  7171  eqsndc  7176  fientri3  7188  tpfidceq  7203  fiintim  7204  opabfi  7213  f1dmvrnfibi  7224  sbthlemi6  7245  0fsupp  7264  elfir  7273  fifo  7280  2omap  7282  supelti  7306  supsnti  7309  cnvinfex  7322  ordiso2  7339  updjud  7386  djudom  7397  difinfsn  7404  ctssdc  7417  enumctlemm  7418  enumct  7419  nninfninc  7427  enomnilem  7442  fodjuf  7449  ismkvnex  7459  omnimkv  7460  enmkvlem  7465  enwomnilem  7473  nninfdcinf  7475  nninfwlporlem  7477  isnumi  7491  exmidfodomrlemrALT  7519  finacn  7524  djudoml  7539  djudomr  7540  netap  7584  2omotaplemap  7587  2omotaplemst  7588  exmidapne  7590  cc2lem  7596  cc3  7598  ltsopi  7651  pitri3or  7653  ltdcpi  7654  indpi  7673  enqdc  7692  enqdc1  7693  addcmpblnq  7698  mulcanenq  7716  recrecnq  7725  nqtri3or  7727  ltdcnq  7728  ltsonq  7729  ltaddnq  7738  subhalfnqq  7745  archnqq  7748  prarloclemarch2  7750  enq0tr  7765  nqnq0  7772  addcmpblnq0  7774  mulcanenq0ec  7776  nnnq0lem1  7777  nqpnq0nq  7784  nq0m0r  7787  nq02m  7796  prarloclemlt  7824  prarloclemcalc  7833  addlocpr  7867  nqprl  7882  nqpru  7883  addnqprlemrl  7888  addnqprlemru  7889  prmuloclemcalc  7896  mullocprlem  7901  mulnqprlemrl  7904  mulnqprlemru  7905  1idprl  7921  1idpru  7922  ltaddpr  7928  ltexprlemm  7931  ltexprlemopl  7932  ltexprlemopu  7934  ltexprlemdisj  7937  ltexprlemrl  7941  ltexprlemru  7943  addcanprleml  7945  addcanprlemu  7946  addcanprg  7947  prplnqu  7951  recexprlemloc  7962  recexprlem1ssl  7964  recexprlem1ssu  7965  aptiprleml  7970  aptiprlemu  7971  archpr  7974  cauappcvgprlemm  7976  cauappcvgprlemopl  7977  cauappcvgprlemloc  7983  cauappcvgprlemladdfu  7985  cauappcvgprlemladdfl  7986  cauappcvgprlem1  7990  cauappcvgprlem2  7991  caucvgprlemnkj  7997  caucvgprlemopl  8000  caucvgprlemloc  8006  caucvgprlemladdfu  8008  caucvgprlem2  8011  caucvgprprlemnkltj  8020  caucvgprprlemopl  8028  caucvgprprlemloc  8034  caucvgprprlemexbt  8037  caucvgprprlemaddq  8039  caucvgprprlem2  8041  suplocexprlemmu  8049  suplocexprlemru  8050  suplocexprlemloc  8052  suplocexprlemlub  8055  prsrlem1  8073  0idsr  8098  1idsr  8099  recexgt0sr  8104  archsr  8113  prsradd  8117  caucvgsrlemcau  8124  caucvgsrlembound  8125  caucvgsrlemoffgt1  8130  suplocsrlemb  8137  suplocsrlempr  8138  suplocsrlem  8139  pitonnlem1p1  8177  pitonn  8179  pitoregt0  8180  peano2nnnn  8184  recidpirq  8189  axcaucvglemval  8228  leid  8373  nltled  8411  readdcan  8430  addneintrd  8478  addneintr2d  8479  pncan  8496  subsub2  8518  subsub4  8523  negned  8598  subne0d  8610  subneintrd  8645  subneintr2d  8647  subeq0bd  8670  subdi  8676  gt0add  8865  rimul  8877  rereim  8878  ltmul1a  8883  apreim  8895  apirr  8897  mulap0r  8907  msqge0  8908  mulge0  8911  gt0ap0  8918  ltap  8925  subap0d  8936  recexaplem2  8944  mulap0bad  8951  mulap0bbd  8952  mul0eqap  8964  divrecap  8982  div0ap  8996  div1  8997  recrecap  9003  divdivdivap  9007  ddcanap  9020  rerecclap  9024  div2negap  9029  diveqap1bd  9130  recgt0  9144  prodgt0  9146  lemul1a  9152  recp1lt1  9193  squeeze0  9198  peano2nn  9269  div4p1lem1div2  9512  arch  9513  peano2z  9633  peano2zm  9635  ztri3or  9640  nn0n0n1ge2  9668  zextle  9690  gtndiv  9694  suprzclex  9697  nn0ind-raph  9716  uzid  9889  uzneg  9894  uztric  9897  uz11  9898  eluzp1l  9900  qdivcl  9996  irrmul  10000  irrmulap  10001  rpnegap  10040  negelrpd  10042  ledivge1le  10080  mul2lt0rlt0  10113  mul2lt0rgt0  10114  nn0ledivnn  10121  ltpnf  10135  mnflt  10138  pnfge  10144  mnfle  10147  xrlttr  10150  xrltso  10151  xrlttri3  10152  xrleid  10155  xaddass2  10225  xltadd1  10231  xlt2add  10235  xleaddadd  10242  lincmble  10359  iccf1o  10360  fztri3or  10396  fznlem  10398  fzn  10399  fzsplit2  10407  fzsplit3  10410  fznatpl1  10435  uzsplit  10451  fseq1p1m1  10453  fzm1  10459  fznn0sub2  10487  difelfznle  10494  1fv  10498  fzodcel  10512  fzospliti  10537  fzouzsplit  10540  eluzgtdifelfzo  10567  exfzdc  10611  subfzo0  10613  zsupcllemstep  10614  zsupcl  10616  zssinfcl  10617  infssuzex  10618  infssuzcldc  10620  infssfzcldc  10621  infssfzledc  10622  suprzubdc  10623  nninfdcex  10624  qdcle  10633  exbtwnz  10637  qbtwnrelemcalc  10642  flqlelt  10663  qfraclt1  10667  qfracge0  10668  flqltnz  10674  btwnzge0  10687  flhalf  10689  fldiv4lem1div2uz2  10693  ceiqle  10702  intfracq  10709  mulqmod0  10719  modqge0  10721  modqlt  10722  modqid  10738  modqid0  10739  m1modge3gt1  10760  modqltm1p1mod  10765  q2txmodxeq0  10773  modaddmodlo  10777  modsumfzodifsn  10785  addmodlteq  10787  frecuzrdgtcl  10801  frecuzrdgtclt  10810  uzennn  10825  uzsinds  10833  seqf  10853  seqf2  10857  monoord2  10875  iseqf1olemqk  10896  iseqf1olemjpcl  10897  iseqf1olemqpcl  10898  seq3f1olemqsumkj  10900  seq3f1olemqsum  10902  seq3f1olemstep  10903  seq3f1oleml  10905  seqf1oglem1  10908  ser3le  10926  exp3vallem  10929  exp3val  10930  expp1  10935  expcllem  10939  ltexp2a  10980  leexp2a  10981  resq01  11047  nn0ltexp2  11099  faclbnd  11131  faclbnd2  11132  faclbnd3  11133  bcval5  11153  bcpasc  11156  bcm1n  11159  hashennn  11171  fihasheqf1oi  11178  hashsng  11189  fihashfn  11192  hashun  11197  fihashss  11209  fihashssdif  11211  hashfz  11214  hashxp  11219  hashmap  11220  hashpwfi  11221  fimaxq  11222  sseqn  11231  hashfibclem  11234  zfz1isolem1  11240  seq3coll  11242  hashdmprop2dom  11244  wrdf  11258  wrdlenge2n0  11288  fstwrdne0  11292  wrdred1hash  11296  ccatvalfn  11317  ccatsymb  11318  ccatlid  11322  ccatrid  11323  ccatrn  11325  ccatalpha  11329  eqs1  11344  ccats1val2  11356  fzowrddc  11367  swrdlen  11372  swrdnd  11379  swrd0g  11380  swrdfv2  11383  swrdwrdsymbg  11384  pfxn0  11408  pfxwrdsymbg  11410  pfxsuff1eqwrdeq  11419  swrdswrd  11425  ccats1pfxeq  11434  ccats1pfxeqrex  11435  wrdind  11442  wrd2ind  11443  swrdccatin1  11445  pfxccatin12lem4  11446  swrdccatin2  11449  pfxccatin12  11453  pfxccat3a  11458  swrdccat3blem  11459  pfxccatid  11461  swrdccatin2d  11464  shftfn  11537  cjth  11559  cjmulrcl  11600  reim0bd  11657  rerebd  11658  cjrebd  11659  caucvgre  11694  cvg1nlemcxze  11695  cvg1nlemcau  11697  cvg1nlemres  11698  recvguniq  11708  resqrexlemover  11723  resqrexlemdec  11724  resqrexlemgt0  11733  resqrexlemoverl  11734  resqrexlemglsq  11735  rersqrtthlem  11743  sqrtgt0  11747  leabs  11787  absexpzap  11793  absle  11802  recvalap  11810  abstri  11817  abs2dif  11819  amgm2  11831  absne0d  11900  maxleim  11918  maxabslemab  11919  maxabslemlub  11920  maxltsup  11931  zmaxcl  11937  fimaxre2  11940  minmax  11943  rpmincl  11951  bdtrilem  11952  bdtri  11953  xrmaxleim  11957  xrmaxiflemcom  11962  xrmaxltsup  11971  xrmaxadd  11974  xrminmax  11978  xrminrpcl  11987  climconst  12003  climuni  12006  2clim  12014  climcn1  12021  climcn2  12022  reccn2ap  12026  climge0  12038  climle  12047  climsqz  12048  climsqz2  12049  serf0  12065  summodclem3  12094  summodclem2a  12095  fsumcl2lem  12112  sumpr  12127  sumtp  12128  fsum0diaglem  12154  mptfzshft  12156  fsumle  12177  fsumlt  12178  divcnv  12211  trireciplem  12214  expcnvap0  12216  expcnv  12218  explecnv  12219  geosergap  12220  cvgratnnlembern  12237  cvgratnnlemabsle  12241  cvgratnnlemsumlt  12242  cvgratz  12246  cvgratgt0  12247  mertenslemi1  12249  mertenslem2  12250  mertensabs  12251  clim2divap  12254  prodmodclem3  12289  prodmodclem2a  12290  fprodseq  12297  fprodmul  12305  fprodfac  12329  fprodconst  12334  fprodap0  12335  fprodap0f  12350  fprodle  12354  eftcl  12368  ef0lem  12374  efsub  12395  eftlub  12404  eflegeo  12415  tanval2ap  12427  sinadd  12450  cos2t  12464  cos2tsin  12465  sin01bnd  12471  cos01bnd  12472  eirraplem  12491  dvdsval2  12504  dvdsdc  12512  dvds0lem  12515  zdvdsdc  12526  dvdscmulr  12534  dvdsmulcr  12535  fsumdvds  12556  dvdslelemd  12557  divconjdvds  12563  dvdsext  12569  fzm1ndvds  12570  dvdsmod  12576  3dvds  12578  oexpneg  12591  2tp1odd  12598  mulsucdiv2z  12599  2teven  12601  zeo5  12602  opeo  12611  omeo  12612  nn0ob  12622  divalglemnqt  12634  bitsdc  12661  bits0o  12664  bitsfzolem  12668  bitsfzo  12669  bitsmod  12670  bitscmp  12672  bitsinv1lem  12675  gcddvds  12687  dvdslegcd  12688  gcdneg  12706  bezoutlemnewy  12720  bezoutlemstep  12721  bezoutlema  12723  bezoutlemb  12724  bezoutlemmo  12730  bezoutlemle  12732  bezoutlemsup  12733  dfgcd3  12734  bezout  12735  dfgcd2  12738  uzwodc  12761  lcmcllem  12792  lcmneg  12799  lcmgcdlem  12802  lcmdvds  12804  lcmid  12805  3lcm2e6woprm  12811  6lcm4e12  12812  ncoprmgcdne1b  12814  mulgcddvds  12819  divgcdcoprmex  12827  cncongr1  12828  cncongr2  12829  isprm2lem  12841  prmind2  12845  dvdsnprmd  12850  prm2orodd  12851  sqnprm  12861  isprm5lem  12866  rpexp  12878  sqrt2irrlem  12886  oddpwdclemdc  12898  sqrt2irraplemnn  12904  qnumdencoprm  12918  qeqnumdivden  12919  nn0gcdsq  12925  nn0sqrtelqelz  12931  nonsq  12932  phicl2  12939  phibnd  12942  hashdvds  12946  phiprmpw  12947  phimullem  12950  eulerthlemrprm  12954  eulerthlema  12955  eulerthlemth  12957  prmdiveq  12961  hashgcdlem  12963  odzdvds  12971  modprminv  12975  nnnn0modprm0  12981  modprmn0modprm0  12982  pythagtriplem10  12995  pythagtriplem19  13008  pythagtrip  13009  pcpre1  13018  pcpremul  13019  pceu  13021  pcmul  13027  pcdiv  13028  pcqmul  13029  pcqdiv  13033  pcexp  13035  pcdvdsb  13046  pcidlem  13049  pcdvdstr  13053  pcgcd1  13054  pc2dvds  13056  pcprmpw2  13059  difsqpwdvds  13064  pcaddlem  13065  pcadd  13066  pcadd2  13067  pcmpt  13069  pcmptdvds  13071  pcprod  13072  fldivp1  13074  pcfaclem  13075  pcfac  13076  pcbc  13077  qexpz  13078  pockthlem  13082  pockthg  13083  1arithlem4  13092  1arith  13093  1arith2  13094  4sqlem6  13109  4sqlem8  13111  4sqlem9  13112  4sqlem10  13113  4sqexercise1  13124  4sqexercise2  13125  4sqlemsdc  13126  4sqlem11  13127  4sqlem12  13128  4sqlem15  13131  4sqlem16  13132  4sqlem17  13133  ballotfilemfc0  13179  ballotfilemfcc  13180  ballotfilemimin  13196  ballotfilem1c  13198  ballotfilemro  13213  ballotfilemfrcn0  13220  znnen  13236  ennnfonelemk  13238  ennnfonelemkh  13250  ennnfonelemhf1o  13251  ennnfonelemrnh  13254  ennnfonelemfun  13255  ennnfonelemf1  13256  ennnfonelemrn  13257  ennnfonelemnn0  13260  ctinfomlemom  13265  ctiunctlemudc  13275  unct  13280  omctfn  13281  ssnnctlemct  13284  nninfdclemp1  13288  nninfdc  13291  structfung  13316  setsfun  13334  setsfun0  13335  setscom  13339  strslfv3  13345  setsslid  13350  imasaddfnlemg  13581  imasaddvallemg  13582  mgmsscl  13627  plusffng  13631  mgmplusf  13632  mgm0  13635  mgm1  13636  opifismgmdc  13637  gsumfzval  13657  gsumprval  13665  sgrp1  13677  issgrpd  13678  mndpfo  13702  mndfo  13703  mnd1  13713  0subm  13742  mhmima  13749  grpinvfng  13802  isgrpinv  13812  grpinvid  13818  grpinvf1o  13828  grpinvadd  13836  grpsubf  13837  grpsubsub4  13851  grplactcnv  13860  grp1  13864  grp1inv  13865  qusgrp2  13869  mulgfng  13880  subginv  13937  resgrpisgrp  13951  subgintm  13954  0subg  13955  0nsg  13970  qusinv  13992  ghminv  14006  ghmrn  14013  ghmeql  14023  ghmnsgima  14024  kerf1ghm  14030  conjnmz  14035  gfsumval  14105  gsumshift  14108  gsumgfsum  14109  gfsumsn  14110  gfsump1  14111  prdsplusgsgrpcl  14135  prdsplusgcl  14137  prdsidlem  14138  prdsinvlem  14141  prdsinvgd  14143  pwsdiagel  14155  pwssnf1o  14156  rngass  14181  rngmneg1  14189  rngmneg2  14190  qusrng  14200  srgideu  14218  srgidmlem  14224  srgpcomp  14236  srg1expzeq1  14241  ringcl  14259  ringideu  14263  ringidmlem  14268  ringnegl  14297  ringnegr  14298  ring1  14305  qusring2  14312  opprringbg  14326  dvdsrd  14342  dvdsr01  14352  isunitd  14354  unitinvcl  14371  unitinvinv  14372  unitnegcl  14378  rhmmul  14412  rhmf1o  14416  nzrunit  14436  lringuplu  14444  subrngintm  14461  subrgsubm  14483  subrgintm  14492  rrgsupp  14515  ringunitap  14534  aprsym  14537  aprnzr  14540  aprlring  14541  drnglring  14548  drngunitap  14549  scaffng  14586  lmodscaf  14587  lsssn0  14647  lss1d  14660  lssintclm  14661  lspval  14667  lspcl  14668  lspsnid  14684  lspprid1  14688  lspsn  14693  sraval  14714  rspcl  14768  rspssid  14769  rspssp  14771  rnglidlmmgm  14773  rnglidlmsgrp  14774  cnfldneg  14850  zringinvg  14881  expghmap  14884  znzrhfo  14925  znf1o  14928  znhash  14933  znidomb  14935  znrrg  14937  psrbagfsupp  14948  psrbagfi  14952  psrbaglecl  14953  psrbagaddclfi  14954  psrbagcon  14955  psraddcl  14964  psr0cl  14965  psrnegcl  14967  psrneg  14971  psr1clfi  14972  mplsubgfilemm  14982  mplsubgfilemcl  14983  baspartn  15044  eltg3i  15050  tgclb  15059  topbas  15061  2basgeng  15076  topcld  15103  0cld  15106  uncld  15107  neif  15135  elnei  15146  0nei  15160  restbasg  15162  iscnp4  15212  cnpnei  15213  cnclima  15217  cncnp  15224  cnrest2r  15231  cndis  15235  lmff  15243  lmtopcnp  15244  txbas  15252  txopn  15259  txcnp  15265  upxp  15266  txdis1cn  15272  cnmpt11  15277  cnmpt21  15285  psmetge0  15325  xmetge0  15359  xmettpos  15364  xmetrtri  15370  metrtri  15371  xblpnfps  15392  xblpnf  15393  blfps  15403  blf  15404  ssblps  15419  ssbl  15420  blbas  15427  metss2  15492  xmettxlem  15503  xmettx  15504  qtopbas  15516  divcnap  15559  cncfss  15577  cdivcncfap  15598  expcncf  15603  cnopnap  15605  maxcncf  15609  mincncf  15610  dedekindeulemuub  15611  dedekindeulemlu  15615  dedekindeu  15617  suplociccex  15619  dedekindicclemuub  15620  dedekindicclemlu  15624  dedekindicclemicc  15626  ivthinclemlopn  15630  ivthinclemuopn  15632  ivthinc  15637  ivthreinc  15639  hoverlt1  15643  ellimc3apf  15654  limcimolemlt  15658  limcimo  15659  limcresi  15660  cnplimclemle  15662  reldvg  15673  dvfgg  15682  dvidlemap  15685  dvidrelem  15686  dvidsslem  15687  dvcjbr  15702  dvcj  15703  dvrecap  15707  dveflem  15720  dvef  15721  elply2  15729  elplyr  15734  plycj  15755  plyreres  15758  reeff1oleme  15766  pilem3  15777  sinq34lt0t  15825  cosq14gt0  15826  coseq0q4123  15828  tangtx  15832  sincosq1eq  15833  cosordlem  15843  logdivlti  15875  relogbval  15945  relogbzcl  15946  nnlogbexp  15953  logbgcd1irr  15961  logbgcd1irraplemexp  15962  logbgcd1irraplemap  15963  pellexlem1  15974  pellexlem3  15976  wilthlem1  15977  mpodvdsmulf1o  15987  mersenne  15994  perfectlem2  15997  perfect  15998  zabsle1  16001  lgslem1  16002  lgsval  16006  lgsfvalg  16007  lgsfcl2  16008  lgsval2lem  16012  lgscl1  16025  lgsmod  16028  lgsdir2lem5  16034  lgsdir2  16035  lgsdilem2  16038  lgsdi  16039  lgsne0  16040  gausslemma2dlem0c  16053  gausslemma2dlem0h  16058  gausslemma2dlem1a  16060  gausslemma2dlem1f1o  16062  gausslemma2dlem3  16065  lgseisenlem1  16072  lgseisenlem2  16073  lgseisenlem3  16074  lgseisenlem4  16075  lgseisen  16076  lgsquadlem1  16079  lgsquadlem2  16080  lgsquadlem3  16081  lgsquad3  16086  2lgslem3b1  16100  2lgslem3c1  16101  2lgs  16106  2lgsoddprmlem2  16108  2lgsoddprm  16115  2sqlem3  16119  2sqlem8  16125  2sqlem10  16127  structgrssvtx  16166  structgrssiedg  16167  ushgruhgr  16204  uhgrun  16210  incistruhgr  16214  upgrop  16228  upgruhgr  16235  umgrupgr  16236  umgrnloopv  16238  umgredgprv  16239  umgr0e  16242  upgr1edc  16245  umgr1een  16249  upgrun  16250  umgrun  16252  umgrislfupgrdom  16255  upgredg  16268  umgrpredgv  16271  usgrop  16290  usgrausgrien  16293  ausgrumgrien  16294  ausgrusgrien  16295  uspgrupgrushgr  16306  usgrumgr  16308  usgrumgruspgr  16309  usgruspgrben  16310  usgrislfuspgrdom  16314  edgssv2en  16323  usgrf1oedg  16329  usgredg4  16339  usgredg2vlem2  16347  usgredg2v  16348  ushgredgedg  16350  ushgredgedgloop  16352  usgrstrrepeen  16355  usgr0e  16356  uhgr0v0e  16358  uspgr1edc  16364  usgr1e  16365  griedg0ssusgr  16375  subgrprop3  16386  subgruhgredgdm  16394  subuhgr  16396  subupgr  16397  subumgr  16398  subusgr  16399  uhgrspansubgrlem  16400  1loopgrvd2fi  16429  1loopgrvd0fi  16430  1hevtxdg0fi  16431  vdegp1aid  16438  vdegp1bid  16439  wlkm  16463  wlkvtxiedg  16469  wlkvtxiedgg  16470  wlkeq  16478  wlk1walkdom  16483  uspgr2wlkeq  16489  uspgr2wlkeqi  16491  upgr2wlkdc  16501  wlkres  16503  trlreslem  16513  clwwlkccatlem  16524  clwwlkn1loopb  16544  clwwlkext2edg  16546  clwwlknonex2lem1  16561  clwwlknonex2  16563  trlsegvdeglem2  16585  trlsegvdeglem3  16586  eupth2lem3lem4fi  16597  eupth2lemsfi  16602  fnmptd  16715  bj-sels  16823  bj-nnelon  16868  pw1map  16908  pwle2  16911  pwf1oexmid  16912  pw1nct  16916  nninfall  16926  nninfsellemdc  16927  nninfself  16930  nnnninfex  16939  nninfnfiinf  16940  refeq  16947  isomninnlem  16953  cvgcmp2nlemabs  16955  trilpolemlt1  16964  trirec0  16967  apdifflemf  16969  apdifflemr  16970  apdiff  16971  qdiff  16972  iswomninnlem  16973  iswomni0  16975  ismkvnnlem  16976  reap0  16982  cndcap  16983  trimul0or  16984