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  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  8410  readdcan  8429  addneintrd  8477  addneintr2d  8478  pncan  8495  subsub2  8517  subsub4  8522  negned  8597  subne0d  8609  subneintrd  8644  subneintr2d  8646  subeq0bd  8669  subdi  8675  gt0add  8864  rimul  8876  rereim  8877  ltmul1a  8882  apreim  8894  apirr  8896  mulap0r  8906  msqge0  8907  mulge0  8910  gt0ap0  8917  ltap  8924  subap0d  8935  recexaplem2  8943  mulap0bad  8950  mulap0bbd  8951  mul0eqap  8961  divrecap  8979  div0ap  8993  div1  8994  recrecap  9000  divdivdivap  9004  ddcanap  9017  rerecclap  9021  div2negap  9026  diveqap1bd  9127  recgt0  9141  prodgt0  9143  lemul1a  9149  recp1lt1  9190  squeeze0  9195  peano2nn  9266  div4p1lem1div2  9509  arch  9510  peano2z  9630  peano2zm  9632  ztri3or  9637  nn0n0n1ge2  9665  zextle  9687  gtndiv  9691  suprzclex  9694  nn0ind-raph  9713  uzid  9886  uzneg  9891  uztric  9894  uz11  9895  eluzp1l  9897  qdivcl  9993  irrmul  9997  irrmulap  9998  rpnegap  10037  negelrpd  10039  ledivge1le  10077  mul2lt0rlt0  10110  mul2lt0rgt0  10111  nn0ledivnn  10118  ltpnf  10132  mnflt  10135  pnfge  10141  mnfle  10144  xrlttr  10147  xrltso  10148  xrlttri3  10149  xrleid  10152  xaddass2  10222  xltadd1  10228  xlt2add  10232  xleaddadd  10239  lincmble  10356  iccf1o  10357  fztri3or  10393  fznlem  10395  fzn  10396  fzsplit2  10404  fzsplit3  10407  fznatpl1  10432  uzsplit  10448  fseq1p1m1  10450  fzm1  10456  fznn0sub2  10484  difelfznle  10491  1fv  10495  fzodcel  10509  fzospliti  10534  fzouzsplit  10537  eluzgtdifelfzo  10564  exfzdc  10608  subfzo0  10610  zsupcllemstep  10611  zsupcl  10613  zssinfcl  10614  infssuzex  10615  infssuzcldc  10617  infssfzcldc  10618  infssfzledc  10619  suprzubdc  10620  nninfdcex  10621  qdcle  10630  exbtwnz  10634  qbtwnrelemcalc  10639  flqlelt  10660  qfraclt1  10664  qfracge0  10665  flqltnz  10671  btwnzge0  10684  flhalf  10686  fldiv4lem1div2uz2  10690  ceiqle  10699  intfracq  10706  mulqmod0  10716  modqge0  10718  modqlt  10719  modqid  10735  modqid0  10736  m1modge3gt1  10757  modqltm1p1mod  10762  q2txmodxeq0  10770  modaddmodlo  10774  modsumfzodifsn  10782  addmodlteq  10784  frecuzrdgtcl  10798  frecuzrdgtclt  10807  uzennn  10822  uzsinds  10830  seqf  10850  seqf2  10854  monoord2  10872  iseqf1olemqk  10893  iseqf1olemjpcl  10894  iseqf1olemqpcl  10895  seq3f1olemqsumkj  10897  seq3f1olemqsum  10899  seq3f1olemstep  10900  seq3f1oleml  10902  seqf1oglem1  10905  ser3le  10923  exp3vallem  10926  exp3val  10927  expp1  10932  expcllem  10936  ltexp2a  10977  leexp2a  10978  resq01  11044  nn0ltexp2  11096  faclbnd  11128  faclbnd2  11129  faclbnd3  11130  bcval5  11150  bcpasc  11153  bcm1n  11156  hashennn  11168  fihasheqf1oi  11175  hashsng  11186  fihashfn  11189  hashun  11194  fihashss  11206  fihashssdif  11208  hashfz  11211  hashxp  11216  hashmap  11217  hashpwfi  11218  fimaxq  11219  sseqn  11228  hashfibclem  11231  zfz1isolem1  11237  seq3coll  11239  hashdmprop2dom  11241  wrdf  11255  wrdlenge2n0  11285  fstwrdne0  11289  wrdred1hash  11293  ccatvalfn  11314  ccatsymb  11315  ccatlid  11319  ccatrid  11320  ccatrn  11322  ccatalpha  11326  eqs1  11341  ccats1val2  11353  fzowrddc  11364  swrdlen  11369  swrdnd  11376  swrd0g  11377  swrdfv2  11380  swrdwrdsymbg  11381  pfxn0  11405  pfxwrdsymbg  11407  pfxsuff1eqwrdeq  11416  swrdswrd  11422  ccats1pfxeq  11431  ccats1pfxeqrex  11432  wrdind  11439  wrd2ind  11440  swrdccatin1  11442  pfxccatin12lem4  11443  swrdccatin2  11446  pfxccatin12  11450  pfxccat3a  11455  swrdccat3blem  11456  pfxccatid  11458  swrdccatin2d  11461  shftfn  11534  cjth  11556  cjmulrcl  11597  reim0bd  11654  rerebd  11655  cjrebd  11656  caucvgre  11691  cvg1nlemcxze  11692  cvg1nlemcau  11694  cvg1nlemres  11695  recvguniq  11705  resqrexlemover  11720  resqrexlemdec  11721  resqrexlemgt0  11730  resqrexlemoverl  11731  resqrexlemglsq  11732  rersqrtthlem  11740  sqrtgt0  11744  leabs  11784  absexpzap  11790  absle  11799  recvalap  11807  abstri  11814  abs2dif  11816  amgm2  11828  absne0d  11897  maxleim  11915  maxabslemab  11916  maxabslemlub  11917  maxltsup  11928  zmaxcl  11934  fimaxre2  11937  minmax  11940  rpmincl  11948  bdtrilem  11949  bdtri  11950  xrmaxleim  11954  xrmaxiflemcom  11959  xrmaxltsup  11968  xrmaxadd  11971  xrminmax  11975  xrminrpcl  11984  climconst  12000  climuni  12003  2clim  12011  climcn1  12018  climcn2  12019  reccn2ap  12023  climge0  12035  climle  12044  climsqz  12045  climsqz2  12046  serf0  12062  summodclem3  12091  summodclem2a  12092  fsumcl2lem  12109  sumpr  12124  sumtp  12125  fsum0diaglem  12151  mptfzshft  12153  fsumle  12174  fsumlt  12175  divcnv  12208  trireciplem  12211  expcnvap0  12213  expcnv  12215  explecnv  12216  geosergap  12217  cvgratnnlembern  12234  cvgratnnlemabsle  12238  cvgratnnlemsumlt  12239  cvgratz  12243  cvgratgt0  12244  mertenslemi1  12246  mertenslem2  12247  mertensabs  12248  clim2divap  12251  prodmodclem3  12286  prodmodclem2a  12287  fprodseq  12294  fprodmul  12302  fprodfac  12326  fprodconst  12331  fprodap0  12332  fprodap0f  12347  fprodle  12351  eftcl  12365  ef0lem  12371  efsub  12392  eftlub  12401  eflegeo  12412  tanval2ap  12424  sinadd  12447  cos2t  12461  cos2tsin  12462  sin01bnd  12468  cos01bnd  12469  eirraplem  12488  dvdsval2  12501  dvdsdc  12509  dvds0lem  12512  zdvdsdc  12523  dvdscmulr  12531  dvdsmulcr  12532  fsumdvds  12553  dvdslelemd  12554  divconjdvds  12560  dvdsext  12566  fzm1ndvds  12567  dvdsmod  12573  3dvds  12575  oexpneg  12588  2tp1odd  12595  mulsucdiv2z  12596  2teven  12598  zeo5  12599  opeo  12608  omeo  12609  nn0ob  12619  divalglemnqt  12631  bitsdc  12658  bits0o  12661  bitsfzolem  12665  bitsfzo  12666  bitsmod  12667  bitscmp  12669  bitsinv1lem  12672  gcddvds  12684  dvdslegcd  12685  gcdneg  12703  bezoutlemnewy  12717  bezoutlemstep  12718  bezoutlema  12720  bezoutlemb  12721  bezoutlemmo  12727  bezoutlemle  12729  bezoutlemsup  12730  dfgcd3  12731  bezout  12732  dfgcd2  12735  uzwodc  12758  lcmcllem  12789  lcmneg  12796  lcmgcdlem  12799  lcmdvds  12801  lcmid  12802  3lcm2e6woprm  12808  6lcm4e12  12809  ncoprmgcdne1b  12811  mulgcddvds  12816  divgcdcoprmex  12824  cncongr1  12825  cncongr2  12826  isprm2lem  12838  prmind2  12842  dvdsnprmd  12847  prm2orodd  12848  sqnprm  12858  isprm5lem  12863  rpexp  12875  sqrt2irrlem  12883  oddpwdclemdc  12895  sqrt2irraplemnn  12901  qnumdencoprm  12915  qeqnumdivden  12916  nn0gcdsq  12922  nn0sqrtelqelz  12928  nonsq  12929  phicl2  12936  phibnd  12939  hashdvds  12943  phiprmpw  12944  phimullem  12947  eulerthlemrprm  12951  eulerthlema  12952  eulerthlemth  12954  prmdiveq  12958  hashgcdlem  12960  odzdvds  12968  modprminv  12972  nnnn0modprm0  12978  modprmn0modprm0  12979  pythagtriplem10  12992  pythagtriplem19  13005  pythagtrip  13006  pcpre1  13015  pcpremul  13016  pceu  13018  pcmul  13024  pcdiv  13025  pcqmul  13026  pcqdiv  13030  pcexp  13032  pcdvdsb  13043  pcidlem  13046  pcdvdstr  13050  pcgcd1  13051  pc2dvds  13053  pcprmpw2  13056  difsqpwdvds  13061  pcaddlem  13062  pcadd  13063  pcadd2  13064  pcmpt  13066  pcmptdvds  13068  pcprod  13069  fldivp1  13071  pcfaclem  13072  pcfac  13073  pcbc  13074  qexpz  13075  pockthlem  13079  pockthg  13080  1arithlem4  13089  1arith  13090  1arith2  13091  4sqlem6  13106  4sqlem8  13108  4sqlem9  13109  4sqlem10  13110  4sqexercise1  13121  4sqexercise2  13122  4sqlemsdc  13123  4sqlem11  13124  4sqlem12  13125  4sqlem15  13128  4sqlem16  13129  4sqlem17  13130  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemimin  13193  ballotfilem1c  13195  ballotfilemro  13210  ballotfilemfrcn0  13217  znnen  13233  ennnfonelemk  13235  ennnfonelemkh  13247  ennnfonelemhf1o  13248  ennnfonelemrnh  13251  ennnfonelemfun  13252  ennnfonelemf1  13253  ennnfonelemrn  13254  ennnfonelemnn0  13257  ctinfomlemom  13262  ctiunctlemudc  13272  unct  13277  omctfn  13278  ssnnctlemct  13281  nninfdclemp1  13285  nninfdc  13288  structfung  13313  setsfun  13331  setsfun0  13332  setscom  13336  strslfv3  13342  setsslid  13347  imasaddfnlemg  13578  imasaddvallemg  13579  mgmsscl  13624  plusffng  13628  mgmplusf  13629  mgm0  13632  mgm1  13633  opifismgmdc  13634  gsumfzval  13654  gsumprval  13662  sgrp1  13674  issgrpd  13675  mndpfo  13699  mndfo  13700  mnd1  13710  0subm  13739  mhmima  13746  grpinvfng  13799  isgrpinv  13809  grpinvid  13815  grpinvf1o  13825  grpinvadd  13833  grpsubf  13834  grpsubsub4  13848  grplactcnv  13857  grp1  13861  grp1inv  13862  qusgrp2  13866  mulgfng  13877  subginv  13934  resgrpisgrp  13948  subgintm  13951  0subg  13952  0nsg  13967  qusinv  13989  ghminv  14003  ghmrn  14010  ghmeql  14020  ghmnsgima  14021  kerf1ghm  14027  conjnmz  14032  gfsumval  14102  gsumshift  14105  gsumgfsum  14106  gfsumsn  14107  gfsump1  14108  prdsplusgsgrpcl  14132  prdsplusgcl  14134  prdsidlem  14135  prdsinvlem  14138  prdsinvgd  14140  pwsdiagel  14152  pwssnf1o  14153  rngass  14178  rngmneg1  14186  rngmneg2  14187  qusrng  14197  srgideu  14215  srgidmlem  14221  srgpcomp  14233  srg1expzeq1  14238  ringcl  14256  ringideu  14260  ringidmlem  14265  ringnegl  14294  ringnegr  14295  ring1  14302  qusring2  14309  opprringbg  14323  dvdsrd  14339  dvdsr01  14349  isunitd  14351  unitinvcl  14368  unitinvinv  14369  unitnegcl  14375  rhmmul  14409  rhmf1o  14413  nzrunit  14433  lringuplu  14441  subrngintm  14458  subrgsubm  14480  subrgintm  14489  rrgsupp  14512  ringunitap  14531  aprsym  14534  aprnzr  14537  aprlring  14538  drnglring  14545  drngunitap  14546  scaffng  14583  lmodscaf  14584  lsssn0  14644  lss1d  14657  lssintclm  14658  lspval  14664  lspcl  14665  lspsnid  14681  lspprid1  14685  lspsn  14690  sraval  14711  rspcl  14765  rspssid  14766  rspssp  14768  rnglidlmmgm  14770  rnglidlmsgrp  14771  cnfldneg  14847  zringinvg  14878  expghmap  14881  znzrhfo  14922  znf1o  14925  znhash  14930  znidomb  14932  znrrg  14934  psrbagfsupp  14945  psrbagfi  14949  psrbaglecl  14950  psrbagaddclfi  14951  psrbagcon  14952  psraddcl  14961  psr0cl  14962  psrnegcl  14964  psrneg  14968  psr1clfi  14969  mplsubgfilemm  14979  mplsubgfilemcl  14980  baspartn  15041  eltg3i  15047  tgclb  15056  topbas  15058  2basgeng  15073  topcld  15100  0cld  15103  uncld  15104  neif  15132  elnei  15143  0nei  15157  restbasg  15159  iscnp4  15209  cnpnei  15210  cnclima  15214  cncnp  15221  cnrest2r  15228  cndis  15232  lmff  15240  lmtopcnp  15241  txbas  15249  txopn  15256  txcnp  15262  upxp  15263  txdis1cn  15269  cnmpt11  15274  cnmpt21  15282  psmetge0  15322  xmetge0  15356  xmettpos  15361  xmetrtri  15367  metrtri  15368  xblpnfps  15389  xblpnf  15390  blfps  15400  blf  15401  ssblps  15416  ssbl  15417  blbas  15424  metss2  15489  xmettxlem  15500  xmettx  15501  qtopbas  15513  divcnap  15556  cncfss  15574  cdivcncfap  15595  expcncf  15600  cnopnap  15602  maxcncf  15606  mincncf  15607  dedekindeulemuub  15608  dedekindeulemlu  15612  dedekindeu  15614  suplociccex  15616  dedekindicclemuub  15617  dedekindicclemlu  15621  dedekindicclemicc  15623  ivthinclemlopn  15627  ivthinclemuopn  15629  ivthinc  15634  ivthreinc  15636  hoverlt1  15640  ellimc3apf  15651  limcimolemlt  15655  limcimo  15656  limcresi  15657  cnplimclemle  15659  reldvg  15670  dvfgg  15679  dvidlemap  15682  dvidrelem  15683  dvidsslem  15684  dvcjbr  15699  dvcj  15700  dvrecap  15704  dveflem  15717  dvef  15718  elply2  15726  elplyr  15731  plycj  15752  plyreres  15755  reeff1oleme  15763  pilem3  15774  sinq34lt0t  15822  cosq14gt0  15823  coseq0q4123  15825  tangtx  15829  sincosq1eq  15830  cosordlem  15840  logdivlti  15872  relogbval  15942  relogbzcl  15943  nnlogbexp  15950  logbgcd1irr  15958  logbgcd1irraplemexp  15959  logbgcd1irraplemap  15960  pellexlem1  15971  pellexlem3  15973  wilthlem1  15974  mpodvdsmulf1o  15984  mersenne  15991  perfectlem2  15994  perfect  15995  zabsle1  15998  lgslem1  15999  lgsval  16003  lgsfvalg  16004  lgsfcl2  16005  lgsval2lem  16009  lgscl1  16022  lgsmod  16025  lgsdir2lem5  16031  lgsdir2  16032  lgsdilem2  16035  lgsdi  16036  lgsne0  16037  gausslemma2dlem0c  16050  gausslemma2dlem0h  16055  gausslemma2dlem1a  16057  gausslemma2dlem1f1o  16059  gausslemma2dlem3  16062  lgseisenlem1  16069  lgseisenlem2  16070  lgseisenlem3  16071  lgseisenlem4  16072  lgseisen  16073  lgsquadlem1  16076  lgsquadlem2  16077  lgsquadlem3  16078  lgsquad3  16083  2lgslem3b1  16097  2lgslem3c1  16098  2lgs  16103  2lgsoddprmlem2  16105  2lgsoddprm  16112  2sqlem3  16116  2sqlem8  16122  2sqlem10  16124  structgrssvtx  16163  structgrssiedg  16164  ushgruhgr  16201  uhgrun  16207  incistruhgr  16211  upgrop  16225  upgruhgr  16232  umgrupgr  16233  umgrnloopv  16235  umgredgprv  16236  umgr0e  16239  upgr1edc  16242  umgr1een  16246  upgrun  16247  umgrun  16249  umgrislfupgrdom  16252  upgredg  16265  umgrpredgv  16268  usgrop  16287  usgrausgrien  16290  ausgrumgrien  16291  ausgrusgrien  16292  uspgrupgrushgr  16303  usgrumgr  16305  usgrumgruspgr  16306  usgruspgrben  16307  usgrislfuspgrdom  16311  edgssv2en  16320  usgrf1oedg  16326  usgredg4  16336  usgredg2vlem2  16344  usgredg2v  16345  ushgredgedg  16347  ushgredgedgloop  16349  usgrstrrepeen  16352  usgr0e  16353  uhgr0v0e  16355  uspgr1edc  16361  usgr1e  16362  griedg0ssusgr  16372  subgrprop3  16383  subgruhgredgdm  16391  subuhgr  16393  subupgr  16394  subumgr  16395  subusgr  16396  uhgrspansubgrlem  16397  1loopgrvd2fi  16426  1loopgrvd0fi  16427  1hevtxdg0fi  16428  vdegp1aid  16435  vdegp1bid  16436  wlkm  16460  wlkvtxiedg  16466  wlkvtxiedgg  16467  wlkeq  16475  wlk1walkdom  16480  uspgr2wlkeq  16486  uspgr2wlkeqi  16488  upgr2wlkdc  16498  wlkres  16500  trlreslem  16510  clwwlkccatlem  16521  clwwlkn1loopb  16541  clwwlkext2edg  16543  clwwlknonex2lem1  16558  clwwlknonex2  16560  trlsegvdeglem2  16582  trlsegvdeglem3  16583  eupth2lem3lem4fi  16594  eupth2lemsfi  16599  fnmptd  16702  bj-sels  16810  bj-nnelon  16855  pw1map  16895  pwle2  16898  pwf1oexmid  16899  pw1nct  16903  nninfall  16913  nninfsellemdc  16914  nninfself  16917  nnnninfex  16926  nninfnfiinf  16927  refeq  16934  isomninnlem  16940  cvgcmp2nlemabs  16942  trilpolemlt1  16951  trirec0  16954  apdifflemf  16956  apdifflemr  16957  apdiff  16958  qdiff  16959  iswomninnlem  16960  iswomni0  16962  ismkvnnlem  16963  reap0  16969  cndcap  16970  trimul0or  16971