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 )

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  mapss  6977  fdiagfn  6978  ixpssmap2g  7013  mapsnf1o  7023  f1oen4g  7042  f1dom4g  7043  f1dom2g  7046  dom3d  7064  en2prd  7110  dom1oi  7121  pw2f1odclem  7138  fopwdom  7140  mapxpen  7152  nndomo  7169  dif1en  7187  findcard2  7197  findcard2s  7198  diffisn  7201  fimax2gtrilemstep  7209  eqsndc  7214  fientri3  7226  tpfidceq  7241  fiintim  7242  opabfi  7251  f1dmvrnfibi  7262  sbthlemi6  7284  0fsupp  7303  elfir  7312  fifo  7319  ofrfidc  7323  2omap  7324  supelti  7348  supsnti  7351  cnvinfex  7364  ordiso2  7381  updjud  7428  djudom  7439  difinfsn  7446  ctssdc  7459  enumctlemm  7460  enumct  7461  nninfninc  7469  enomnilem  7484  fodjuf  7491  ismkvnex  7501  omnimkv  7502  enmkvlem  7507  enwomnilem  7515  nninfdcinf  7517  nninfwlporlem  7519  isnumi  7533  exmidfodomrlemrALT  7561  finacn  7566  djudoml  7581  djudomr  7582  netap  7626  2omotaplemap  7629  2omotaplemst  7630  exmidapne  7632  cc2lem  7638  cc3  7640  ltsopi  7693  pitri3or  7695  ltdcpi  7696  indpi  7715  enqdc  7734  enqdc1  7735  addcmpblnq  7740  mulcanenq  7758  recrecnq  7767  nqtri3or  7769  ltdcnq  7770  ltsonq  7771  ltaddnq  7780  subhalfnqq  7787  archnqq  7790  prarloclemarch2  7792  enq0tr  7807  nqnq0  7814  addcmpblnq0  7816  mulcanenq0ec  7818  nnnq0lem1  7819  nqpnq0nq  7826  nq0m0r  7829  nq02m  7838  prarloclemlt  7866  prarloclemcalc  7875  addlocpr  7909  nqprl  7924  nqpru  7925  addnqprlemrl  7930  addnqprlemru  7931  prmuloclemcalc  7938  mullocprlem  7943  mulnqprlemrl  7946  mulnqprlemru  7947  1idprl  7963  1idpru  7964  ltaddpr  7970  ltexprlemm  7973  ltexprlemopl  7974  ltexprlemopu  7976  ltexprlemdisj  7979  ltexprlemrl  7983  ltexprlemru  7985  addcanprleml  7987  addcanprlemu  7988  addcanprg  7989  prplnqu  7993  recexprlemloc  8004  recexprlem1ssl  8006  recexprlem1ssu  8007  aptiprleml  8012  aptiprlemu  8013  archpr  8016  cauappcvgprlemm  8018  cauappcvgprlemopl  8019  cauappcvgprlemloc  8025  cauappcvgprlemladdfu  8027  cauappcvgprlemladdfl  8028  cauappcvgprlem1  8032  cauappcvgprlem2  8033  caucvgprlemnkj  8039  caucvgprlemopl  8042  caucvgprlemloc  8048  caucvgprlemladdfu  8050  caucvgprlem2  8053  caucvgprprlemnkltj  8062  caucvgprprlemopl  8070  caucvgprprlemloc  8076  caucvgprprlemexbt  8079  caucvgprprlemaddq  8081  caucvgprprlem2  8083  suplocexprlemmu  8091  suplocexprlemru  8092  suplocexprlemloc  8094  suplocexprlemlub  8097  prsrlem1  8115  0idsr  8140  1idsr  8141  recexgt0sr  8146  archsr  8155  prsradd  8159  caucvgsrlemcau  8166  caucvgsrlembound  8167  caucvgsrlemoffgt1  8172  suplocsrlemb  8179  suplocsrlempr  8180  suplocsrlem  8181  pitonnlem1p1  8219  pitonn  8221  pitoregt0  8222  peano2nnnn  8226  recidpirq  8231  axcaucvglemval  8270  leid  8415  nltled  8454  readdcan  8473  addneintrd  8521  addneintr2d  8522  pncan  8539  subsub2  8561  subsub4  8566  negned  8641  subne0d  8653  subneintrd  8688  subneintr2d  8690  subeq0bd  8713  subdi  8719  gt0add  8909  rimul  8921  rereim  8922  ltmul1a  8927  apreim  8939  apirr  8941  mulap0r  8951  msqge0  8952  mulge0  8955  gt0ap0  8962  ltap  8969  subap0d  8980  recexaplem2  8988  mulap0bad  8995  mulap0bbd  8996  mul0eqap  9008  divrecap  9026  div0ap  9040  div1  9041  recrecap  9047  divdivdivap  9051  ddcanap  9064  rerecclap  9068  div2negap  9073  diveqap1bd  9174  recgt0  9188  prodgt0  9190  lemul1a  9196  recp1lt1  9237  squeeze0  9242  peano2nn  9325  div4p1lem1div2  9570  arch  9571  peano2z  9691  peano2zm  9693  ztri3or  9698  nn0n0n1ge2  9726  zextle  9748  gtndiv  9752  suprzclex  9755  nn0ind-raph  9774  uzid  9952  uzneg  9957  uztric  9960  uz11  9961  eluzp1l  9963  qdivcl  10059  irrmul  10064  irrmulap  10065  rpnegap  10104  negelrpd  10106  ledivge1le  10144  mul2lt0rlt0  10177  mul2lt0rgt0  10178  nn0ledivnn  10185  ltpnf  10199  mnflt  10202  pnfge  10208  mnfle  10211  xrlttr  10214  xrltso  10215  xrlttri3  10216  xrleid  10219  xaddass2  10289  xltadd1  10295  xlt2add  10299  xleaddadd  10306  lincmble  10423  iccf1o  10424  fztri3or  10460  fznlem  10462  fzn  10463  fzsplit2  10472  fzsplit3  10475  fznatpl1  10500  uzsplit  10516  fseq1p1m1  10518  fzm1  10524  fznn0sub2  10552  difelfznle  10559  1fv  10563  fzodcel  10577  fzospliti  10602  fzouzsplit  10605  eluzgtdifelfzo  10632  exfzdc  10676  subfzo0  10678  zsupcllemstep  10679  zsupcl  10681  zssinfcl  10682  infssuzex  10683  infssuzcldc  10685  infssfzcldc  10686  infssfzledc  10687  suprzubdc  10688  nninfdcex  10689  qdcle  10698  exbtwnz  10702  qbtwnrelemcalc  10707  flqlelt  10729  flaplelt  10730  qfraclt1  10734  qfracge0  10735  flaplt  10739  flqltnz  10743  btwnzge0  10756  flhalf  10758  fldiv4lem1div2uz2  10762  ceiqle  10771  intfracq  10778  mulqmod0  10788  modqge0  10790  modqlt  10791  modqid  10807  modqid0  10808  m1modge3gt1  10829  modqltm1p1mod  10834  q2txmodxeq0  10842  modaddmodlo  10846  modsumfzodifsn  10854  addmodlteq  10856  frecuzrdgtcl  10870  frecuzrdgtclt  10879  uzennn  10894  uzsinds  10902  seqf  10922  seqf2  10926  monoord2  10944  iseqf1olemqk  10965  iseqf1olemjpcl  10966  iseqf1olemqpcl  10967  seq3f1olemqsumkj  10969  seq3f1olemqsum  10971  seq3f1olemstep  10972  seq3f1oleml  10974  seqf1oglem1  10977  ser3le  10995  exp3vallem  10998  exp3val  10999  expp1  11004  expcllem  11008  ltexp2a  11049  leexp2a  11050  resq01  11116  nn0ltexp2  11169  faclbnd  11201  faclbnd2  11202  faclbnd3  11203  bcval5  11223  bcpasc  11226  bcm1n  11229  hashennn  11241  fihasheqf1oi  11248  hashsng  11259  fihashfn  11262  hashun  11267  fihashss  11279  fihashssdif  11281  hashfz  11284  hashxp  11289  hashmap  11290  hashpwfi  11291  fimaxq  11292  sseqn  11301  hashfibclem  11304  hashf1lem2  11308  hashf1  11309  zfz1isolem1  11314  seq3coll  11316  hashdmprop2dom  11318  wrdf  11332  wrdlenge2n0  11362  fstwrdne0  11366  wrdred1hash  11370  ccatvalfn  11391  ccatsymb  11392  ccatlid  11396  ccatrid  11397  ccatrn  11399  ccatalpha  11403  eqs1  11418  ccats1val2  11430  fzowrddc  11441  swrdlen  11446  swrdnd  11453  swrd0g  11454  swrdfv2  11457  swrdwrdsymbg  11458  pfxn0  11482  pfxwrdsymbg  11484  pfxsuff1eqwrdeq  11493  swrdswrd  11499  ccats1pfxeq  11508  ccats1pfxeqrex  11509  wrdind  11516  wrd2ind  11517  swrdccatin1  11519  pfxccatin12lem4  11520  swrdccatin2  11523  pfxccatin12  11527  pfxccat3a  11532  swrdccat3blem  11533  pfxccatid  11535  swrdccatin2d  11538  shftfn  11611  cjth  11633  cjmulrcl  11674  sq01  11682  reim0bd  11732  rerebd  11733  cjrebd  11734  caucvgre  11769  cvg1nlemcxze  11770  cvg1nlemcau  11772  cvg1nlemres  11773  recvguniq  11783  resqrexlemover  11798  resqrexlemdec  11799  resqrexlemgt0  11808  resqrexlemoverl  11809  resqrexlemglsq  11810  rersqrtthlem  11818  sqrtgt0  11822  leabs  11862  absexpzap  11869  absle  11878  recvalap  11886  abstri  11893  abs2dif  11895  amgm2  11907  absne0d  11976  maxleim  11994  maxabslemab  11995  maxabslemlub  11996  maxltsup  12007  zmaxcl  12013  fimaxre2  12016  minmax  12020  rpmincl  12028  zmincl  12029  bdtrilem  12030  bdtri  12031  xrmaxleim  12035  xrmaxiflemcom  12040  xrmaxltsup  12049  xrmaxadd  12052  xrminmax  12056  xrminrpcl  12065  climconst  12081  climuni  12084  2clim  12092  climcn1  12099  climcn2  12100  reccn2ap  12104  climge0  12116  climle  12125  climsqz  12126  climsqz2  12127  serf0  12143  summodclem3  12172  summodclem2a  12173  fsumcl2lem  12190  sumpr  12205  sumtp  12206  fsum0diaglem  12232  mptfzshft  12234  fsumle  12255  fsumlt  12256  divcnv  12289  trireciplem  12292  expcnvap0  12294  expcnv  12296  explecnv  12297  geosergap  12298  cvgratnnlembern  12315  cvgratnnlemabsle  12319  cvgratnnlemsumlt  12320  cvgratz  12324  cvgratgt0  12325  mertenslemi1  12327  mertenslem2  12328  mertensabs  12329  clim2divap  12332  prodmodclem3  12367  prodmodclem2a  12368  fprodseq  12375  fprodmul  12383  fprodfac  12407  fprodconst  12412  fprodap0  12413  fprodap0f  12428  fprodle  12432  eftcl  12446  ef0lem  12452  efsub  12473  eftlub  12482  eflegeo  12493  tanval2ap  12505  sinadd  12528  cos2t  12542  cos2tsin  12543  sin01bnd  12549  cos01bnd  12550  eirraplem  12569  dvdsval2  12582  dvdsdc  12590  dvds0lem  12593  zdvdsdc  12604  dvdscmulr  12612  dvdsmulcr  12613  fsumdvds  12634  dvdslelemd  12635  divconjdvds  12641  dvdsext  12647  fzm1ndvds  12648  dvdsmod  12654  3dvds  12656  oexpneg  12669  2tp1odd  12676  mulsucdiv2z  12677  2teven  12679  zeo5  12680  opeo  12689  omeo  12690  nn0ob  12700  divalglemnqt  12712  bitsdc  12739  bits0o  12742  bitsfzolem  12746  bitsfzo  12747  bitsmod  12748  bitscmp  12750  bitsinv1lem  12753  gcddvds  12765  dvdslegcd  12766  gcdneg  12784  bezoutlemnewy  12798  bezoutlemstep  12799  bezoutlema  12801  bezoutlemb  12802  bezoutlemmo  12808  bezoutlemle  12810  bezoutlemsup  12811  dfgcd3  12812  bezout  12813  dfgcd2  12816  uzwodc  12839  lcmcllem  12870  lcmneg  12877  lcmgcdlem  12880  lcmdvds  12882  lcmid  12883  3lcm2e6woprm  12889  6lcm4e12  12890  ncoprmgcdne1b  12892  mulgcddvds  12897  divgcdcoprmex  12905  cncongr1  12906  cncongr2  12907  isprm2lem  12919  prmind2  12923  dvdsnprmd  12928  prm2orodd  12929  sqnprm  12940  isprm5lem  12945  rpexp  12957  sqrt2irrlem  12965  nnmaxpwlemparts  12977  sqrt2irraplemnn  12984  qnumdencoprm  12998  qeqnumdivden  12999  nn0gcdsq  13005  nn0sqrtelqelz  13011  nonsq  13012  sqrtrirr  13014  phicl2  13021  phibnd  13024  hashdvds  13028  phiprmpw  13029  phimullem  13032  eulerthlemrprm  13036  eulerthlema  13037  eulerthlemth  13039  prmdiveq  13043  hashgcdlem  13045  odzdvds  13053  modprminv  13057  nnnn0modprm0  13063  modprmn0modprm0  13064  pythagtriplem10  13077  pythagtriplem19  13090  pythagtrip  13091  pcpre1  13100  pcpremul  13101  pceu  13103  pcmul  13109  pcdiv  13110  pcqmul  13111  pcqdiv  13115  pcexp  13117  pcdvdsb  13128  pcidlem  13131  pcdvdstr  13135  pcgcd1  13136  pc2dvds  13138  pcprmpw2  13141  difsqpwdvds  13146  pcaddlem  13147  pcadd  13148  pcadd2  13149  pcmpt  13151  pcmptdvds  13153  pcprod  13154  fldivp1  13156  pcfaclem  13157  pcfac  13158  pcbc  13159  qexpz  13160  pockthlem  13164  pockthg  13165  1arithlem4  13174  1arith  13175  1arith2  13176  4sqlem6  13191  4sqlem8  13193  4sqlem9  13194  4sqlem10  13195  4sqexercise1  13206  4sqexercise2  13207  4sqlemsdc  13208  4sqlem11  13209  4sqlem12  13210  4sqlem15  13213  4sqlem16  13214  4sqlem17  13215  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemimin  13307  ballotfilem1c  13309  ballotfilemro  13324  ballotfilemfrcn0  13331  znnen  13347  ennnfonelemk  13349  ennnfonelemkh  13361  ennnfonelemhf1o  13362  ennnfonelemrnh  13365  ennnfonelemfun  13366  ennnfonelemf1  13367  ennnfonelemrn  13368  ennnfonelemnn0  13371  ctinfomlemom  13376  ctiunctlemudc  13386  unct  13391  omctfn  13392  ssnnctlemct  13395  nninfdclemp1  13399  nninfdc  13402  structfung  13427  setsfun  13445  setsfun0  13446  setscom  13450  strslfv3  13456  setsslid  13461  imasaddfnlemg  13694  imasaddvallemg  13695  mgmsscl  13740  plusffng  13744  mgmplusf  13745  mgm0  13748  mgm1  13749  opifismgmdc  13750  gzsumfzval  13770  sgrp1  13785  issgrpd  13786  mndpfo  13810  mndfo  13811  mnd1  13821  0subm  13850  mhmima  13857  grpinvfng  13908  isgrpinv  13918  grpinvid  13924  grpinvf1o  13934  grpinvadd  13942  grpsubf  13943  grpsubsub4  13957  grplactcnv  13966  grp1  13970  grp1inv  13971  qusgrp2  13975  mulgfng  13986  subginv  14043  resgrpisgrp  14057  subgintm  14060  0subg  14061  0nsg  14076  qusinv  14098  ghminv  14112  ghmrn  14119  ghmeql  14129  ghmnsgima  14130  kerf1ghm  14136  conjnmz  14141  cntzval  14153  cntz2ss  14168  cntzsubg  14171  cntzmhm  14173  cntzmhm2  14174  gzsumshift  14239  gsumvalfi  14242  gzsumgsum  14245  gsumsncmn  14246  gsump1  14247  gsumf1ofi  14250  gsumsubmclfi  14253  gsummptfidmsplit  14254  idjusnfi  14270  prdsplusgsgrpcl  14297  prdsplusgcl  14299  prdsidlem  14300  prdsinvlem  14303  prdsinvgd  14305  pwsdiagel  14317  pwssnf1o  14318  rngass  14345  rngmneg1  14353  rngmneg2  14354  qusrng  14364  srgideu  14383  srgidmlem  14389  srgpcomp  14401  srg1expzeq1  14406  ringcl  14424  ringideu  14428  ringidmlem  14434  ringnegl  14463  ringnegr  14464  ring1  14471  qusring2  14480  opprringbg  14494  dvdsrd  14510  dvdsr01  14520  isunitd  14522  unitinvcl  14539  unitinvinv  14540  unitnegcl  14546  rhmmul  14580  rhmf1o  14584  nzrunit  14604  lringuplu  14612  subrngintm  14629  subrgsubm  14651  subrgintm  14660  rrgsupp  14683  ringunitap  14702  aprsym  14705  aprnzr  14708  aprlring  14709  drnglring  14716  drngunitap  14717  scaffng  14755  lmodscaf  14756  lsssn0  14816  lss1d  14829  lssintclm  14830  lspval  14836  lspcl  14837  lspsnid  14853  lspprid1  14857  lspsn  14862  sraval  14883  rspcl  14937  rspssid  14938  rspssp  14940  rnglidlmmgm  14942  rnglidlmsgrp  14943  cnfldneg  15019  zringinvg  15048  expghmap  15051  znzrhfo  15092  znf1o  15095  znhash  15100  znidomb  15102  znrrg  15104  psrbagfsupp  15164  psrbagfi  15168  psrbaglecl  15169  psrbagaddclfi  15170  psrbagcon  15171  psrbaglefifi  15172  psraddcl  15184  psrmulclfilem  15189  psr0cl  15191  psrnegcl  15193  psrneg  15197  psr1clfi  15198  psrlidmfi  15199  psrridmfi  15200  mplsubgfilemm  15214  mplsubgfilemcl  15215  baspartn  15276  eltg3i  15282  tgclb  15291  topbas  15293  2basgeng  15308  topcld  15335  0cld  15338  uncld  15339  neif  15367  elnei  15378  0nei  15392  restbasg  15394  iscnp4  15444  cnpnei  15445  cnclima  15449  cncnp  15456  cnrest2r  15463  cndis  15467  lmff  15475  lmtopcnp  15476  txbas  15484  txopn  15491  txcnp  15497  upxp  15498  txdis1cn  15504  cnmpt11  15509  cnmpt21  15517  psmetge0  15557  xmetge0  15591  xmettpos  15596  xmetrtri  15602  metrtri  15603  xblpnfps  15624  xblpnf  15625  blfps  15635  blf  15636  ssblps  15651  ssbl  15652  blbas  15659  metss2  15724  xmettxlem  15735  xmettx  15736  qtopbas  15748  divcnap  15791  cncfss  15809  cdivcncfap  15830  expcncf  15835  cnopnap  15837  maxcncf  15841  mincncf  15842  dedekindeulemuub  15843  dedekindeulemlu  15847  dedekindeu  15849  suplociccex  15851  dedekindicclemuub  15852  dedekindicclemlu  15856  dedekindicclemicc  15858  ivthinclemlopn  15862  ivthinclemuopn  15864  ivthinc  15869  ivthreinc  15871  hoverlt1  15875  ellimc3apf  15886  limcimolemlt  15890  limcimo  15891  limcresi  15892  cnplimclemle  15894  reldvg  15905  dvfgg  15914  dvidlemap  15917  dvidrelem  15918  dvidsslem  15919  dvcjbr  15934  dvcj  15935  dvrecap  15939  dveflem  15952  dvef  15953  elply2  15961  elplyr  15966  plycj  15987  plyreres  15990  reeff1oleme  15998  efap1p  16005  pilem3  16010  sinq34lt0t  16058  cosq14gt0  16059  coseq0q4123  16061  tangtx  16065  sincosq1eq  16066  cosordlem  16077  logdivlti  16111  logdivlt  16124  relogbval  16187  relogbzcl  16188  nnlogbexp  16195  logbgcd1irr  16203  logbgcd1irraplemexp  16204  logbgcd1irraplemap  16205  zprmlogbaplem2  16216  zprmlogbap  16218  birthdaylem2  16226  birthdaylem3  16227  pellexlem1  16229  pellexlem3  16231  wilthlem1  16232  efchtqdvds  16265  ppiqwordi  16268  ppiqeq0  16280  mpodvdsmulf1o  16284  ppiqub  16293  chtqleppi  16294  chtublem  16295  chtqub  16296  mersenne  16297  perfectlem2  16300  perfect  16301  bcmono  16304  bcmax  16305  bposlem1  16311  bposlem2  16312  bposlem3  16313  bposlem6  16316  bposlem7  16317  bposlem9  16319  zabsle1  16323  lgslem1  16324  lgsval  16328  lgsfvalg  16329  lgsfcl2  16330  lgsval2lem  16334  lgscl1  16347  lgsmod  16350  lgsdir2lem5  16356  lgsdir2  16357  lgsdilem2  16360  lgsdi  16361  lgsne0  16362  gausslemma2dlem0c  16375  gausslemma2dlem0h  16380  gausslemma2dlem1a  16382  gausslemma2dlem1f1o  16384  gausslemma2dlem3  16387  lgseisenlem1  16394  lgseisenlem2  16395  lgseisenlem3  16396  lgseisenlem4  16397  lgseisen  16398  lgsquadlem1  16401  lgsquadlem2  16402  lgsquadlem3  16403  lgsquad3  16408  2lgslem3b1  16422  2lgslem3c1  16423  2lgs  16428  2lgsoddprmlem2  16430  2lgsoddprm  16437  2sqlem3  16441  2sqlem8  16447  2sqlem10  16449  structgrssvtx  16488  structgrssiedg  16489  ushgruhgr  16526  uhgrun  16532  incistruhgr  16536  upgrop  16550  upgruhgr  16557  umgrupgr  16558  umgrnloopv  16560  umgredgprv  16561  umgr0e  16564  upgr1edc  16567  umgr1een  16571  upgrun  16572  umgrun  16574  umgrislfupgrdom  16577  upgredg  16590  umgrpredgv  16593  usgrop  16612  usgrausgrien  16615  ausgrumgrien  16616  ausgrusgrien  16617  uspgrupgrushgr  16628  usgrumgr  16630  usgrumgruspgr  16631  usgruspgrben  16632  usgrislfuspgrdom  16636  edgssv2en  16645  usgrf1oedg  16651  usgredg4  16661  usgredg2vlem2  16669  usgredg2v  16670  ushgredgedg  16672  ushgredgedgloop  16674  usgrstrrepeen  16677  usgr0e  16678  uhgr0v0e  16680  uspgr1edc  16686  usgr1e  16687  griedg0ssusgr  16697  subgrprop3  16708  subgruhgredgdm  16716  subuhgr  16718  subupgr  16719  subumgr  16720  subusgr  16721  uhgrspansubgrlem  16722  1loopgrvd2fi  16751  1loopgrvd0fi  16752  1hevtxdg0fi  16753  vdegp1aid  16760  vdegp1bid  16761  wlkm  16785  wlkvtxiedg  16791  wlkvtxiedgg  16792  wlkeq  16800  wlk1walkdom  16805  uspgr2wlkeq  16811  uspgr2wlkeqi  16813  upgr2wlkdc  16823  wlkres  16825  trlreslem  16835  clwwlkccatlem  16846  clwwlkn1loopb  16866  clwwlkext2edg  16868  clwwlknonex2lem1  16883  clwwlknonex2  16885  trlsegvdeglem2  16907  trlsegvdeglem3  16908  eupth2lem3lem4fi  16919  eupth2lemsfi  16924  fnmptd  17037  bj-sels  17145  bj-nnelon  17190  pw1map  17230  pwle2  17233  pwf1oexmid  17234  pw1nct  17238  stnot  17244  nninfall  17258  nninfsellemdc  17259  nninfself  17262  nnnninfex  17271  nninfnfiinf  17272  refeq  17279  isomninnlem  17285  cvgcmp2nlemabs  17287  trilpolemlt1  17297  trirec0  17300  apdifflemf  17302  apdifflemr  17303  apdiff  17304  qdiff  17305  iswomninnlem  17306  iswomni0  17308  ismkvnnlem  17309  reap0  17315  cndcap  17316