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  6545  smores2  6570  tfrlemisucaccv  6601  tfrlemibfn  6604  tfr1onlemsucaccv  6617  tfr1onlembfn  6620  tfrcllemsucaccv  6630  tfrcllembfn  6633  tfrcl  6640  tfri3  6643  frecabcl  6675  nnsucsssuc  6770  ersym  6824  ertr  6827  swoer  6840  erth  6858  riinerm  6887  qliftfund  6897  eroprf  6907  ecopoverg  6915  th3qlem1  6916  mapfoss  6952  elmapssres  6959  mapm  6975  mapss  6979  fdiagfn  6980  ixpssmap2g  7015  mapsnf1o  7025  f1oen4g  7044  f1dom4g  7045  f1dom2g  7048  dom3d  7066  en2prd  7112  dom1oi  7123  pw2f1odclem  7140  fopwdom  7142  mapxpen  7154  nndomo  7171  dif1en  7189  findcard2  7199  findcard2s  7200  diffisn  7203  fimax2gtrilemstep  7211  eqsndc  7216  fientri3  7228  tpfidceq  7243  fiintim  7244  opabfi  7253  f1dmvrnfibi  7264  sbthlemi6  7286  funisfsuppdc  7298  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  9689  peano2zm  9691  ztri3or  9696  nn0n0n1ge2  9724  zextle  9747  gtndiv  9751  suprzclex  9754  nn0ind-raph  9773  uzid  9951  uzneg  9956  uztric  9959  uz11  9960  eluzp1l  9962  qdivcl  10058  irrmul  10063  irrmulap  10064  rpnegap  10103  negelrpd  10105  ledivge1le  10143  mul2lt0rlt0  10176  mul2lt0rgt0  10177  nn0ledivnn  10184  ltpnf  10198  mnflt  10201  pnfge  10207  mnfle  10210  xrlttr  10213  xrltso  10214  xrlttri3  10215  xrleid  10218  xaddass2  10288  xltadd1  10294  xlt2add  10298  xleaddadd  10305  lincmble  10422  iccf1o  10423  fztri3or  10459  fznlem  10461  fzn  10462  fzsplit2  10471  fzsplit3  10474  fznatpl1  10499  uzsplit  10515  fseq1p1m1  10517  fzm1  10523  fznn0sub2  10551  difelfznle  10558  1fv  10562  fzodcel  10576  fzospliti  10601  fzouzsplit  10604  eluzgtdifelfzo  10631  exfzdc  10675  subfzo0  10677  zsupcllemstep  10678  zsupcl  10680  zssinfcl  10681  infssuzex  10682  infssuzcldc  10684  infssfzcldc  10685  infssfzledc  10686  suprzubdc  10687  nninfdcex  10688  qdcle  10697  exbtwnz  10701  qbtwnrelemcalc  10706  flqlelt  10728  flaplelt  10729  qfraclt1  10733  qfracge0  10734  flaplt  10738  flqltnz  10742  btwnzge0  10755  flhalf  10757  fldiv4lem1div2uz2  10761  ceiqle  10770  intfracq  10777  mulqmod0  10787  modqge0  10789  modqlt  10790  modqid  10806  modqid0  10807  m1modge3gt1  10828  modqltm1p1mod  10833  q2txmodxeq0  10841  modaddmodlo  10845  modsumfzodifsn  10853  addmodlteq  10855  frecuzrdgtcl  10869  frecuzrdgtclt  10878  uzennn  10893  uzsinds  10901  seqf  10921  seqf2  10925  monoord2  10943  iseqf1olemqk  10964  iseqf1olemjpcl  10965  iseqf1olemqpcl  10966  seq3f1olemqsumkj  10968  seq3f1olemqsum  10970  seq3f1olemstep  10971  seq3f1oleml  10973  seqf1oglem1  10976  ser3le  10994  exp3vallem  10997  exp3val  10998  expp1  11003  expcllem  11007  ltexp2a  11048  leexp2a  11049  resq01  11115  nn0ltexp2  11168  faclbnd  11200  faclbnd2  11201  faclbnd3  11202  bcval5  11222  bcpasc  11225  bcm1n  11228  hashennn  11240  fihasheqf1oi  11247  hashsng  11258  fihashfn  11261  hashun  11266  fihashss  11278  fihashssdif  11280  hashfz  11283  hashxp  11288  hashmap  11289  hashpwfi  11290  fimaxq  11291  sseqn  11300  hashfibclem  11303  hashf1lem2  11307  hashf1  11308  zfz1isolem1  11313  seq3coll  11315  hashdmprop2dom  11317  wrdf  11331  wrdlenge2n0  11361  fstwrdne0  11365  wrdred1hash  11369  ccatvalfn  11390  ccatsymb  11391  ccatlid  11395  ccatrid  11396  ccatrn  11398  ccatalpha  11402  eqs1  11417  ccats1val2  11429  fzowrddc  11440  swrdlen  11445  swrdnd  11452  swrd0g  11453  swrdfv2  11456  swrdwrdsymbg  11457  pfxn0  11481  pfxwrdsymbg  11483  pfxsuff1eqwrdeq  11492  swrdswrd  11498  ccats1pfxeq  11507  ccats1pfxeqrex  11508  wrdind  11515  wrd2ind  11516  swrdccatin1  11518  pfxccatin12lem4  11519  swrdccatin2  11522  pfxccatin12  11526  pfxccat3a  11531  swrdccat3blem  11532  pfxccatid  11534  swrdccatin2d  11537  shftfn  11610  cjth  11632  cjmulrcl  11673  sq01  11681  reim0bd  11731  rerebd  11732  cjrebd  11733  caucvgre  11768  cvg1nlemcxze  11769  cvg1nlemcau  11771  cvg1nlemres  11772  recvguniq  11782  resqrexlemover  11797  resqrexlemdec  11798  resqrexlemgt0  11807  resqrexlemoverl  11808  resqrexlemglsq  11809  rersqrtthlem  11817  sqrtgt0  11821  leabs  11861  absexpzap  11868  absle  11877  recvalap  11885  abstri  11892  abs2dif  11894  amgm2  11906  absne0d  11975  maxleim  11993  maxabslemab  11994  maxabslemlub  11995  maxltsup  12006  zmaxcl  12012  fimaxre2  12015  minmax  12019  rpmincl  12027  zmincl  12028  bdtrilem  12029  bdtri  12030  xrmaxleim  12034  xrmaxiflemcom  12039  xrmaxltsup  12048  xrmaxadd  12051  xrminmax  12055  xrminrpcl  12064  climconst  12080  climuni  12083  2clim  12091  climcn1  12098  climcn2  12099  reccn2ap  12103  climge0  12115  climle  12124  climsqz  12125  climsqz2  12126  serf0  12142  summodclem3  12171  summodclem2a  12172  fsumcl2lem  12189  sumpr  12204  sumtp  12205  fsum0diaglem  12231  mptfzshft  12233  fsumle  12254  fsumlt  12255  divcnv  12288  trireciplem  12291  expcnvap0  12293  expcnv  12295  explecnv  12296  geosergap  12297  cvgratnnlembern  12314  cvgratnnlemabsle  12318  cvgratnnlemsumlt  12319  cvgratz  12323  cvgratgt0  12324  mertenslemi1  12326  mertenslem2  12327  mertensabs  12328  clim2divap  12331  prodmodclem3  12366  prodmodclem2a  12367  fprodseq  12374  fprodmul  12382  fprodfac  12406  fprodconst  12411  fprodap0  12412  fprodap0f  12427  fprodle  12431  eftcl  12445  ef0lem  12451  efsub  12472  eftlub  12481  eflegeo  12492  tanval2ap  12504  sinadd  12527  cos2t  12541  cos2tsin  12542  sin01bnd  12548  cos01bnd  12549  eirraplem  12568  dvdsval2  12581  dvdsdc  12589  dvds0lem  12592  zdvdsdc  12603  dvdscmulr  12611  dvdsmulcr  12612  fsumdvds  12633  dvdslelemd  12634  divconjdvds  12640  dvdsext  12646  fzm1ndvds  12647  dvdsmod  12653  3dvds  12655  oexpneg  12668  2tp1odd  12675  mulsucdiv2z  12676  2teven  12678  zeo5  12679  opeo  12688  omeo  12689  nn0ob  12699  divalglemnqt  12711  bitsdc  12738  bits0o  12741  bitsfzolem  12745  bitsfzo  12746  bitsmod  12747  bitscmp  12749  bitsinv1lem  12752  gcddvds  12764  dvdslegcd  12765  gcdneg  12783  bezoutlemnewy  12797  bezoutlemstep  12798  bezoutlema  12800  bezoutlemb  12801  bezoutlemmo  12807  bezoutlemle  12809  bezoutlemsup  12810  dfgcd3  12811  bezout  12812  dfgcd2  12815  uzwodc  12838  lcmcllem  12869  lcmneg  12876  lcmgcdlem  12879  lcmdvds  12881  lcmid  12882  3lcm2e6woprm  12888  6lcm4e12  12889  ncoprmgcdne1b  12891  mulgcddvds  12896  divgcdcoprmex  12904  cncongr1  12905  cncongr2  12906  isprm2lem  12918  prmind2  12922  dvdsnprmd  12927  prm2orodd  12928  sqnprm  12939  isprm5lem  12944  rpexp  12956  sqrt2irrlem  12964  nnmaxpwlemparts  12976  sqrt2irraplemnn  12983  qnumdencoprm  12997  qeqnumdivden  12998  nn0gcdsq  13004  nn0sqrtelqelz  13010  nonsq  13011  sqrtrirr  13013  phicl2  13020  phibnd  13023  hashdvds  13027  phiprmpw  13028  phimullem  13031  eulerthlemrprm  13035  eulerthlema  13036  eulerthlemth  13038  prmdiveq  13042  hashgcdlem  13044  odzdvds  13052  modprminv  13056  nnnn0modprm0  13062  modprmn0modprm0  13063  pythagtriplem10  13076  pythagtriplem19  13089  pythagtrip  13090  pcpre1  13099  pcpremul  13100  pceu  13102  pcmul  13108  pcdiv  13109  pcqmul  13110  pcqdiv  13114  pcexp  13116  pcdvdsb  13127  pcidlem  13130  pcdvdstr  13134  pcgcd1  13135  pc2dvds  13137  pcprmpw2  13140  difsqpwdvds  13145  pcaddlem  13146  pcadd  13147  pcadd2  13148  pcmpt  13150  pcmptdvds  13152  pcprod  13153  fldivp1  13155  pcfaclem  13156  pcfac  13157  pcbc  13158  qexpz  13159  pockthlem  13163  pockthg  13164  1arithlem4  13173  1arith  13174  1arith2  13175  4sqlem6  13190  4sqlem8  13192  4sqlem9  13193  4sqlem10  13194  4sqexercise1  13205  4sqexercise2  13206  4sqlemsdc  13207  4sqlem11  13208  4sqlem12  13209  4sqlem15  13212  4sqlem16  13213  4sqlem17  13214  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemimin  13306  ballotfilem1c  13308  ballotfilemro  13323  ballotfilemfrcn0  13330  znnen  13346  ennnfonelemk  13348  ennnfonelemkh  13360  ennnfonelemhf1o  13361  ennnfonelemrnh  13364  ennnfonelemfun  13365  ennnfonelemf1  13366  ennnfonelemrn  13367  ennnfonelemnn0  13370  ctinfomlemom  13375  ctiunctlemudc  13385  unct  13390  omctfn  13391  ssnnctlemct  13394  nninfdclemp1  13398  nninfdc  13401  structfung  13426  setsfun  13444  setsfun0  13445  setscom  13449  strslfv3  13455  setsslid  13460  imasaddfnlemg  13693  imasaddvallemg  13694  mgmsscl  13739  plusffng  13743  mgmplusf  13744  mgm0  13747  mgm1  13748  opifismgmdc  13749  gzsumfzval  13769  sgrp1  13784  issgrpd  13785  mndpfo  13809  mndfo  13810  mnd1  13820  0subm  13849  mhmima  13856  grpinvfng  13907  isgrpinv  13917  grpinvid  13923  grpinvf1o  13933  grpinvadd  13941  grpsubf  13942  grpsubsub4  13956  grplactcnv  13965  grp1  13969  grp1inv  13970  qusgrp2  13974  mulgfng  13985  subginv  14042  resgrpisgrp  14056  subgintm  14059  0subg  14060  0nsg  14075  qusinv  14097  ghminv  14111  ghmrn  14118  ghmeql  14128  ghmnsgima  14129  kerf1ghm  14135  conjnmz  14140  cntzval  14152  cntz2ss  14167  cntzsubg  14170  cntzmhm  14172  cntzmhm2  14173  gzsumshift  14238  gsumvalfi  14241  gzsumgsum  14244  gsumsncmn  14245  gsump1  14246  gsumf1ofi  14249  gsumsubmclfi  14252  gsummptfidmsplit  14253  idjusnfi  14269  prdsplusgsgrpcl  14296  prdsplusgcl  14298  prdsidlem  14299  prdsinvlem  14302  prdsinvgd  14304  pwsdiagel  14316  pwssnf1o  14317  rngass  14344  rngmneg1  14352  rngmneg2  14353  qusrng  14363  srgideu  14382  srgidmlem  14388  srgpcomp  14400  srg1expzeq1  14405  ringcl  14423  ringideu  14427  ringidmlem  14433  ringnegl  14462  ringnegr  14463  ring1  14470  qusring2  14479  opprringbg  14493  dvdsrd  14509  dvdsr01  14519  isunitd  14521  unitinvcl  14538  unitinvinv  14539  unitnegcl  14545  rhmmul  14579  rhmf1o  14583  nzrunit  14603  lringuplu  14611  subrngintm  14628  subrgsubm  14650  subrgintm  14659  rrgsupp  14682  ringunitap  14701  aprsym  14704  aprnzr  14707  aprlring  14708  drnglring  14715  drngunitap  14716  scaffng  14754  lmodscaf  14755  lsssn0  14815  lss1d  14828  lssintclm  14829  lspval  14835  lspcl  14836  lspsnid  14852  lspprid1  14856  lspsn  14861  sraval  14882  rspcl  14936  rspssid  14937  rspssp  14939  rnglidlmmgm  14941  rnglidlmsgrp  14942  cnfldneg  15018  zringinvg  15047  expghmap  15050  znzrhfo  15091  znf1o  15094  znhash  15099  znidomb  15101  znrrg  15103  psrbagfsuppfi  15165  psrbagfi  15166  psrbagdceq  15167  snifpsrbagfi  15168  psrbaglecl  15172  psrbagaddclfi  15173  psrbagcon  15174  psrbaglefifi  15175  psrbagmaxlemfi  15180  psrbagmaxlem1x  15181  psrbagmaxlem1y  15182  psraddcl  15193  psrmulclfilem  15198  psr0cl  15200  psrnegcl  15202  psrneg  15206  psr1clfi  15207  psrlidmfi  15208  psrridmfi  15209  mvrffi  15218  mvrclfi  15226  mplsubgfilemm  15231  mplsubgfilemcl  15232  mplsubgfileminv  15233  baspartn  15293  eltg3i  15299  tgclb  15308  topbas  15310  2basgeng  15325  topcld  15352  0cld  15355  uncld  15356  neif  15384  elnei  15395  0nei  15409  restbasg  15411  iscnp4  15461  cnpnei  15462  cnclima  15466  cncnp  15473  cnrest2r  15480  cndis  15484  lmff  15492  lmtopcnp  15493  txbas  15501  txopn  15508  txcnp  15514  upxp  15515  txdis1cn  15521  cnmpt11  15526  cnmpt21  15534  psmetge0  15574  xmetge0  15608  xmettpos  15613  xmetrtri  15619  metrtri  15620  xblpnfps  15641  xblpnf  15642  blfps  15652  blf  15653  ssblps  15668  ssbl  15669  blbas  15676  metss2  15741  xmettxlem  15752  xmettx  15753  qtopbas  15765  divcnap  15808  cncfss  15826  cdivcncfap  15847  expcncf  15852  cnopnap  15854  maxcncf  15858  mincncf  15859  dedekindeulemuub  15860  dedekindeulemlu  15864  dedekindeu  15866  suplociccex  15868  dedekindicclemuub  15869  dedekindicclemlu  15873  dedekindicclemicc  15875  ivthinclemlopn  15879  ivthinclemuopn  15881  ivthinc  15886  ivthreinc  15888  hoverlt1  15892  ellimc3apf  15903  limcimolemlt  15907  limcimo  15908  limcresi  15909  cnplimclemle  15911  reldvg  15922  dvfgg  15931  dvidlemap  15934  dvidrelem  15935  dvidsslem  15936  dvcjbr  15951  dvcj  15952  dvrecap  15956  dveflem  15969  dvef  15970  elply2  15978  elplyr  15983  plycj  16004  plyreres  16007  reeff1oleme  16015  efap1p  16022  pilem3  16027  sinq34lt0t  16075  cosq14gt0  16076  coseq0q4123  16078  tangtx  16082  sincosq1eq  16083  cosordlem  16094  logdivlti  16128  logdivlt  16141  relogbval  16204  relogbzcl  16205  nnlogbexp  16212  logbgcd1irr  16220  logbgcd1irraplemexp  16221  logbgcd1irraplemap  16222  zprmlogbaplem2  16233  zprmlogbap  16235  birthdaylem2  16243  birthdaylem3  16244  pellexlem1  16246  pellexlem3  16248  wilthlem1  16249  efchtqdvds  16282  ppiqwordi  16285  ppiqeq0  16297  mpodvdsmulf1o  16301  ppiqub  16310  chtqleppi  16311  chtublem  16312  chtqub  16313  mersenne  16314  perfectlem2  16317  perfect  16318  bcmono  16321  bcmax  16322  bposlem1  16328  bposlem2  16329  bposlem3  16330  bposlem6  16333  bposlem7  16334  bposlem9  16336  zabsle1  16340  lgslem1  16341  lgsval  16345  lgsfvalg  16346  lgsfcl2  16347  lgsval2lem  16351  lgscl1  16364  lgsmod  16367  lgsdir2lem5  16373  lgsdir2  16374  lgsdilem2  16377  lgsdi  16378  lgsne0  16379  gausslemma2dlem0c  16392  gausslemma2dlem0h  16397  gausslemma2dlem1a  16399  gausslemma2dlem1f1o  16401  gausslemma2dlem3  16404  lgseisenlem1  16411  lgseisenlem2  16412  lgseisenlem3  16413  lgseisenlem4  16414  lgseisen  16415  lgsquadlem1  16418  lgsquadlem2  16419  lgsquadlem3  16420  lgsquad3  16425  2lgslem3b1  16439  2lgslem3c1  16440  2lgs  16445  2lgsoddprmlem2  16447  2lgsoddprm  16454  2sqlem3  16458  2sqlem8  16464  2sqlem10  16466  structgrssvtx  16505  structgrssiedg  16506  ushgruhgr  16543  uhgrun  16549  incistruhgr  16553  upgrop  16567  upgruhgr  16574  umgrupgr  16575  umgrnloopv  16577  umgredgprv  16578  umgr0e  16581  upgr1edc  16584  umgr1een  16588  upgrun  16589  umgrun  16591  umgrislfupgrdom  16594  upgredg  16607  umgrpredgv  16610  usgrop  16629  usgrausgrien  16632  ausgrumgrien  16633  ausgrusgrien  16634  uspgrupgrushgr  16645  usgrumgr  16647  usgrumgruspgr  16648  usgruspgrben  16649  usgrislfuspgrdom  16653  edgssv2en  16662  usgrf1oedg  16668  usgredg4  16678  usgredg2vlem2  16686  usgredg2v  16687  ushgredgedg  16689  ushgredgedgloop  16691  usgrstrrepeen  16694  usgr0e  16695  uhgr0v0e  16697  uspgr1edc  16703  usgr1e  16704  griedg0ssusgr  16714  subgrprop3  16725  subgruhgredgdm  16733  subuhgr  16735  subupgr  16736  subumgr  16737  subusgr  16738  uhgrspansubgrlem  16739  1loopgrvd2fi  16768  1loopgrvd0fi  16769  1hevtxdg0fi  16770  vdegp1aid  16777  vdegp1bid  16778  wlkm  16802  wlkvtxiedg  16808  wlkvtxiedgg  16809  wlkeq  16817  wlk1walkdom  16822  uspgr2wlkeq  16828  uspgr2wlkeqi  16830  upgr2wlkdc  16840  wlkres  16842  trlreslem  16852  clwwlkccatlem  16863  clwwlkn1loopb  16883  clwwlkext2edg  16885  clwwlknonex2lem1  16900  clwwlknonex2  16902  trlsegvdeglem2  16924  trlsegvdeglem3  16925  eupth2lem3lem4fi  16936  eupth2lemsfi  16941  fnmptd  17054  bj-sels  17162  bj-nnelon  17207  pw1map  17247  pwle2  17250  pwf1oexmid  17251  pw1nct  17255  stnot  17261  nninfall  17275  nninfsellemdc  17276  nninfself  17279  nnnninfex  17288  nninfnfiinf  17289  refeq  17296  isomninnlem  17302  cvgcmp2nlemabs  17304  trilpolemlt1  17314  trirec0  17317  apdifflemf  17319  apdifflemr  17320  apdiff  17321  qdiff  17322  iswomninnlem  17323  iswomni0  17325  ismkvnnlem  17326  reap0  17332  cndcap  17333