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 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used 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  elpwd  3697  eqbrtrd  4152  3brtr4d  4162  snelpwi  4351  prelpwi  4354  pwel  4358  ordelon  4528  onin  4531  elelsuc  4554  onsuc  4648  onsucb  4650  onintonm  4664  omsinds  4769  sosng  4848  relssdv  4867  eqbrrdv  4872  eqrelrdv2  4874  relsnopg  4879  breldmg  4987  elrnmptdv  5036  iss  5109  xpimasn  5236  elxp4  5275  elxp5  5276  iotam  5369  funssres  5420  f0rn0  5587  fimadmfo  5624  sefvex  5716  fdmeu  5746  fvun1  5769  eqfnfvd  5809  fvimacnvi  5823  fvimacnv  5824  fvelrn  5839  fmpt3d  5864  fmpt2d  5870  resflem  5872  fmptco  5874  fsn  5880  funopsn  5891  fncofn  5893  ftpg  5899  fconst2g  5930  funfvima3  5952  elabrexg  5964  foeqcnvco  5996  f1eqcocnv  5997  fliftfun  6002  fliftfund  6003  fliftval  6006  riota5f  6065  f1ofveu  6073  f1ocnvd  6292  f1opw2  6296  f1o3d  6298  off  6315  offval2  6318  ofrfval2  6319  offveq  6323  caofref  6327  caofinvl  6328  elxp6  6403  cnvf1olem  6460  f2ndf  6462  f1od2  6471  elmpom  6474  fvn0elsupp  6491  suppfnss  6497  tposf12  6540  smores2  6565  tfrlemisucaccv  6596  tfrlemibfn  6599  tfr1onlemsucaccv  6612  tfr1onlembfn  6615  tfrcllemsucaccv  6625  tfrcllembfn  6628  tfrcl  6635  tfri3  6638  frecabcl  6670  nnsucsssuc  6765  ersym  6819  ertr  6822  swoer  6835  erth  6853  riinerm  6882  qliftfund  6892  eroprf  6902  ecopoverg  6910  th3qlem1  6911  mapfoss  6947  elmapssres  6954  mapss  6973  fdiagfn  6974  ixpssmap2g  7009  mapsnf1o  7019  f1oen4g  7038  f1dom4g  7039  f1dom2g  7042  dom3d  7060  en2prd  7106  dom1oi  7117  pw2f1odclem  7134  fopwdom  7136  mapxpen  7148  nndomo  7165  dif1en  7183  findcard2  7193  findcard2s  7194  diffisn  7197  fimax2gtrilemstep  7205  eqsndc  7210  fientri3  7222  tpfidceq  7237  fiintim  7238  opabfi  7247  f1dmvrnfibi  7258  sbthlemi6  7279  0fsupp  7298  elfir  7307  fifo  7314  2omap  7318  supelti  7342  supsnti  7345  cnvinfex  7358  ordiso2  7375  updjud  7422  djudom  7433  difinfsn  7440  ctssdc  7453  enumctlemm  7454  enumct  7455  nninfninc  7463  enomnilem  7478  fodjuf  7485  ismkvnex  7495  omnimkv  7496  enmkvlem  7501  enwomnilem  7509  nninfdcinf  7511  nninfwlporlem  7513  isnumi  7527  exmidfodomrlemrALT  7555  finacn  7560  djudoml  7575  djudomr  7576  netap  7620  2omotaplemap  7623  2omotaplemst  7624  exmidapne  7626  cc2lem  7632  cc3  7634  ltsopi  7687  pitri3or  7689  ltdcpi  7690  indpi  7709  enqdc  7728  enqdc1  7729  addcmpblnq  7734  mulcanenq  7752  recrecnq  7761  nqtri3or  7763  ltdcnq  7764  ltsonq  7765  ltaddnq  7774  subhalfnqq  7781  archnqq  7784  prarloclemarch2  7786  enq0tr  7801  nqnq0  7808  addcmpblnq0  7810  mulcanenq0ec  7812  nnnq0lem1  7813  nqpnq0nq  7820  nq0m0r  7823  nq02m  7832  prarloclemlt  7860  prarloclemcalc  7869  addlocpr  7903  nqprl  7918  nqpru  7919  addnqprlemrl  7924  addnqprlemru  7925  prmuloclemcalc  7932  mullocprlem  7937  mulnqprlemrl  7940  mulnqprlemru  7941  1idprl  7957  1idpru  7958  ltaddpr  7964  ltexprlemm  7967  ltexprlemopl  7968  ltexprlemopu  7970  ltexprlemdisj  7973  ltexprlemrl  7977  ltexprlemru  7979  addcanprleml  7981  addcanprlemu  7982  addcanprg  7983  prplnqu  7987  recexprlemloc  7998  recexprlem1ssl  8000  recexprlem1ssu  8001  aptiprleml  8006  aptiprlemu  8007  archpr  8010  cauappcvgprlemm  8012  cauappcvgprlemopl  8013  cauappcvgprlemloc  8019  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  cauappcvgprlem1  8026  cauappcvgprlem2  8027  caucvgprlemnkj  8033  caucvgprlemopl  8036  caucvgprlemloc  8042  caucvgprlemladdfu  8044  caucvgprlem2  8047  caucvgprprlemnkltj  8056  caucvgprprlemopl  8064  caucvgprprlemloc  8070  caucvgprprlemexbt  8073  caucvgprprlemaddq  8075  caucvgprprlem2  8077  suplocexprlemmu  8085  suplocexprlemru  8086  suplocexprlemloc  8088  suplocexprlemlub  8091  prsrlem1  8109  0idsr  8134  1idsr  8135  recexgt0sr  8140  archsr  8149  prsradd  8153  caucvgsrlemcau  8160  caucvgsrlembound  8161  caucvgsrlemoffgt1  8166  suplocsrlemb  8173  suplocsrlempr  8174  suplocsrlem  8175  pitonnlem1p1  8213  pitonn  8215  pitoregt0  8216  peano2nnnn  8220  recidpirq  8225  axcaucvglemval  8264  leid  8409  nltled  8447  readdcan  8466  addneintrd  8514  addneintr2d  8515  pncan  8532  subsub2  8554  subsub4  8559  negned  8634  subne0d  8646  subneintrd  8681  subneintr2d  8683  subeq0bd  8706  subdi  8712  gt0add  8902  rimul  8914  rereim  8915  ltmul1a  8920  apreim  8932  apirr  8934  mulap0r  8944  msqge0  8945  mulge0  8948  gt0ap0  8955  ltap  8962  subap0d  8973  recexaplem2  8981  mulap0bad  8988  mulap0bbd  8989  mul0eqap  9001  divrecap  9019  div0ap  9033  div1  9034  recrecap  9040  divdivdivap  9044  ddcanap  9057  rerecclap  9061  div2negap  9066  diveqap1bd  9167  recgt0  9181  prodgt0  9183  lemul1a  9189  recp1lt1  9230  squeeze0  9235  peano2nn  9317  div4p1lem1div2  9561  arch  9562  peano2z  9682  peano2zm  9684  ztri3or  9689  nn0n0n1ge2  9717  zextle  9739  gtndiv  9743  suprzclex  9746  nn0ind-raph  9765  uzid  9938  uzneg  9943  uztric  9946  uz11  9947  eluzp1l  9949  qdivcl  10045  irrmul  10049  irrmulap  10050  rpnegap  10089  negelrpd  10091  ledivge1le  10129  mul2lt0rlt0  10162  mul2lt0rgt0  10163  nn0ledivnn  10170  ltpnf  10184  mnflt  10187  pnfge  10193  mnfle  10196  xrlttr  10199  xrltso  10200  xrlttri3  10201  xrleid  10204  xaddass2  10274  xltadd1  10280  xlt2add  10284  xleaddadd  10291  lincmble  10408  iccf1o  10409  fztri3or  10445  fznlem  10447  fzn  10448  fzsplit2  10457  fzsplit3  10460  fznatpl1  10485  uzsplit  10501  fseq1p1m1  10503  fzm1  10509  fznn0sub2  10537  difelfznle  10544  1fv  10548  fzodcel  10562  fzospliti  10587  fzouzsplit  10590  eluzgtdifelfzo  10617  exfzdc  10661  subfzo0  10663  zsupcllemstep  10664  zsupcl  10666  zssinfcl  10667  infssuzex  10668  infssuzcldc  10670  infssfzcldc  10671  infssfzledc  10672  suprzubdc  10673  nninfdcex  10674  qdcle  10683  exbtwnz  10687  qbtwnrelemcalc  10692  flqlelt  10713  qfraclt1  10717  qfracge0  10718  flqltnz  10724  btwnzge0  10737  flhalf  10739  fldiv4lem1div2uz2  10743  ceiqle  10752  intfracq  10759  mulqmod0  10769  modqge0  10771  modqlt  10772  modqid  10788  modqid0  10789  m1modge3gt1  10810  modqltm1p1mod  10815  q2txmodxeq0  10823  modaddmodlo  10827  modsumfzodifsn  10835  addmodlteq  10837  frecuzrdgtcl  10851  frecuzrdgtclt  10860  uzennn  10875  uzsinds  10883  seqf  10903  seqf2  10907  monoord2  10925  iseqf1olemqk  10946  iseqf1olemjpcl  10947  iseqf1olemqpcl  10948  seq3f1olemqsumkj  10950  seq3f1olemqsum  10952  seq3f1olemstep  10953  seq3f1oleml  10955  seqf1oglem1  10958  ser3le  10976  exp3vallem  10979  exp3val  10980  expp1  10985  expcllem  10989  ltexp2a  11030  leexp2a  11031  resq01  11097  nn0ltexp2  11149  faclbnd  11181  faclbnd2  11182  faclbnd3  11183  bcval5  11203  bcpasc  11206  bcm1n  11209  hashennn  11221  fihasheqf1oi  11228  hashsng  11239  fihashfn  11242  hashun  11247  fihashss  11259  fihashssdif  11261  hashfz  11264  hashxp  11269  hashmap  11270  hashpwfi  11271  fimaxq  11272  sseqn  11281  hashfibclem  11284  hashf1lem2  11288  hashf1  11289  zfz1isolem1  11294  seq3coll  11296  hashdmprop2dom  11298  wrdf  11312  wrdlenge2n0  11342  fstwrdne0  11346  wrdred1hash  11350  ccatvalfn  11371  ccatsymb  11372  ccatlid  11376  ccatrid  11377  ccatrn  11379  ccatalpha  11383  eqs1  11398  ccats1val2  11410  fzowrddc  11421  swrdlen  11426  swrdnd  11433  swrd0g  11434  swrdfv2  11437  swrdwrdsymbg  11438  pfxn0  11462  pfxwrdsymbg  11464  pfxsuff1eqwrdeq  11473  swrdswrd  11479  ccats1pfxeq  11488  ccats1pfxeqrex  11489  wrdind  11496  wrd2ind  11497  swrdccatin1  11499  pfxccatin12lem4  11500  swrdccatin2  11503  pfxccatin12  11507  pfxccat3a  11512  swrdccat3blem  11513  pfxccatid  11515  swrdccatin2d  11518  shftfn  11591  cjth  11613  cjmulrcl  11654  sq01  11662  reim0bd  11712  rerebd  11713  cjrebd  11714  caucvgre  11749  cvg1nlemcxze  11750  cvg1nlemcau  11752  cvg1nlemres  11753  recvguniq  11763  resqrexlemover  11778  resqrexlemdec  11779  resqrexlemgt0  11788  resqrexlemoverl  11789  resqrexlemglsq  11790  rersqrtthlem  11798  sqrtgt0  11802  leabs  11842  absexpzap  11848  absle  11857  recvalap  11865  abstri  11872  abs2dif  11874  amgm2  11886  absne0d  11955  maxleim  11973  maxabslemab  11974  maxabslemlub  11975  maxltsup  11986  zmaxcl  11992  fimaxre2  11995  minmax  11998  rpmincl  12006  bdtrilem  12007  bdtri  12008  xrmaxleim  12012  xrmaxiflemcom  12017  xrmaxltsup  12026  xrmaxadd  12029  xrminmax  12033  xrminrpcl  12042  climconst  12058  climuni  12061  2clim  12069  climcn1  12076  climcn2  12077  reccn2ap  12081  climge0  12093  climle  12102  climsqz  12103  climsqz2  12104  serf0  12120  summodclem3  12149  summodclem2a  12150  fsumcl2lem  12167  sumpr  12182  sumtp  12183  fsum0diaglem  12209  mptfzshft  12211  fsumle  12232  fsumlt  12233  divcnv  12266  trireciplem  12269  expcnvap0  12271  expcnv  12273  explecnv  12274  geosergap  12275  cvgratnnlembern  12292  cvgratnnlemabsle  12296  cvgratnnlemsumlt  12297  cvgratz  12301  cvgratgt0  12302  mertenslemi1  12304  mertenslem2  12305  mertensabs  12306  clim2divap  12309  prodmodclem3  12344  prodmodclem2a  12345  fprodseq  12352  fprodmul  12360  fprodfac  12384  fprodconst  12389  fprodap0  12390  fprodap0f  12405  fprodle  12409  eftcl  12423  ef0lem  12429  efsub  12450  eftlub  12459  eflegeo  12470  tanval2ap  12482  sinadd  12505  cos2t  12519  cos2tsin  12520  sin01bnd  12526  cos01bnd  12527  eirraplem  12546  dvdsval2  12559  dvdsdc  12567  dvds0lem  12570  zdvdsdc  12581  dvdscmulr  12589  dvdsmulcr  12590  fsumdvds  12611  dvdslelemd  12612  divconjdvds  12618  dvdsext  12624  fzm1ndvds  12625  dvdsmod  12631  3dvds  12633  oexpneg  12646  2tp1odd  12653  mulsucdiv2z  12654  2teven  12656  zeo5  12657  opeo  12666  omeo  12667  nn0ob  12677  divalglemnqt  12689  bitsdc  12716  bits0o  12719  bitsfzolem  12723  bitsfzo  12724  bitsmod  12725  bitscmp  12727  bitsinv1lem  12730  gcddvds  12742  dvdslegcd  12743  gcdneg  12761  bezoutlemnewy  12775  bezoutlemstep  12776  bezoutlema  12778  bezoutlemb  12779  bezoutlemmo  12785  bezoutlemle  12787  bezoutlemsup  12788  dfgcd3  12789  bezout  12790  dfgcd2  12793  uzwodc  12816  lcmcllem  12847  lcmneg  12854  lcmgcdlem  12857  lcmdvds  12859  lcmid  12860  3lcm2e6woprm  12866  6lcm4e12  12867  ncoprmgcdne1b  12869  mulgcddvds  12874  divgcdcoprmex  12882  cncongr1  12883  cncongr2  12884  isprm2lem  12896  prmind2  12900  dvdsnprmd  12905  prm2orodd  12906  sqnprm  12916  isprm5lem  12921  rpexp  12933  sqrt2irrlem  12941  oddpwdclemdc  12953  sqrt2irraplemnn  12959  qnumdencoprm  12973  qeqnumdivden  12974  nn0gcdsq  12980  nn0sqrtelqelz  12986  nonsq  12987  phicl2  12994  phibnd  12997  hashdvds  13001  phiprmpw  13002  phimullem  13005  eulerthlemrprm  13009  eulerthlema  13010  eulerthlemth  13012  prmdiveq  13016  hashgcdlem  13018  odzdvds  13026  modprminv  13030  nnnn0modprm0  13036  modprmn0modprm0  13037  pythagtriplem10  13050  pythagtriplem19  13063  pythagtrip  13064  pcpre1  13073  pcpremul  13074  pceu  13076  pcmul  13082  pcdiv  13083  pcqmul  13084  pcqdiv  13088  pcexp  13090  pcdvdsb  13101  pcidlem  13104  pcdvdstr  13108  pcgcd1  13109  pc2dvds  13111  pcprmpw2  13114  difsqpwdvds  13119  pcaddlem  13120  pcadd  13121  pcadd2  13122  pcmpt  13124  pcmptdvds  13126  pcprod  13127  fldivp1  13129  pcfaclem  13130  pcfac  13131  pcbc  13132  qexpz  13133  pockthlem  13137  pockthg  13138  1arithlem4  13147  1arith  13148  1arith2  13149  4sqlem6  13164  4sqlem8  13166  4sqlem9  13167  4sqlem10  13168  4sqexercise1  13179  4sqexercise2  13180  4sqlemsdc  13181  4sqlem11  13182  4sqlem12  13183  4sqlem15  13186  4sqlem16  13187  4sqlem17  13188  ballotfilemfc0  13234  ballotfilemfcc  13235  ballotfilemimin  13251  ballotfilem1c  13253  ballotfilemro  13268  ballotfilemfrcn0  13275  znnen  13291  ennnfonelemk  13293  ennnfonelemkh  13305  ennnfonelemhf1o  13306  ennnfonelemrnh  13309  ennnfonelemfun  13310  ennnfonelemf1  13311  ennnfonelemrn  13312  ennnfonelemnn0  13315  ctinfomlemom  13320  ctiunctlemudc  13330  unct  13335  omctfn  13336  ssnnctlemct  13339  nninfdclemp1  13343  nninfdc  13346  structfung  13371  setsfun  13389  setsfun0  13390  setscom  13394  strslfv3  13400  setsslid  13405  imasaddfnlemg  13637  imasaddvallemg  13638  mgmsscl  13683  plusffng  13687  mgmplusf  13688  mgm0  13691  mgm1  13692  opifismgmdc  13693  gzsumfzval  13713  sgrp1  13728  issgrpd  13729  mndpfo  13753  mndfo  13754  mnd1  13764  0subm  13793  mhmima  13800  grpinvfng  13851  isgrpinv  13861  grpinvid  13867  grpinvf1o  13877  grpinvadd  13885  grpsubf  13886  grpsubsub4  13900  grplactcnv  13909  grp1  13913  grp1inv  13914  qusgrp2  13918  mulgfng  13929  subginv  13986  resgrpisgrp  14000  subgintm  14003  0subg  14004  0nsg  14019  qusinv  14041  ghminv  14055  ghmrn  14062  ghmeql  14072  ghmnsgima  14073  kerf1ghm  14079  conjnmz  14084  gzsumshift  14151  gsumvalfi  14154  gzsumgsum  14157  gsumsncmn  14158  gsump1  14159  gsumf1ofi  14162  gsumsubmclfi  14165  prdsplusgsgrpcl  14192  prdsplusgcl  14194  prdsidlem  14195  prdsinvlem  14198  prdsinvgd  14200  pwsdiagel  14212  pwssnf1o  14213  rngass  14240  rngmneg1  14248  rngmneg2  14249  qusrng  14259  srgideu  14278  srgidmlem  14284  srgpcomp  14296  srg1expzeq1  14301  ringcl  14319  ringideu  14323  ringidmlem  14329  ringnegl  14358  ringnegr  14359  ring1  14366  qusring2  14373  opprringbg  14387  dvdsrd  14403  dvdsr01  14413  isunitd  14415  unitinvcl  14432  unitinvinv  14433  unitnegcl  14439  rhmmul  14473  rhmf1o  14477  nzrunit  14497  lringuplu  14505  subrngintm  14522  subrgsubm  14544  subrgintm  14553  rrgsupp  14576  ringunitap  14595  aprsym  14598  aprnzr  14601  aprlring  14602  drnglring  14609  drngunitap  14610  scaffng  14648  lmodscaf  14649  lsssn0  14709  lss1d  14722  lssintclm  14723  lspval  14729  lspcl  14730  lspsnid  14746  lspprid1  14750  lspsn  14755  sraval  14776  rspcl  14830  rspssid  14831  rspssp  14833  rnglidlmmgm  14835  rnglidlmsgrp  14836  cnfldneg  14912  zringinvg  14941  expghmap  14944  znzrhfo  14985  znf1o  14988  znhash  14993  znidomb  14995  znrrg  14997  psrbagfsupp  15057  psrbagfi  15061  psrbaglecl  15062  psrbagaddclfi  15063  psrbagcon  15064  psraddcl  15073  psr0cl  15074  psrnegcl  15076  psrneg  15080  psr1clfi  15081  mplsubgfilemm  15091  mplsubgfilemcl  15092  baspartn  15153  eltg3i  15159  tgclb  15168  topbas  15170  2basgeng  15185  topcld  15212  0cld  15215  uncld  15216  neif  15244  elnei  15255  0nei  15269  restbasg  15271  iscnp4  15321  cnpnei  15322  cnclima  15326  cncnp  15333  cnrest2r  15340  cndis  15344  lmff  15352  lmtopcnp  15353  txbas  15361  txopn  15368  txcnp  15374  upxp  15375  txdis1cn  15381  cnmpt11  15386  cnmpt21  15394  psmetge0  15434  xmetge0  15468  xmettpos  15473  xmetrtri  15479  metrtri  15480  xblpnfps  15501  xblpnf  15502  blfps  15512  blf  15513  ssblps  15528  ssbl  15529  blbas  15536  metss2  15601  xmettxlem  15612  xmettx  15613  qtopbas  15625  divcnap  15668  cncfss  15686  cdivcncfap  15707  expcncf  15712  cnopnap  15714  maxcncf  15718  mincncf  15719  dedekindeulemuub  15720  dedekindeulemlu  15724  dedekindeu  15726  suplociccex  15728  dedekindicclemuub  15729  dedekindicclemlu  15733  dedekindicclemicc  15735  ivthinclemlopn  15739  ivthinclemuopn  15741  ivthinc  15746  ivthreinc  15748  hoverlt1  15752  ellimc3apf  15763  limcimolemlt  15767  limcimo  15768  limcresi  15769  cnplimclemle  15771  reldvg  15782  dvfgg  15791  dvidlemap  15794  dvidrelem  15795  dvidsslem  15796  dvcjbr  15811  dvcj  15812  dvrecap  15816  dveflem  15829  dvef  15830  elply2  15838  elplyr  15843  plycj  15864  plyreres  15867  reeff1oleme  15875  efap1p  15882  pilem3  15887  sinq34lt0t  15935  cosq14gt0  15936  coseq0q4123  15938  tangtx  15942  sincosq1eq  15943  cosordlem  15953  logdivlti  15986  logdivlt  15999  relogbval  16059  relogbzcl  16060  nnlogbexp  16067  logbgcd1irr  16075  logbgcd1irraplemexp  16076  logbgcd1irraplemap  16077  birthdaylem2  16094  birthdaylem3  16095  pellexlem1  16097  pellexlem3  16099  wilthlem1  16100  mpodvdsmulf1o  16110  mersenne  16117  perfectlem2  16120  perfect  16121  bcmono  16124  bcmax  16125  zabsle1  16130  lgslem1  16131  lgsval  16135  lgsfvalg  16136  lgsfcl2  16137  lgsval2lem  16141  lgscl1  16154  lgsmod  16157  lgsdir2lem5  16163  lgsdir2  16164  lgsdilem2  16167  lgsdi  16168  lgsne0  16169  gausslemma2dlem0c  16182  gausslemma2dlem0h  16187  gausslemma2dlem1a  16189  gausslemma2dlem1f1o  16191  gausslemma2dlem3  16194  lgseisenlem1  16201  lgseisenlem2  16202  lgseisenlem3  16203  lgseisenlem4  16204  lgseisen  16205  lgsquadlem1  16208  lgsquadlem2  16209  lgsquadlem3  16210  lgsquad3  16215  2lgslem3b1  16229  2lgslem3c1  16230  2lgs  16235  2lgsoddprmlem2  16237  2lgsoddprm  16244  2sqlem3  16248  2sqlem8  16254  2sqlem10  16256  structgrssvtx  16295  structgrssiedg  16296  ushgruhgr  16333  uhgrun  16339  incistruhgr  16343  upgrop  16357  upgruhgr  16364  umgrupgr  16365  umgrnloopv  16367  umgredgprv  16368  umgr0e  16371  upgr1edc  16374  umgr1een  16378  upgrun  16379  umgrun  16381  umgrislfupgrdom  16384  upgredg  16397  umgrpredgv  16400  usgrop  16419  usgrausgrien  16422  ausgrumgrien  16423  ausgrusgrien  16424  uspgrupgrushgr  16435  usgrumgr  16437  usgrumgruspgr  16438  usgruspgrben  16439  usgrislfuspgrdom  16443  edgssv2en  16452  usgrf1oedg  16458  usgredg4  16468  usgredg2vlem2  16476  usgredg2v  16477  ushgredgedg  16479  ushgredgedgloop  16481  usgrstrrepeen  16484  usgr0e  16485  uhgr0v0e  16487  uspgr1edc  16493  usgr1e  16494  griedg0ssusgr  16504  subgrprop3  16515  subgruhgredgdm  16523  subuhgr  16525  subupgr  16526  subumgr  16527  subusgr  16528  uhgrspansubgrlem  16529  1loopgrvd2fi  16558  1loopgrvd0fi  16559  1hevtxdg0fi  16560  vdegp1aid  16567  vdegp1bid  16568  wlkm  16592  wlkvtxiedg  16598  wlkvtxiedgg  16599  wlkeq  16607  wlk1walkdom  16612  uspgr2wlkeq  16618  uspgr2wlkeqi  16620  upgr2wlkdc  16630  wlkres  16632  trlreslem  16642  clwwlkccatlem  16653  clwwlkn1loopb  16673  clwwlkext2edg  16675  clwwlknonex2lem1  16690  clwwlknonex2  16692  trlsegvdeglem2  16714  trlsegvdeglem3  16715  eupth2lem3lem4fi  16726  eupth2lemsfi  16731  fnmptd  16844  bj-sels  16952  bj-nnelon  16997  pw1map  17037  pwle2  17040  pwf1oexmid  17041  pw1nct  17045  stnot  17051  nninfall  17064  nninfsellemdc  17065  nninfself  17068  nnnninfex  17077  nninfnfiinf  17078  refeq  17085  isomninnlem  17091  cvgcmp2nlemabs  17093  trilpolemlt1  17102  trirec0  17105  apdifflemf  17107  apdifflemr  17108  apdiff  17109  qdiff  17110  iswomninnlem  17111  iswomni0  17113  ismkvnnlem  17114  reap0  17120  cndcap  17121