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  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  eqbrtrd  4150  3brtr4d  4160  snelpwi  4349  prelpwi  4352  pwel  4356  ordelon  4526  onin  4529  elelsuc  4552  onsuc  4646  onsucb  4648  onintonm  4662  omsinds  4767  sosng  4846  relssdv  4865  eqbrrdv  4870  eqrelrdv2  4872  relsnopg  4877  breldmg  4985  elrnmptdv  5034  iss  5107  xpimasn  5234  elxp4  5273  elxp5  5274  iotam  5367  funssres  5418  f0rn0  5585  fimadmfo  5622  sefvex  5714  fdmeu  5743  fvun1  5766  eqfnfvd  5803  fvimacnvi  5817  fvimacnv  5818  fvelrn  5833  fmpt3d  5858  fmpt2d  5864  resflem  5866  fmptco  5868  fsn  5874  funopsn  5885  fncofn  5887  ftpg  5893  fconst2g  5924  funfvima3  5946  elabrexg  5958  foeqcnvco  5990  f1eqcocnv  5991  fliftfun  5996  fliftfund  5997  fliftval  6000  riota5f  6059  f1ofveu  6067  f1ocnvd  6286  f1opw2  6290  f1o3d  6292  off  6309  offval2  6312  ofrfval2  6313  offveq  6317  caofref  6321  caofinvl  6322  elxp6  6397  cnvf1olem  6454  f2ndf  6456  f1od2  6465  elmpom  6468  fvn0elsupp  6485  suppfnss  6491  tposf12  6534  smores2  6559  tfrlemisucaccv  6590  tfrlemibfn  6593  tfr1onlemsucaccv  6606  tfr1onlembfn  6609  tfrcllemsucaccv  6619  tfrcllembfn  6622  tfrcl  6629  tfri3  6632  frecabcl  6664  nnsucsssuc  6759  ersym  6813  ertr  6816  swoer  6829  erth  6847  riinerm  6876  qliftfund  6886  eroprf  6896  ecopoverg  6904  th3qlem1  6905  mapfoss  6941  elmapssres  6948  mapss  6967  fdiagfn  6968  ixpssmap2g  7003  mapsnf1o  7013  f1oen4g  7032  f1dom4g  7033  f1dom2g  7036  dom3d  7054  en2prd  7100  dom1oi  7111  pw2f1odclem  7128  fopwdom  7130  mapxpen  7142  nndomo  7159  dif1en  7177  findcard2  7187  findcard2s  7188  diffisn  7191  fimax2gtrilemstep  7199  eqsndc  7204  fientri3  7216  tpfidceq  7231  fiintim  7232  opabfi  7241  f1dmvrnfibi  7252  sbthlemi6  7273  0fsupp  7292  elfir  7301  fifo  7308  2omap  7312  supelti  7336  supsnti  7339  cnvinfex  7352  ordiso2  7369  updjud  7416  djudom  7427  difinfsn  7434  ctssdc  7447  enumctlemm  7448  enumct  7449  nninfninc  7457  enomnilem  7472  fodjuf  7479  ismkvnex  7489  omnimkv  7490  enmkvlem  7495  enwomnilem  7503  nninfdcinf  7505  nninfwlporlem  7507  isnumi  7521  exmidfodomrlemrALT  7549  finacn  7554  djudoml  7569  djudomr  7570  netap  7614  2omotaplemap  7617  2omotaplemst  7618  exmidapne  7620  cc2lem  7626  cc3  7628  ltsopi  7681  pitri3or  7683  ltdcpi  7684  indpi  7703  enqdc  7722  enqdc1  7723  addcmpblnq  7728  mulcanenq  7746  recrecnq  7755  nqtri3or  7757  ltdcnq  7758  ltsonq  7759  ltaddnq  7768  subhalfnqq  7775  archnqq  7778  prarloclemarch2  7780  enq0tr  7795  nqnq0  7802  addcmpblnq0  7804  mulcanenq0ec  7806  nnnq0lem1  7807  nqpnq0nq  7814  nq0m0r  7817  nq02m  7826  prarloclemlt  7854  prarloclemcalc  7863  addlocpr  7897  nqprl  7912  nqpru  7913  addnqprlemrl  7918  addnqprlemru  7919  prmuloclemcalc  7926  mullocprlem  7931  mulnqprlemrl  7934  mulnqprlemru  7935  1idprl  7951  1idpru  7952  ltaddpr  7958  ltexprlemm  7961  ltexprlemopl  7962  ltexprlemopu  7964  ltexprlemdisj  7967  ltexprlemrl  7971  ltexprlemru  7973  addcanprleml  7975  addcanprlemu  7976  addcanprg  7977  prplnqu  7981  recexprlemloc  7992  recexprlem1ssl  7994  recexprlem1ssu  7995  aptiprleml  8000  aptiprlemu  8001  archpr  8004  cauappcvgprlemm  8006  cauappcvgprlemopl  8007  cauappcvgprlemloc  8013  cauappcvgprlemladdfu  8015  cauappcvgprlemladdfl  8016  cauappcvgprlem1  8020  cauappcvgprlem2  8021  caucvgprlemnkj  8027  caucvgprlemopl  8030  caucvgprlemloc  8036  caucvgprlemladdfu  8038  caucvgprlem2  8041  caucvgprprlemnkltj  8050  caucvgprprlemopl  8058  caucvgprprlemloc  8064  caucvgprprlemexbt  8067  caucvgprprlemaddq  8069  caucvgprprlem2  8071  suplocexprlemmu  8079  suplocexprlemru  8080  suplocexprlemloc  8082  suplocexprlemlub  8085  prsrlem1  8103  0idsr  8128  1idsr  8129  recexgt0sr  8134  archsr  8143  prsradd  8147  caucvgsrlemcau  8154  caucvgsrlembound  8155  caucvgsrlemoffgt1  8160  suplocsrlemb  8167  suplocsrlempr  8168  suplocsrlem  8169  pitonnlem1p1  8207  pitonn  8209  pitoregt0  8210  peano2nnnn  8214  recidpirq  8219  axcaucvglemval  8258  leid  8403  nltled  8441  readdcan  8460  addneintrd  8508  addneintr2d  8509  pncan  8526  subsub2  8548  subsub4  8553  negned  8628  subne0d  8640  subneintrd  8675  subneintr2d  8677  subeq0bd  8700  subdi  8706  gt0add  8895  rimul  8907  rereim  8908  ltmul1a  8913  apreim  8925  apirr  8927  mulap0r  8937  msqge0  8938  mulge0  8941  gt0ap0  8948  ltap  8955  subap0d  8966  recexaplem2  8974  mulap0bad  8981  mulap0bbd  8982  mul0eqap  8994  divrecap  9012  div0ap  9026  div1  9027  recrecap  9033  divdivdivap  9037  ddcanap  9050  rerecclap  9054  div2negap  9059  diveqap1bd  9160  recgt0  9174  prodgt0  9176  lemul1a  9182  recp1lt1  9223  squeeze0  9228  peano2nn  9299  div4p1lem1div2  9542  arch  9543  peano2z  9663  peano2zm  9665  ztri3or  9670  nn0n0n1ge2  9698  zextle  9720  gtndiv  9724  suprzclex  9727  nn0ind-raph  9746  uzid  9919  uzneg  9924  uztric  9927  uz11  9928  eluzp1l  9930  qdivcl  10026  irrmul  10030  irrmulap  10031  rpnegap  10070  negelrpd  10072  ledivge1le  10110  mul2lt0rlt0  10143  mul2lt0rgt0  10144  nn0ledivnn  10151  ltpnf  10165  mnflt  10168  pnfge  10174  mnfle  10177  xrlttr  10180  xrltso  10181  xrlttri3  10182  xrleid  10185  xaddass2  10255  xltadd1  10261  xlt2add  10265  xleaddadd  10272  lincmble  10389  iccf1o  10390  fztri3or  10426  fznlem  10428  fzn  10429  fzsplit2  10438  fzsplit3  10441  fznatpl1  10466  uzsplit  10482  fseq1p1m1  10484  fzm1  10490  fznn0sub2  10518  difelfznle  10525  1fv  10529  fzodcel  10543  fzospliti  10568  fzouzsplit  10571  eluzgtdifelfzo  10598  exfzdc  10642  subfzo0  10644  zsupcllemstep  10645  zsupcl  10647  zssinfcl  10648  infssuzex  10649  infssuzcldc  10651  infssfzcldc  10652  infssfzledc  10653  suprzubdc  10654  nninfdcex  10655  qdcle  10664  exbtwnz  10668  qbtwnrelemcalc  10673  flqlelt  10694  qfraclt1  10698  qfracge0  10699  flqltnz  10705  btwnzge0  10718  flhalf  10720  fldiv4lem1div2uz2  10724  ceiqle  10733  intfracq  10740  mulqmod0  10750  modqge0  10752  modqlt  10753  modqid  10769  modqid0  10770  m1modge3gt1  10791  modqltm1p1mod  10796  q2txmodxeq0  10804  modaddmodlo  10808  modsumfzodifsn  10816  addmodlteq  10818  frecuzrdgtcl  10832  frecuzrdgtclt  10841  uzennn  10856  uzsinds  10864  seqf  10884  seqf2  10888  monoord2  10906  iseqf1olemqk  10927  iseqf1olemjpcl  10928  iseqf1olemqpcl  10929  seq3f1olemqsumkj  10931  seq3f1olemqsum  10933  seq3f1olemstep  10934  seq3f1oleml  10936  seqf1oglem1  10939  ser3le  10957  exp3vallem  10960  exp3val  10961  expp1  10966  expcllem  10970  ltexp2a  11011  leexp2a  11012  resq01  11078  nn0ltexp2  11130  faclbnd  11162  faclbnd2  11163  faclbnd3  11164  bcval5  11184  bcpasc  11187  bcm1n  11190  hashennn  11202  fihasheqf1oi  11209  hashsng  11220  fihashfn  11223  hashun  11228  fihashss  11240  fihashssdif  11242  hashfz  11245  hashxp  11250  hashmap  11251  hashpwfi  11252  fimaxq  11253  sseqn  11262  hashfibclem  11265  hashf1lem2  11269  hashf1  11270  zfz1isolem1  11275  seq3coll  11277  hashdmprop2dom  11279  wrdf  11293  wrdlenge2n0  11323  fstwrdne0  11327  wrdred1hash  11331  ccatvalfn  11352  ccatsymb  11353  ccatlid  11357  ccatrid  11358  ccatrn  11360  ccatalpha  11364  eqs1  11379  ccats1val2  11391  fzowrddc  11402  swrdlen  11407  swrdnd  11414  swrd0g  11415  swrdfv2  11418  swrdwrdsymbg  11419  pfxn0  11443  pfxwrdsymbg  11445  pfxsuff1eqwrdeq  11454  swrdswrd  11460  ccats1pfxeq  11469  ccats1pfxeqrex  11470  wrdind  11477  wrd2ind  11478  swrdccatin1  11480  pfxccatin12lem4  11481  swrdccatin2  11484  pfxccatin12  11488  pfxccat3a  11493  swrdccat3blem  11494  pfxccatid  11496  swrdccatin2d  11499  shftfn  11572  cjth  11594  cjmulrcl  11635  sq01  11643  reim0bd  11693  rerebd  11694  cjrebd  11695  caucvgre  11730  cvg1nlemcxze  11731  cvg1nlemcau  11733  cvg1nlemres  11734  recvguniq  11744  resqrexlemover  11759  resqrexlemdec  11760  resqrexlemgt0  11769  resqrexlemoverl  11770  resqrexlemglsq  11771  rersqrtthlem  11779  sqrtgt0  11783  leabs  11823  absexpzap  11829  absle  11838  recvalap  11846  abstri  11853  abs2dif  11855  amgm2  11867  absne0d  11936  maxleim  11954  maxabslemab  11955  maxabslemlub  11956  maxltsup  11967  zmaxcl  11973  fimaxre2  11976  minmax  11979  rpmincl  11987  bdtrilem  11988  bdtri  11989  xrmaxleim  11993  xrmaxiflemcom  11998  xrmaxltsup  12007  xrmaxadd  12010  xrminmax  12014  xrminrpcl  12023  climconst  12039  climuni  12042  2clim  12050  climcn1  12057  climcn2  12058  reccn2ap  12062  climge0  12074  climle  12083  climsqz  12084  climsqz2  12085  serf0  12101  summodclem3  12130  summodclem2a  12131  fsumcl2lem  12148  sumpr  12163  sumtp  12164  fsum0diaglem  12190  mptfzshft  12192  fsumle  12213  fsumlt  12214  divcnv  12247  trireciplem  12250  expcnvap0  12252  expcnv  12254  explecnv  12255  geosergap  12256  cvgratnnlembern  12273  cvgratnnlemabsle  12277  cvgratnnlemsumlt  12278  cvgratz  12282  cvgratgt0  12283  mertenslemi1  12285  mertenslem2  12286  mertensabs  12287  clim2divap  12290  prodmodclem3  12325  prodmodclem2a  12326  fprodseq  12333  fprodmul  12341  fprodfac  12365  fprodconst  12370  fprodap0  12371  fprodap0f  12386  fprodle  12390  eftcl  12404  ef0lem  12410  efsub  12431  eftlub  12440  eflegeo  12451  tanval2ap  12463  sinadd  12486  cos2t  12500  cos2tsin  12501  sin01bnd  12507  cos01bnd  12508  eirraplem  12527  dvdsval2  12540  dvdsdc  12548  dvds0lem  12551  zdvdsdc  12562  dvdscmulr  12570  dvdsmulcr  12571  fsumdvds  12592  dvdslelemd  12593  divconjdvds  12599  dvdsext  12605  fzm1ndvds  12606  dvdsmod  12612  3dvds  12614  oexpneg  12627  2tp1odd  12634  mulsucdiv2z  12635  2teven  12637  zeo5  12638  opeo  12647  omeo  12648  nn0ob  12658  divalglemnqt  12670  bitsdc  12697  bits0o  12700  bitsfzolem  12704  bitsfzo  12705  bitsmod  12706  bitscmp  12708  bitsinv1lem  12711  gcddvds  12723  dvdslegcd  12724  gcdneg  12742  bezoutlemnewy  12756  bezoutlemstep  12757  bezoutlema  12759  bezoutlemb  12760  bezoutlemmo  12766  bezoutlemle  12768  bezoutlemsup  12769  dfgcd3  12770  bezout  12771  dfgcd2  12774  uzwodc  12797  lcmcllem  12828  lcmneg  12835  lcmgcdlem  12838  lcmdvds  12840  lcmid  12841  3lcm2e6woprm  12847  6lcm4e12  12848  ncoprmgcdne1b  12850  mulgcddvds  12855  divgcdcoprmex  12863  cncongr1  12864  cncongr2  12865  isprm2lem  12877  prmind2  12881  dvdsnprmd  12886  prm2orodd  12887  sqnprm  12897  isprm5lem  12902  rpexp  12914  sqrt2irrlem  12922  oddpwdclemdc  12934  sqrt2irraplemnn  12940  qnumdencoprm  12954  qeqnumdivden  12955  nn0gcdsq  12961  nn0sqrtelqelz  12967  nonsq  12968  phicl2  12975  phibnd  12978  hashdvds  12982  phiprmpw  12983  phimullem  12986  eulerthlemrprm  12990  eulerthlema  12991  eulerthlemth  12993  prmdiveq  12997  hashgcdlem  12999  odzdvds  13007  modprminv  13011  nnnn0modprm0  13017  modprmn0modprm0  13018  pythagtriplem10  13031  pythagtriplem19  13044  pythagtrip  13045  pcpre1  13054  pcpremul  13055  pceu  13057  pcmul  13063  pcdiv  13064  pcqmul  13065  pcqdiv  13069  pcexp  13071  pcdvdsb  13082  pcidlem  13085  pcdvdstr  13089  pcgcd1  13090  pc2dvds  13092  pcprmpw2  13095  difsqpwdvds  13100  pcaddlem  13101  pcadd  13102  pcadd2  13103  pcmpt  13105  pcmptdvds  13107  pcprod  13108  fldivp1  13110  pcfaclem  13111  pcfac  13112  pcbc  13113  qexpz  13114  pockthlem  13118  pockthg  13119  1arithlem4  13128  1arith  13129  1arith2  13130  4sqlem6  13145  4sqlem8  13147  4sqlem9  13148  4sqlem10  13149  4sqexercise1  13160  4sqexercise2  13161  4sqlemsdc  13162  4sqlem11  13163  4sqlem12  13164  4sqlem15  13167  4sqlem16  13168  4sqlem17  13169  ballotfilemfc0  13215  ballotfilemfcc  13216  ballotfilemimin  13232  ballotfilem1c  13234  ballotfilemro  13249  ballotfilemfrcn0  13256  znnen  13272  ennnfonelemk  13274  ennnfonelemkh  13286  ennnfonelemhf1o  13287  ennnfonelemrnh  13290  ennnfonelemfun  13291  ennnfonelemf1  13292  ennnfonelemrn  13293  ennnfonelemnn0  13296  ctinfomlemom  13301  ctiunctlemudc  13311  unct  13316  omctfn  13317  ssnnctlemct  13320  nninfdclemp1  13324  nninfdc  13327  structfung  13352  setsfun  13370  setsfun0  13371  setscom  13375  strslfv3  13381  setsslid  13386  imasaddfnlemg  13618  imasaddvallemg  13619  mgmsscl  13664  plusffng  13668  mgmplusf  13669  mgm0  13672  mgm1  13673  opifismgmdc  13674  gzsumfzval  13694  sgrp1  13709  issgrpd  13710  mndpfo  13734  mndfo  13735  mnd1  13745  0subm  13774  mhmima  13781  grpinvfng  13832  isgrpinv  13842  grpinvid  13848  grpinvf1o  13858  grpinvadd  13866  grpsubf  13867  grpsubsub4  13881  grplactcnv  13890  grp1  13894  grp1inv  13895  qusgrp2  13899  mulgfng  13910  subginv  13967  resgrpisgrp  13981  subgintm  13984  0subg  13985  0nsg  14000  qusinv  14022  ghminv  14036  ghmrn  14043  ghmeql  14053  ghmnsgima  14054  kerf1ghm  14060  conjnmz  14065  gzsumshift  14132  gsumvalfi  14135  gzsumgsum  14138  gsumsncmn  14139  gsump1  14140  gsumf1ofi  14143  gsumsubmclfi  14146  prdsplusgsgrpcl  14173  prdsplusgcl  14175  prdsidlem  14176  prdsinvlem  14179  prdsinvgd  14181  pwsdiagel  14193  pwssnf1o  14194  rngass  14221  rngmneg1  14229  rngmneg2  14230  qusrng  14240  srgideu  14259  srgidmlem  14265  srgpcomp  14277  srg1expzeq1  14282  ringcl  14300  ringideu  14304  ringidmlem  14310  ringnegl  14339  ringnegr  14340  ring1  14347  qusring2  14354  opprringbg  14368  dvdsrd  14384  dvdsr01  14394  isunitd  14396  unitinvcl  14413  unitinvinv  14414  unitnegcl  14420  rhmmul  14454  rhmf1o  14458  nzrunit  14478  lringuplu  14486  subrngintm  14503  subrgsubm  14525  subrgintm  14534  rrgsupp  14557  ringunitap  14576  aprsym  14579  aprnzr  14582  aprlring  14583  drnglring  14590  drngunitap  14591  scaffng  14629  lmodscaf  14630  lsssn0  14690  lss1d  14703  lssintclm  14704  lspval  14710  lspcl  14711  lspsnid  14727  lspprid1  14731  lspsn  14736  sraval  14757  rspcl  14811  rspssid  14812  rspssp  14814  rnglidlmmgm  14816  rnglidlmsgrp  14817  cnfldneg  14893  zringinvg  14922  expghmap  14925  znzrhfo  14966  znf1o  14969  znhash  14974  znidomb  14976  znrrg  14978  psrbagfsupp  15038  psrbagfi  15042  psrbaglecl  15043  psrbagaddclfi  15044  psrbagcon  15045  psraddcl  15054  psr0cl  15055  psrnegcl  15057  psrneg  15061  psr1clfi  15062  mplsubgfilemm  15072  mplsubgfilemcl  15073  baspartn  15134  eltg3i  15140  tgclb  15149  topbas  15151  2basgeng  15166  topcld  15193  0cld  15196  uncld  15197  neif  15225  elnei  15236  0nei  15250  restbasg  15252  iscnp4  15302  cnpnei  15303  cnclima  15307  cncnp  15314  cnrest2r  15321  cndis  15325  lmff  15333  lmtopcnp  15334  txbas  15342  txopn  15349  txcnp  15355  upxp  15356  txdis1cn  15362  cnmpt11  15367  cnmpt21  15375  psmetge0  15415  xmetge0  15449  xmettpos  15454  xmetrtri  15460  metrtri  15461  xblpnfps  15482  xblpnf  15483  blfps  15493  blf  15494  ssblps  15509  ssbl  15510  blbas  15517  metss2  15582  xmettxlem  15593  xmettx  15594  qtopbas  15606  divcnap  15649  cncfss  15667  cdivcncfap  15688  expcncf  15693  cnopnap  15695  maxcncf  15699  mincncf  15700  dedekindeulemuub  15701  dedekindeulemlu  15705  dedekindeu  15707  suplociccex  15709  dedekindicclemuub  15710  dedekindicclemlu  15714  dedekindicclemicc  15716  ivthinclemlopn  15720  ivthinclemuopn  15722  ivthinc  15727  ivthreinc  15729  hoverlt1  15733  ellimc3apf  15744  limcimolemlt  15748  limcimo  15749  limcresi  15750  cnplimclemle  15752  reldvg  15763  dvfgg  15772  dvidlemap  15775  dvidrelem  15776  dvidsslem  15777  dvcjbr  15792  dvcj  15793  dvrecap  15797  dveflem  15810  dvef  15811  elply2  15819  elplyr  15824  plycj  15845  plyreres  15848  reeff1oleme  15856  pilem3  15867  sinq34lt0t  15915  cosq14gt0  15916  coseq0q4123  15918  tangtx  15922  sincosq1eq  15923  cosordlem  15933  logdivlti  15965  relogbval  16036  relogbzcl  16037  nnlogbexp  16044  logbgcd1irr  16052  logbgcd1irraplemexp  16053  logbgcd1irraplemap  16054  birthdaylem2  16071  birthdaylem3  16072  pellexlem1  16074  pellexlem3  16076  wilthlem1  16077  mpodvdsmulf1o  16087  mersenne  16094  perfectlem2  16097  perfect  16098  zabsle1  16101  lgslem1  16102  lgsval  16106  lgsfvalg  16107  lgsfcl2  16108  lgsval2lem  16112  lgscl1  16125  lgsmod  16128  lgsdir2lem5  16134  lgsdir2  16135  lgsdilem2  16138  lgsdi  16139  lgsne0  16140  gausslemma2dlem0c  16153  gausslemma2dlem0h  16158  gausslemma2dlem1a  16160  gausslemma2dlem1f1o  16162  gausslemma2dlem3  16165  lgseisenlem1  16172  lgseisenlem2  16173  lgseisenlem3  16174  lgseisenlem4  16175  lgseisen  16176  lgsquadlem1  16179  lgsquadlem2  16180  lgsquadlem3  16181  lgsquad3  16186  2lgslem3b1  16200  2lgslem3c1  16201  2lgs  16206  2lgsoddprmlem2  16208  2lgsoddprm  16215  2sqlem3  16219  2sqlem8  16225  2sqlem10  16227  structgrssvtx  16266  structgrssiedg  16267  ushgruhgr  16304  uhgrun  16310  incistruhgr  16314  upgrop  16328  upgruhgr  16335  umgrupgr  16336  umgrnloopv  16338  umgredgprv  16339  umgr0e  16342  upgr1edc  16345  umgr1een  16349  upgrun  16350  umgrun  16352  umgrislfupgrdom  16355  upgredg  16368  umgrpredgv  16371  usgrop  16390  usgrausgrien  16393  ausgrumgrien  16394  ausgrusgrien  16395  uspgrupgrushgr  16406  usgrumgr  16408  usgrumgruspgr  16409  usgruspgrben  16410  usgrislfuspgrdom  16414  edgssv2en  16423  usgrf1oedg  16429  usgredg4  16439  usgredg2vlem2  16447  usgredg2v  16448  ushgredgedg  16450  ushgredgedgloop  16452  usgrstrrepeen  16455  usgr0e  16456  uhgr0v0e  16458  uspgr1edc  16464  usgr1e  16465  griedg0ssusgr  16475  subgrprop3  16486  subgruhgredgdm  16494  subuhgr  16496  subupgr  16497  subumgr  16498  subusgr  16499  uhgrspansubgrlem  16500  1loopgrvd2fi  16529  1loopgrvd0fi  16530  1hevtxdg0fi  16531  vdegp1aid  16538  vdegp1bid  16539  wlkm  16563  wlkvtxiedg  16569  wlkvtxiedgg  16570  wlkeq  16578  wlk1walkdom  16583  uspgr2wlkeq  16589  uspgr2wlkeqi  16591  upgr2wlkdc  16601  wlkres  16603  trlreslem  16613  clwwlkccatlem  16624  clwwlkn1loopb  16644  clwwlkext2edg  16646  clwwlknonex2lem1  16661  clwwlknonex2  16663  trlsegvdeglem2  16685  trlsegvdeglem3  16686  eupth2lem3lem4fi  16697  eupth2lemsfi  16702  fnmptd  16815  bj-sels  16923  bj-nnelon  16968  pw1map  17008  pwle2  17011  pwf1oexmid  17012  pw1nct  17016  nninfall  17026  nninfsellemdc  17027  nninfself  17030  nnnninfex  17039  nninfnfiinf  17040  refeq  17047  isomninnlem  17053  cvgcmp2nlemabs  17055  trilpolemlt1  17064  trirec0  17067  apdifflemf  17069  apdifflemr  17070  apdiff  17071  qdiff  17072  iswomninnlem  17073  iswomni0  17075  ismkvnnlem  17076  reap0  17082  cndcap  17083