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  4153  3brtr4d  4163  snelpwi  4353  prelpwi  4356  pwel  4360  ordelon  4530  onin  4533  elelsuc  4556  onsuc  4650  onsucb  4652  onintonm  4666  omsinds  4771  sosng  4850  relssdv  4869  eqbrrdv  4874  eqrelrdv2  4876  relsnopg  4881  breldmg  4989  elrnmptdv  5038  iss  5112  xpimasn  5239  elxp4  5278  elxp5  5279  iotam  5372  funssres  5423  f0rn0  5590  fimadmfo  5627  sefvex  5719  fdmeu  5749  fvun1  5772  eqfnfvd  5812  fvimacnvi  5826  fvimacnv  5827  fvelrn  5842  fmpt3d  5867  fmpt2d  5873  resflem  5875  fmptco  5877  fsn  5883  funopsn  5894  fncofn  5896  ftpg  5902  fconst2g  5933  funfvima3  5955  elabrexg  5967  foeqcnvco  5999  f1eqcocnv  6000  fliftfun  6005  fliftfund  6006  fliftval  6009  riota5f  6068  f1ofveu  6076  f1ocnvd  6295  f1opw2  6299  f1o3d  6301  off  6319  offval2  6322  ofrfval2  6323  offveq  6327  caofref  6331  caofinvl  6332  elxp6  6407  cnvf1olem  6464  f2ndf  6466  f1od2  6475  elmpom  6478  fvn0elsupp  6495  suppfnss  6501  tposf12  6544  smores2  6569  tfrlemisucaccv  6600  tfrlemibfn  6603  tfr1onlemsucaccv  6616  tfr1onlembfn  6619  tfrcllemsucaccv  6629  tfrcllembfn  6632  tfrcl  6639  tfri3  6642  frecabcl  6674  nnsucsssuc  6769  ersym  6823  ertr  6826  swoer  6839  erth  6857  riinerm  6886  qliftfund  6896  eroprf  6906  ecopoverg  6914  th3qlem1  6915  mapfoss  6951  elmapssres  6958  mapm  6974  mapss  6978  fdiagfn  6979  ixpssmap2g  7014  mapsnf1o  7024  f1oen4g  7043  f1dom4g  7044  f1dom2g  7047  dom3d  7065  en2prd  7111  dom1oi  7122  pw2f1odclem  7139  fopwdom  7141  mapxpen  7153  nndomo  7170  dif1en  7188  findcard2  7198  findcard2s  7199  diffisn  7202  fimax2gtrilemstep  7210  eqsndc  7215  fientri3  7227  tpfidceq  7242  fiintim  7243  opabfi  7252  f1dmvrnfibi  7263  sbthlemi6  7285  0fsupp  7304  elfir  7313  fifo  7320  ofrfidc  7324  2omap  7325  supelti  7349  supsnti  7352  cnvinfex  7365  ordiso2  7382  updjud  7429  djudom  7440  difinfsn  7447  ctssdc  7460  enumctlemm  7461  enumct  7462  nninfninc  7470  enomnilem  7485  fodjuf  7492  ismkvnex  7502  omnimkv  7503  enmkvlem  7508  enwomnilem  7516  nninfdcinf  7518  nninfwlporlem  7520  isnumi  7534  exmidfodomrlemrALT  7562  finacn  7567  djudoml  7582  djudomr  7583  netap  7627  2omotaplemap  7630  2omotaplemst  7631  exmidapne  7633  cc2lem  7639  cc3  7641  ltsopi  7694  pitri3or  7696  ltdcpi  7697  indpi  7716  enqdc  7735  enqdc1  7736  addcmpblnq  7741  mulcanenq  7759  recrecnq  7768  nqtri3or  7770  ltdcnq  7771  ltsonq  7772  ltaddnq  7781  subhalfnqq  7788  archnqq  7791  prarloclemarch2  7793  enq0tr  7808  nqnq0  7815  addcmpblnq0  7817  mulcanenq0ec  7819  nnnq0lem1  7820  nqpnq0nq  7827  nq0m0r  7830  nq02m  7839  prarloclemlt  7867  prarloclemcalc  7876  addlocpr  7910  nqprl  7925  nqpru  7926  addnqprlemrl  7931  addnqprlemru  7932  prmuloclemcalc  7939  mullocprlem  7944  mulnqprlemrl  7947  mulnqprlemru  7948  1idprl  7964  1idpru  7965  ltaddpr  7971  ltexprlemm  7974  ltexprlemopl  7975  ltexprlemopu  7977  ltexprlemdisj  7980  ltexprlemrl  7984  ltexprlemru  7986  addcanprleml  7988  addcanprlemu  7989  addcanprg  7990  prplnqu  7994  recexprlemloc  8005  recexprlem1ssl  8007  recexprlem1ssu  8008  aptiprleml  8013  aptiprlemu  8014  archpr  8017  cauappcvgprlemm  8019  cauappcvgprlemopl  8020  cauappcvgprlemloc  8026  cauappcvgprlemladdfu  8028  cauappcvgprlemladdfl  8029  cauappcvgprlem1  8033  cauappcvgprlem2  8034  caucvgprlemnkj  8040  caucvgprlemopl  8043  caucvgprlemloc  8049  caucvgprlemladdfu  8051  caucvgprlem2  8054  caucvgprprlemnkltj  8063  caucvgprprlemopl  8071  caucvgprprlemloc  8077  caucvgprprlemexbt  8080  caucvgprprlemaddq  8082  caucvgprprlem2  8084  suplocexprlemmu  8092  suplocexprlemru  8093  suplocexprlemloc  8095  suplocexprlemlub  8098  prsrlem1  8116  0idsr  8141  1idsr  8142  recexgt0sr  8147  archsr  8156  prsradd  8160  caucvgsrlemcau  8167  caucvgsrlembound  8168  caucvgsrlemoffgt1  8173  suplocsrlemb  8180  suplocsrlempr  8181  suplocsrlem  8182  pitonnlem1p1  8220  pitonn  8222  pitoregt0  8223  peano2nnnn  8227  recidpirq  8232  axcaucvglemval  8271  leid  8416  nltled  8455  readdcan  8474  addneintrd  8522  addneintr2d  8523  pncan  8540  subsub2  8562  subsub4  8567  negned  8642  subne0d  8654  subneintrd  8689  subneintr2d  8691  subeq0bd  8714  subdi  8720  gt0add  8910  rimul  8922  rereim  8923  ltmul1a  8928  apreim  8940  apirr  8942  mulap0r  8952  msqge0  8953  mulge0  8956  gt0ap0  8963  ltap  8970  subap0d  8981  recexaplem2  8989  mulap0bad  8996  mulap0bbd  8997  mul0eqap  9009  divrecap  9027  div0ap  9041  div1  9042  recrecap  9048  divdivdivap  9052  ddcanap  9065  rerecclap  9069  div2negap  9074  diveqap1bd  9175  recgt0  9189  prodgt0  9191  lemul1a  9197  recp1lt1  9238  squeeze0  9243  peano2nn  9326  div4p1lem1div2  9571  arch  9572  peano2z  9692  peano2zm  9694  ztri3or  9699  nn0n0n1ge2  9727  zextle  9749  gtndiv  9753  suprzclex  9756  nn0ind-raph  9775  uzid  9953  uzneg  9958  uztric  9961  uz11  9962  eluzp1l  9964  qdivcl  10060  irrmul  10065  irrmulap  10066  rpnegap  10105  negelrpd  10107  ledivge1le  10145  mul2lt0rlt0  10178  mul2lt0rgt0  10179  nn0ledivnn  10186  ltpnf  10200  mnflt  10203  pnfge  10209  mnfle  10212  xrlttr  10215  xrltso  10216  xrlttri3  10217  xrleid  10220  xaddass2  10290  xltadd1  10296  xlt2add  10300  xleaddadd  10307  lincmble  10424  iccf1o  10425  fztri3or  10461  fznlem  10463  fzn  10464  fzsplit2  10473  fzsplit3  10476  fznatpl1  10501  uzsplit  10517  fseq1p1m1  10519  fzm1  10525  fznn0sub2  10553  difelfznle  10560  1fv  10564  fzodcel  10578  fzospliti  10603  fzouzsplit  10606  eluzgtdifelfzo  10633  exfzdc  10677  subfzo0  10679  zsupcllemstep  10680  zsupcl  10682  zssinfcl  10683  infssuzex  10684  infssuzcldc  10686  infssfzcldc  10687  infssfzledc  10688  suprzubdc  10689  nninfdcex  10690  qdcle  10699  exbtwnz  10703  qbtwnrelemcalc  10708  flqlelt  10730  flaplelt  10731  qfraclt1  10735  qfracge0  10736  flaplt  10740  flqltnz  10744  btwnzge0  10757  flhalf  10759  fldiv4lem1div2uz2  10763  ceiqle  10772  intfracq  10779  mulqmod0  10789  modqge0  10791  modqlt  10792  modqid  10808  modqid0  10809  m1modge3gt1  10830  modqltm1p1mod  10835  q2txmodxeq0  10843  modaddmodlo  10847  modsumfzodifsn  10855  addmodlteq  10857  frecuzrdgtcl  10871  frecuzrdgtclt  10880  uzennn  10895  uzsinds  10903  seqf  10923  seqf2  10927  monoord2  10945  iseqf1olemqk  10966  iseqf1olemjpcl  10967  iseqf1olemqpcl  10968  seq3f1olemqsumkj  10970  seq3f1olemqsum  10972  seq3f1olemstep  10973  seq3f1oleml  10975  seqf1oglem1  10978  ser3le  10996  exp3vallem  10999  exp3val  11000  expp1  11005  expcllem  11009  ltexp2a  11050  leexp2a  11051  resq01  11117  nn0ltexp2  11170  faclbnd  11202  faclbnd2  11203  faclbnd3  11204  bcval5  11224  bcpasc  11227  bcm1n  11230  hashennn  11242  fihasheqf1oi  11249  hashsng  11260  fihashfn  11263  hashun  11268  fihashss  11280  fihashssdif  11282  hashfz  11285  hashxp  11290  hashmap  11291  hashpwfi  11292  fimaxq  11293  sseqn  11302  hashfibclem  11305  hashf1lem2  11309  hashf1  11310  zfz1isolem1  11315  seq3coll  11317  hashdmprop2dom  11319  wrdf  11333  wrdlenge2n0  11363  fstwrdne0  11367  wrdred1hash  11371  ccatvalfn  11392  ccatsymb  11393  ccatlid  11397  ccatrid  11398  ccatrn  11400  ccatalpha  11404  eqs1  11419  ccats1val2  11431  fzowrddc  11442  swrdlen  11447  swrdnd  11454  swrd0g  11455  swrdfv2  11458  swrdwrdsymbg  11459  pfxn0  11483  pfxwrdsymbg  11485  pfxsuff1eqwrdeq  11494  swrdswrd  11500  ccats1pfxeq  11509  ccats1pfxeqrex  11510  wrdind  11517  wrd2ind  11518  swrdccatin1  11520  pfxccatin12lem4  11521  swrdccatin2  11524  pfxccatin12  11528  pfxccat3a  11533  swrdccat3blem  11534  pfxccatid  11536  swrdccatin2d  11539  shftfn  11612  cjth  11634  cjmulrcl  11675  sq01  11683  reim0bd  11733  rerebd  11734  cjrebd  11735  caucvgre  11770  cvg1nlemcxze  11771  cvg1nlemcau  11773  cvg1nlemres  11774  recvguniq  11784  resqrexlemover  11799  resqrexlemdec  11800  resqrexlemgt0  11809  resqrexlemoverl  11810  resqrexlemglsq  11811  rersqrtthlem  11819  sqrtgt0  11823  leabs  11863  absexpzap  11870  absle  11879  recvalap  11887  abstri  11894  abs2dif  11896  amgm2  11908  absne0d  11977  maxleim  11995  maxabslemab  11996  maxabslemlub  11997  maxltsup  12008  zmaxcl  12014  fimaxre2  12017  minmax  12021  rpmincl  12029  zmincl  12030  bdtrilem  12031  bdtri  12032  xrmaxleim  12036  xrmaxiflemcom  12041  xrmaxltsup  12050  xrmaxadd  12053  xrminmax  12057  xrminrpcl  12066  climconst  12082  climuni  12085  2clim  12093  climcn1  12100  climcn2  12101  reccn2ap  12105  climge0  12117  climle  12126  climsqz  12127  climsqz2  12128  serf0  12144  summodclem3  12173  summodclem2a  12174  fsumcl2lem  12191  sumpr  12206  sumtp  12207  fsum0diaglem  12233  mptfzshft  12235  fsumle  12256  fsumlt  12257  divcnv  12290  trireciplem  12293  expcnvap0  12295  expcnv  12297  explecnv  12298  geosergap  12299  cvgratnnlembern  12316  cvgratnnlemabsle  12320  cvgratnnlemsumlt  12321  cvgratz  12325  cvgratgt0  12326  mertenslemi1  12328  mertenslem2  12329  mertensabs  12330  clim2divap  12333  prodmodclem3  12368  prodmodclem2a  12369  fprodseq  12376  fprodmul  12384  fprodfac  12408  fprodconst  12413  fprodap0  12414  fprodap0f  12429  fprodle  12433  eftcl  12447  ef0lem  12453  efsub  12474  eftlub  12483  eflegeo  12494  tanval2ap  12506  sinadd  12529  cos2t  12543  cos2tsin  12544  sin01bnd  12550  cos01bnd  12551  eirraplem  12570  dvdsval2  12583  dvdsdc  12591  dvds0lem  12594  zdvdsdc  12605  dvdscmulr  12613  dvdsmulcr  12614  fsumdvds  12635  dvdslelemd  12636  divconjdvds  12642  dvdsext  12648  fzm1ndvds  12649  dvdsmod  12655  3dvds  12657  oexpneg  12670  2tp1odd  12677  mulsucdiv2z  12678  2teven  12680  zeo5  12681  opeo  12690  omeo  12691  nn0ob  12701  divalglemnqt  12713  bitsdc  12740  bits0o  12743  bitsfzolem  12747  bitsfzo  12748  bitsmod  12749  bitscmp  12751  bitsinv1lem  12754  gcddvds  12766  dvdslegcd  12767  gcdneg  12785  bezoutlemnewy  12799  bezoutlemstep  12800  bezoutlema  12802  bezoutlemb  12803  bezoutlemmo  12809  bezoutlemle  12811  bezoutlemsup  12812  dfgcd3  12813  bezout  12814  dfgcd2  12817  uzwodc  12840  lcmcllem  12871  lcmneg  12878  lcmgcdlem  12881  lcmdvds  12883  lcmid  12884  3lcm2e6woprm  12890  6lcm4e12  12891  ncoprmgcdne1b  12893  mulgcddvds  12898  divgcdcoprmex  12906  cncongr1  12907  cncongr2  12908  isprm2lem  12920  prmind2  12924  dvdsnprmd  12929  prm2orodd  12930  sqnprm  12941  isprm5lem  12946  rpexp  12958  sqrt2irrlem  12966  nnmaxpwlemparts  12978  sqrt2irraplemnn  12985  qnumdencoprm  12999  qeqnumdivden  13000  nn0gcdsq  13006  nn0sqrtelqelz  13012  nonsq  13013  sqrtrirr  13015  phicl2  13022  phibnd  13025  hashdvds  13029  phiprmpw  13030  phimullem  13033  eulerthlemrprm  13037  eulerthlema  13038  eulerthlemth  13040  prmdiveq  13044  hashgcdlem  13046  odzdvds  13054  modprminv  13058  nnnn0modprm0  13064  modprmn0modprm0  13065  pythagtriplem10  13078  pythagtriplem19  13091  pythagtrip  13092  pcpre1  13101  pcpremul  13102  pceu  13104  pcmul  13110  pcdiv  13111  pcqmul  13112  pcqdiv  13116  pcexp  13118  pcdvdsb  13129  pcidlem  13132  pcdvdstr  13136  pcgcd1  13137  pc2dvds  13139  pcprmpw2  13142  difsqpwdvds  13147  pcaddlem  13148  pcadd  13149  pcadd2  13150  pcmpt  13152  pcmptdvds  13154  pcprod  13155  fldivp1  13157  pcfaclem  13158  pcfac  13159  pcbc  13160  qexpz  13161  pockthlem  13165  pockthg  13166  1arithlem4  13175  1arith  13176  1arith2  13177  4sqlem6  13192  4sqlem8  13194  4sqlem9  13195  4sqlem10  13196  4sqexercise1  13207  4sqexercise2  13208  4sqlemsdc  13209  4sqlem11  13210  4sqlem12  13211  4sqlem15  13214  4sqlem16  13215  4sqlem17  13216  ballotfilemfc0  13291  ballotfilemfcc  13292  ballotfilemimin  13308  ballotfilem1c  13310  ballotfilemro  13325  ballotfilemfrcn0  13332  znnen  13348  ennnfonelemk  13350  ennnfonelemkh  13362  ennnfonelemhf1o  13363  ennnfonelemrnh  13366  ennnfonelemfun  13367  ennnfonelemf1  13368  ennnfonelemrn  13369  ennnfonelemnn0  13372  ctinfomlemom  13377  ctiunctlemudc  13387  unct  13392  omctfn  13393  ssnnctlemct  13396  nninfdclemp1  13400  nninfdc  13403  structfung  13428  setsfun  13446  setsfun0  13447  setscom  13451  strslfv3  13457  setsslid  13462  imasaddfnlemg  13695  imasaddvallemg  13696  mgmsscl  13741  plusffng  13745  mgmplusf  13746  mgm0  13749  mgm1  13750  opifismgmdc  13751  gzsumfzval  13771  sgrp1  13786  issgrpd  13787  mndpfo  13811  mndfo  13812  mnd1  13822  0subm  13851  mhmima  13858  grpinvfng  13909  isgrpinv  13919  grpinvid  13925  grpinvf1o  13935  grpinvadd  13943  grpsubf  13944  grpsubsub4  13958  grplactcnv  13967  grp1  13971  grp1inv  13972  qusgrp2  13976  mulgfng  13987  subginv  14044  resgrpisgrp  14058  subgintm  14061  0subg  14062  0nsg  14077  qusinv  14099  ghminv  14113  ghmrn  14120  ghmeql  14130  ghmnsgima  14131  kerf1ghm  14137  conjnmz  14142  cntzval  14154  cntz2ss  14169  cntzsubg  14172  cntzmhm  14174  cntzmhm2  14175  gzsumshift  14240  gsumvalfi  14243  gzsumgsum  14246  gsumsncmn  14247  gsump1  14248  gsumf1ofi  14251  gsumsubmclfi  14254  gsummptfidmsplit  14255  idjusnfi  14271  prdsplusgsgrpcl  14298  prdsplusgcl  14300  prdsidlem  14301  prdsinvlem  14304  prdsinvgd  14306  pwsdiagel  14318  pwssnf1o  14319  rngass  14346  rngmneg1  14354  rngmneg2  14355  qusrng  14365  srgideu  14384  srgidmlem  14390  srgpcomp  14402  srg1expzeq1  14407  ringcl  14425  ringideu  14429  ringidmlem  14435  ringnegl  14464  ringnegr  14465  ring1  14472  qusring2  14481  opprringbg  14495  dvdsrd  14511  dvdsr01  14521  isunitd  14523  unitinvcl  14540  unitinvinv  14541  unitnegcl  14547  rhmmul  14581  rhmf1o  14585  nzrunit  14605  lringuplu  14613  subrngintm  14630  subrgsubm  14652  subrgintm  14661  rrgsupp  14684  ringunitap  14703  aprsym  14706  aprnzr  14709  aprlring  14710  drnglring  14717  drngunitap  14718  scaffng  14756  lmodscaf  14757  lsssn0  14817  lss1d  14830  lssintclm  14831  lspval  14837  lspcl  14838  lspsnid  14854  lspprid1  14858  lspsn  14863  sraval  14884  rspcl  14938  rspssid  14939  rspssp  14941  rnglidlmmgm  14943  rnglidlmsgrp  14944  cnfldneg  15020  zringinvg  15049  expghmap  15052  znzrhfo  15093  znf1o  15096  znhash  15101  znidomb  15103  znrrg  15105  psrbagfsupp  15167  psrbagfi  15168  psrbagdceq  15169  snifpsrbagfi  15170  psrbaglecl  15174  psrbagaddclfi  15175  psrbagcon  15176  psrbaglefifi  15177  psraddcl  15189  psrmulclfilem  15194  psr0cl  15196  psrnegcl  15198  psrneg  15202  psr1clfi  15203  psrlidmfi  15204  psrridmfi  15205  mvrffi  15214  mplsubgfilemm  15226  mplsubgfilemcl  15227  baspartn  15288  eltg3i  15294  tgclb  15303  topbas  15305  2basgeng  15320  topcld  15347  0cld  15350  uncld  15351  neif  15379  elnei  15390  0nei  15404  restbasg  15406  iscnp4  15456  cnpnei  15457  cnclima  15461  cncnp  15468  cnrest2r  15475  cndis  15479  lmff  15487  lmtopcnp  15488  txbas  15496  txopn  15503  txcnp  15509  upxp  15510  txdis1cn  15516  cnmpt11  15521  cnmpt21  15529  psmetge0  15569  xmetge0  15603  xmettpos  15608  xmetrtri  15614  metrtri  15615  xblpnfps  15636  xblpnf  15637  blfps  15647  blf  15648  ssblps  15663  ssbl  15664  blbas  15671  metss2  15736  xmettxlem  15747  xmettx  15748  qtopbas  15760  divcnap  15803  cncfss  15821  cdivcncfap  15842  expcncf  15847  cnopnap  15849  maxcncf  15853  mincncf  15854  dedekindeulemuub  15855  dedekindeulemlu  15859  dedekindeu  15861  suplociccex  15863  dedekindicclemuub  15864  dedekindicclemlu  15868  dedekindicclemicc  15870  ivthinclemlopn  15874  ivthinclemuopn  15876  ivthinc  15881  ivthreinc  15883  hoverlt1  15887  ellimc3apf  15898  limcimolemlt  15902  limcimo  15903  limcresi  15904  cnplimclemle  15906  reldvg  15917  dvfgg  15926  dvidlemap  15929  dvidrelem  15930  dvidsslem  15931  dvcjbr  15946  dvcj  15947  dvrecap  15951  dveflem  15964  dvef  15965  elply2  15973  elplyr  15978  plycj  15999  plyreres  16002  reeff1oleme  16010  efap1p  16017  pilem3  16022  sinq34lt0t  16070  cosq14gt0  16071  coseq0q4123  16073  tangtx  16077  sincosq1eq  16078  cosordlem  16089  logdivlti  16123  logdivlt  16136  relogbval  16199  relogbzcl  16200  nnlogbexp  16207  logbgcd1irr  16215  logbgcd1irraplemexp  16216  logbgcd1irraplemap  16217  zprmlogbaplem2  16228  zprmlogbap  16230  birthdaylem2  16238  birthdaylem3  16239  pellexlem1  16241  pellexlem3  16243  wilthlem1  16244  efchtqdvds  16277  ppiqwordi  16280  ppiqeq0  16292  mpodvdsmulf1o  16296  ppiqub  16305  chtqleppi  16306  chtublem  16307  chtqub  16308  mersenne  16309  perfectlem2  16312  perfect  16313  bcmono  16316  bcmax  16317  bposlem1  16323  bposlem2  16324  bposlem3  16325  bposlem6  16328  bposlem7  16329  bposlem9  16331  zabsle1  16335  lgslem1  16336  lgsval  16340  lgsfvalg  16341  lgsfcl2  16342  lgsval2lem  16346  lgscl1  16359  lgsmod  16362  lgsdir2lem5  16368  lgsdir2  16369  lgsdilem2  16372  lgsdi  16373  lgsne0  16374  gausslemma2dlem0c  16387  gausslemma2dlem0h  16392  gausslemma2dlem1a  16394  gausslemma2dlem1f1o  16396  gausslemma2dlem3  16399  lgseisenlem1  16406  lgseisenlem2  16407  lgseisenlem3  16408  lgseisenlem4  16409  lgseisen  16410  lgsquadlem1  16413  lgsquadlem2  16414  lgsquadlem3  16415  lgsquad3  16420  2lgslem3b1  16434  2lgslem3c1  16435  2lgs  16440  2lgsoddprmlem2  16442  2lgsoddprm  16449  2sqlem3  16453  2sqlem8  16459  2sqlem10  16461  structgrssvtx  16500  structgrssiedg  16501  ushgruhgr  16538  uhgrun  16544  incistruhgr  16548  upgrop  16562  upgruhgr  16569  umgrupgr  16570  umgrnloopv  16572  umgredgprv  16573  umgr0e  16576  upgr1edc  16579  umgr1een  16583  upgrun  16584  umgrun  16586  umgrislfupgrdom  16589  upgredg  16602  umgrpredgv  16605  usgrop  16624  usgrausgrien  16627  ausgrumgrien  16628  ausgrusgrien  16629  uspgrupgrushgr  16640  usgrumgr  16642  usgrumgruspgr  16643  usgruspgrben  16644  usgrislfuspgrdom  16648  edgssv2en  16657  usgrf1oedg  16663  usgredg4  16673  usgredg2vlem2  16681  usgredg2v  16682  ushgredgedg  16684  ushgredgedgloop  16686  usgrstrrepeen  16689  usgr0e  16690  uhgr0v0e  16692  uspgr1edc  16698  usgr1e  16699  griedg0ssusgr  16709  subgrprop3  16720  subgruhgredgdm  16728  subuhgr  16730  subupgr  16731  subumgr  16732  subusgr  16733  uhgrspansubgrlem  16734  1loopgrvd2fi  16763  1loopgrvd0fi  16764  1hevtxdg0fi  16765  vdegp1aid  16772  vdegp1bid  16773  wlkm  16797  wlkvtxiedg  16803  wlkvtxiedgg  16804  wlkeq  16812  wlk1walkdom  16817  uspgr2wlkeq  16823  uspgr2wlkeqi  16825  upgr2wlkdc  16835  wlkres  16837  trlreslem  16847  clwwlkccatlem  16858  clwwlkn1loopb  16878  clwwlkext2edg  16880  clwwlknonex2lem1  16895  clwwlknonex2  16897  trlsegvdeglem2  16919  trlsegvdeglem3  16920  eupth2lem3lem4fi  16931  eupth2lemsfi  16936  fnmptd  17049  bj-sels  17157  bj-nnelon  17202  pw1map  17242  pwle2  17245  pwf1oexmid  17246  pw1nct  17250  stnot  17256  nninfall  17270  nninfsellemdc  17271  nninfself  17274  nnnninfex  17283  nninfnfiinf  17284  refeq  17291  isomninnlem  17297  cvgcmp2nlemabs  17299  trilpolemlt1  17309  trirec0  17312  apdifflemf  17314  apdifflemr  17315  apdiff  17316  qdiff  17317  iswomninnlem  17318  iswomni0  17320  ismkvnnlem  17321  reap0  17327  cndcap  17328