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  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  8448  readdcan  8467  addneintrd  8515  addneintr2d  8516  pncan  8533  subsub2  8555  subsub4  8560  negned  8635  subne0d  8647  subneintrd  8682  subneintr2d  8684  subeq0bd  8707  subdi  8713  gt0add  8903  rimul  8915  rereim  8916  ltmul1a  8921  apreim  8933  apirr  8935  mulap0r  8945  msqge0  8946  mulge0  8949  gt0ap0  8956  ltap  8963  subap0d  8974  recexaplem2  8982  mulap0bad  8989  mulap0bbd  8990  mul0eqap  9002  divrecap  9020  div0ap  9034  div1  9035  recrecap  9041  divdivdivap  9045  ddcanap  9058  rerecclap  9062  div2negap  9067  diveqap1bd  9168  recgt0  9182  prodgt0  9184  lemul1a  9190  recp1lt1  9231  squeeze0  9236  peano2nn  9318  div4p1lem1div2  9563  arch  9564  peano2z  9684  peano2zm  9686  ztri3or  9691  nn0n0n1ge2  9719  zextle  9741  gtndiv  9745  suprzclex  9748  nn0ind-raph  9767  uzid  9945  uzneg  9950  uztric  9953  uz11  9954  eluzp1l  9956  qdivcl  10052  irrmul  10057  irrmulap  10058  rpnegap  10097  negelrpd  10099  ledivge1le  10137  mul2lt0rlt0  10170  mul2lt0rgt0  10171  nn0ledivnn  10178  ltpnf  10192  mnflt  10195  pnfge  10201  mnfle  10204  xrlttr  10207  xrltso  10208  xrlttri3  10209  xrleid  10212  xaddass2  10282  xltadd1  10288  xlt2add  10292  xleaddadd  10299  lincmble  10416  iccf1o  10417  fztri3or  10453  fznlem  10455  fzn  10456  fzsplit2  10465  fzsplit3  10468  fznatpl1  10493  uzsplit  10509  fseq1p1m1  10511  fzm1  10517  fznn0sub2  10545  difelfznle  10552  1fv  10556  fzodcel  10570  fzospliti  10595  fzouzsplit  10598  eluzgtdifelfzo  10625  exfzdc  10669  subfzo0  10671  zsupcllemstep  10672  zsupcl  10674  zssinfcl  10675  infssuzex  10676  infssuzcldc  10678  infssfzcldc  10679  infssfzledc  10680  suprzubdc  10681  nninfdcex  10682  qdcle  10691  exbtwnz  10695  qbtwnrelemcalc  10700  flqlelt  10722  flaplelt  10723  qfraclt1  10727  qfracge0  10728  flqltnz  10735  btwnzge0  10748  flhalf  10750  fldiv4lem1div2uz2  10754  ceiqle  10763  intfracq  10770  mulqmod0  10780  modqge0  10782  modqlt  10783  modqid  10799  modqid0  10800  m1modge3gt1  10821  modqltm1p1mod  10826  q2txmodxeq0  10834  modaddmodlo  10838  modsumfzodifsn  10846  addmodlteq  10848  frecuzrdgtcl  10862  frecuzrdgtclt  10871  uzennn  10886  uzsinds  10894  seqf  10914  seqf2  10918  monoord2  10936  iseqf1olemqk  10957  iseqf1olemjpcl  10958  iseqf1olemqpcl  10959  seq3f1olemqsumkj  10961  seq3f1olemqsum  10963  seq3f1olemstep  10964  seq3f1oleml  10966  seqf1oglem1  10969  ser3le  10987  exp3vallem  10990  exp3val  10991  expp1  10996  expcllem  11000  ltexp2a  11041  leexp2a  11042  resq01  11108  nn0ltexp2  11161  faclbnd  11193  faclbnd2  11194  faclbnd3  11195  bcval5  11215  bcpasc  11218  bcm1n  11221  hashennn  11233  fihasheqf1oi  11240  hashsng  11251  fihashfn  11254  hashun  11259  fihashss  11271  fihashssdif  11273  hashfz  11276  hashxp  11281  hashmap  11282  hashpwfi  11283  fimaxq  11284  sseqn  11293  hashfibclem  11296  hashf1lem2  11300  hashf1  11301  zfz1isolem1  11306  seq3coll  11308  hashdmprop2dom  11310  wrdf  11324  wrdlenge2n0  11354  fstwrdne0  11358  wrdred1hash  11362  ccatvalfn  11383  ccatsymb  11384  ccatlid  11388  ccatrid  11389  ccatrn  11391  ccatalpha  11395  eqs1  11410  ccats1val2  11422  fzowrddc  11433  swrdlen  11438  swrdnd  11445  swrd0g  11446  swrdfv2  11449  swrdwrdsymbg  11450  pfxn0  11474  pfxwrdsymbg  11476  pfxsuff1eqwrdeq  11485  swrdswrd  11491  ccats1pfxeq  11500  ccats1pfxeqrex  11501  wrdind  11508  wrd2ind  11509  swrdccatin1  11511  pfxccatin12lem4  11512  swrdccatin2  11515  pfxccatin12  11519  pfxccat3a  11524  swrdccat3blem  11525  pfxccatid  11527  swrdccatin2d  11530  shftfn  11603  cjth  11625  cjmulrcl  11666  sq01  11674  reim0bd  11724  rerebd  11725  cjrebd  11726  caucvgre  11761  cvg1nlemcxze  11762  cvg1nlemcau  11764  cvg1nlemres  11765  recvguniq  11775  resqrexlemover  11790  resqrexlemdec  11791  resqrexlemgt0  11800  resqrexlemoverl  11801  resqrexlemglsq  11802  rersqrtthlem  11810  sqrtgt0  11814  leabs  11854  absexpzap  11861  absle  11870  recvalap  11878  abstri  11885  abs2dif  11887  amgm2  11899  absne0d  11968  maxleim  11986  maxabslemab  11987  maxabslemlub  11988  maxltsup  11999  zmaxcl  12005  fimaxre2  12008  minmax  12011  rpmincl  12019  zmincl  12020  bdtrilem  12021  bdtri  12022  xrmaxleim  12026  xrmaxiflemcom  12031  xrmaxltsup  12040  xrmaxadd  12043  xrminmax  12047  xrminrpcl  12056  climconst  12072  climuni  12075  2clim  12083  climcn1  12090  climcn2  12091  reccn2ap  12095  climge0  12107  climle  12116  climsqz  12117  climsqz2  12118  serf0  12134  summodclem3  12163  summodclem2a  12164  fsumcl2lem  12181  sumpr  12196  sumtp  12197  fsum0diaglem  12223  mptfzshft  12225  fsumle  12246  fsumlt  12247  divcnv  12280  trireciplem  12283  expcnvap0  12285  expcnv  12287  explecnv  12288  geosergap  12289  cvgratnnlembern  12306  cvgratnnlemabsle  12310  cvgratnnlemsumlt  12311  cvgratz  12315  cvgratgt0  12316  mertenslemi1  12318  mertenslem2  12319  mertensabs  12320  clim2divap  12323  prodmodclem3  12358  prodmodclem2a  12359  fprodseq  12366  fprodmul  12374  fprodfac  12398  fprodconst  12403  fprodap0  12404  fprodap0f  12419  fprodle  12423  eftcl  12437  ef0lem  12443  efsub  12464  eftlub  12473  eflegeo  12484  tanval2ap  12496  sinadd  12519  cos2t  12533  cos2tsin  12534  sin01bnd  12540  cos01bnd  12541  eirraplem  12560  dvdsval2  12573  dvdsdc  12581  dvds0lem  12584  zdvdsdc  12595  dvdscmulr  12603  dvdsmulcr  12604  fsumdvds  12625  dvdslelemd  12626  divconjdvds  12632  dvdsext  12638  fzm1ndvds  12639  dvdsmod  12645  3dvds  12647  oexpneg  12660  2tp1odd  12667  mulsucdiv2z  12668  2teven  12670  zeo5  12671  opeo  12680  omeo  12681  nn0ob  12691  divalglemnqt  12703  bitsdc  12730  bits0o  12733  bitsfzolem  12737  bitsfzo  12738  bitsmod  12739  bitscmp  12741  bitsinv1lem  12744  gcddvds  12756  dvdslegcd  12757  gcdneg  12775  bezoutlemnewy  12789  bezoutlemstep  12790  bezoutlema  12792  bezoutlemb  12793  bezoutlemmo  12799  bezoutlemle  12801  bezoutlemsup  12802  dfgcd3  12803  bezout  12804  dfgcd2  12807  uzwodc  12830  lcmcllem  12861  lcmneg  12868  lcmgcdlem  12871  lcmdvds  12873  lcmid  12874  3lcm2e6woprm  12880  6lcm4e12  12881  ncoprmgcdne1b  12883  mulgcddvds  12888  divgcdcoprmex  12896  cncongr1  12897  cncongr2  12898  isprm2lem  12910  prmind2  12914  dvdsnprmd  12919  prm2orodd  12920  sqnprm  12931  isprm5lem  12936  rpexp  12948  sqrt2irrlem  12956  nnmaxpwlemparts  12968  sqrt2irraplemnn  12975  qnumdencoprm  12989  qeqnumdivden  12990  nn0gcdsq  12996  nn0sqrtelqelz  13002  nonsq  13003  sqrtrirr  13005  phicl2  13012  phibnd  13015  hashdvds  13019  phiprmpw  13020  phimullem  13023  eulerthlemrprm  13027  eulerthlema  13028  eulerthlemth  13030  prmdiveq  13034  hashgcdlem  13036  odzdvds  13044  modprminv  13048  nnnn0modprm0  13054  modprmn0modprm0  13055  pythagtriplem10  13068  pythagtriplem19  13081  pythagtrip  13082  pcpre1  13091  pcpremul  13092  pceu  13094  pcmul  13100  pcdiv  13101  pcqmul  13102  pcqdiv  13106  pcexp  13108  pcdvdsb  13119  pcidlem  13122  pcdvdstr  13126  pcgcd1  13127  pc2dvds  13129  pcprmpw2  13132  difsqpwdvds  13137  pcaddlem  13138  pcadd  13139  pcadd2  13140  pcmpt  13142  pcmptdvds  13144  pcprod  13145  fldivp1  13147  pcfaclem  13148  pcfac  13149  pcbc  13150  qexpz  13151  pockthlem  13155  pockthg  13156  1arithlem4  13165  1arith  13166  1arith2  13167  4sqlem6  13182  4sqlem8  13184  4sqlem9  13185  4sqlem10  13186  4sqexercise1  13197  4sqexercise2  13198  4sqlemsdc  13199  4sqlem11  13200  4sqlem12  13201  4sqlem15  13204  4sqlem16  13205  4sqlem17  13206  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemimin  13298  ballotfilem1c  13300  ballotfilemro  13315  ballotfilemfrcn0  13322  znnen  13338  ennnfonelemk  13340  ennnfonelemkh  13352  ennnfonelemhf1o  13353  ennnfonelemrnh  13356  ennnfonelemfun  13357  ennnfonelemf1  13358  ennnfonelemrn  13359  ennnfonelemnn0  13362  ctinfomlemom  13367  ctiunctlemudc  13377  unct  13382  omctfn  13383  ssnnctlemct  13386  nninfdclemp1  13390  nninfdc  13393  structfung  13418  setsfun  13436  setsfun0  13437  setscom  13441  strslfv3  13447  setsslid  13452  imasaddfnlemg  13684  imasaddvallemg  13685  mgmsscl  13730  plusffng  13734  mgmplusf  13735  mgm0  13738  mgm1  13739  opifismgmdc  13740  gzsumfzval  13760  sgrp1  13775  issgrpd  13776  mndpfo  13800  mndfo  13801  mnd1  13811  0subm  13840  mhmima  13847  grpinvfng  13898  isgrpinv  13908  grpinvid  13914  grpinvf1o  13924  grpinvadd  13932  grpsubf  13933  grpsubsub4  13947  grplactcnv  13956  grp1  13960  grp1inv  13961  qusgrp2  13965  mulgfng  13976  subginv  14033  resgrpisgrp  14047  subgintm  14050  0subg  14051  0nsg  14066  qusinv  14088  ghminv  14102  ghmrn  14109  ghmeql  14119  ghmnsgima  14120  kerf1ghm  14126  conjnmz  14131  gzsumshift  14198  gsumvalfi  14201  gzsumgsum  14204  gsumsncmn  14205  gsump1  14206  gsumf1ofi  14209  gsumsubmclfi  14212  prdsplusgsgrpcl  14239  prdsplusgcl  14241  prdsidlem  14242  prdsinvlem  14245  prdsinvgd  14247  pwsdiagel  14259  pwssnf1o  14260  rngass  14287  rngmneg1  14295  rngmneg2  14296  qusrng  14306  srgideu  14325  srgidmlem  14331  srgpcomp  14343  srg1expzeq1  14348  ringcl  14366  ringideu  14370  ringidmlem  14376  ringnegl  14405  ringnegr  14406  ring1  14413  qusring2  14420  opprringbg  14434  dvdsrd  14450  dvdsr01  14460  isunitd  14462  unitinvcl  14479  unitinvinv  14480  unitnegcl  14486  rhmmul  14520  rhmf1o  14524  nzrunit  14544  lringuplu  14552  subrngintm  14569  subrgsubm  14591  subrgintm  14600  rrgsupp  14623  ringunitap  14642  aprsym  14645  aprnzr  14648  aprlring  14649  drnglring  14656  drngunitap  14657  scaffng  14695  lmodscaf  14696  lsssn0  14756  lss1d  14769  lssintclm  14770  lspval  14776  lspcl  14777  lspsnid  14793  lspprid1  14797  lspsn  14802  sraval  14823  rspcl  14877  rspssid  14878  rspssp  14880  rnglidlmmgm  14882  rnglidlmsgrp  14883  cnfldneg  14959  zringinvg  14988  expghmap  14991  znzrhfo  15032  znf1o  15035  znhash  15040  znidomb  15042  znrrg  15044  psrbagfsupp  15104  psrbagfi  15108  psrbaglecl  15109  psrbagaddclfi  15110  psrbagcon  15111  psraddcl  15120  psr0cl  15121  psrnegcl  15123  psrneg  15127  psr1clfi  15128  mplsubgfilemm  15138  mplsubgfilemcl  15139  baspartn  15200  eltg3i  15206  tgclb  15215  topbas  15217  2basgeng  15232  topcld  15259  0cld  15262  uncld  15263  neif  15291  elnei  15302  0nei  15316  restbasg  15318  iscnp4  15368  cnpnei  15369  cnclima  15373  cncnp  15380  cnrest2r  15387  cndis  15391  lmff  15399  lmtopcnp  15400  txbas  15408  txopn  15415  txcnp  15421  upxp  15422  txdis1cn  15428  cnmpt11  15433  cnmpt21  15441  psmetge0  15481  xmetge0  15515  xmettpos  15520  xmetrtri  15526  metrtri  15527  xblpnfps  15548  xblpnf  15549  blfps  15559  blf  15560  ssblps  15575  ssbl  15576  blbas  15583  metss2  15648  xmettxlem  15659  xmettx  15660  qtopbas  15672  divcnap  15715  cncfss  15733  cdivcncfap  15754  expcncf  15759  cnopnap  15761  maxcncf  15765  mincncf  15766  dedekindeulemuub  15767  dedekindeulemlu  15771  dedekindeu  15773  suplociccex  15775  dedekindicclemuub  15776  dedekindicclemlu  15780  dedekindicclemicc  15782  ivthinclemlopn  15786  ivthinclemuopn  15788  ivthinc  15793  ivthreinc  15795  hoverlt1  15799  ellimc3apf  15810  limcimolemlt  15814  limcimo  15815  limcresi  15816  cnplimclemle  15818  reldvg  15829  dvfgg  15838  dvidlemap  15841  dvidrelem  15842  dvidsslem  15843  dvcjbr  15858  dvcj  15859  dvrecap  15863  dveflem  15876  dvef  15877  elply2  15885  elplyr  15890  plycj  15911  plyreres  15914  reeff1oleme  15922  efap1p  15929  pilem3  15934  sinq34lt0t  15982  cosq14gt0  15983  coseq0q4123  15985  tangtx  15989  sincosq1eq  15990  cosordlem  16000  logdivlti  16033  logdivlt  16046  relogbval  16106  relogbzcl  16107  nnlogbexp  16114  logbgcd1irr  16122  logbgcd1irraplemexp  16123  logbgcd1irraplemap  16124  zprmlogbaplem2  16135  zprmlogbap  16137  birthdaylem2  16145  birthdaylem3  16146  pellexlem1  16148  pellexlem3  16150  wilthlem1  16151  ppiqwordi  16174  ppiqeq0  16182  mpodvdsmulf1o  16185  ppiqub  16194  mersenne  16195  perfectlem2  16198  perfect  16199  bcmono  16202  bcmax  16203  bposlem1  16209  bposlem2  16210  bposlem3  16211  zabsle1  16216  lgslem1  16217  lgsval  16221  lgsfvalg  16222  lgsfcl2  16223  lgsval2lem  16227  lgscl1  16240  lgsmod  16243  lgsdir2lem5  16249  lgsdir2  16250  lgsdilem2  16253  lgsdi  16254  lgsne0  16255  gausslemma2dlem0c  16268  gausslemma2dlem0h  16273  gausslemma2dlem1a  16275  gausslemma2dlem1f1o  16277  gausslemma2dlem3  16280  lgseisenlem1  16287  lgseisenlem2  16288  lgseisenlem3  16289  lgseisenlem4  16290  lgseisen  16291  lgsquadlem1  16294  lgsquadlem2  16295  lgsquadlem3  16296  lgsquad3  16301  2lgslem3b1  16315  2lgslem3c1  16316  2lgs  16321  2lgsoddprmlem2  16323  2lgsoddprm  16330  2sqlem3  16334  2sqlem8  16340  2sqlem10  16342  structgrssvtx  16381  structgrssiedg  16382  ushgruhgr  16419  uhgrun  16425  incistruhgr  16429  upgrop  16443  upgruhgr  16450  umgrupgr  16451  umgrnloopv  16453  umgredgprv  16454  umgr0e  16457  upgr1edc  16460  umgr1een  16464  upgrun  16465  umgrun  16467  umgrislfupgrdom  16470  upgredg  16483  umgrpredgv  16486  usgrop  16505  usgrausgrien  16508  ausgrumgrien  16509  ausgrusgrien  16510  uspgrupgrushgr  16521  usgrumgr  16523  usgrumgruspgr  16524  usgruspgrben  16525  usgrislfuspgrdom  16529  edgssv2en  16538  usgrf1oedg  16544  usgredg4  16554  usgredg2vlem2  16562  usgredg2v  16563  ushgredgedg  16565  ushgredgedgloop  16567  usgrstrrepeen  16570  usgr0e  16571  uhgr0v0e  16573  uspgr1edc  16579  usgr1e  16580  griedg0ssusgr  16590  subgrprop3  16601  subgruhgredgdm  16609  subuhgr  16611  subupgr  16612  subumgr  16613  subusgr  16614  uhgrspansubgrlem  16615  1loopgrvd2fi  16644  1loopgrvd0fi  16645  1hevtxdg0fi  16646  vdegp1aid  16653  vdegp1bid  16654  wlkm  16678  wlkvtxiedg  16684  wlkvtxiedgg  16685  wlkeq  16693  wlk1walkdom  16698  uspgr2wlkeq  16704  uspgr2wlkeqi  16706  upgr2wlkdc  16716  wlkres  16718  trlreslem  16728  clwwlkccatlem  16739  clwwlkn1loopb  16759  clwwlkext2edg  16761  clwwlknonex2lem1  16776  clwwlknonex2  16778  trlsegvdeglem2  16800  trlsegvdeglem3  16801  eupth2lem3lem4fi  16812  eupth2lemsfi  16817  fnmptd  16930  bj-sels  17038  bj-nnelon  17083  pw1map  17123  pwle2  17126  pwf1oexmid  17127  pw1nct  17131  stnot  17137  nninfall  17150  nninfsellemdc  17151  nninfself  17154  nnnninfex  17163  nninfnfiinf  17164  refeq  17171  isomninnlem  17177  cvgcmp2nlemabs  17179  trilpolemlt1  17188  trirec0  17191  apdifflemf  17193  apdifflemr  17194  apdiff  17195  qdiff  17196  iswomninnlem  17197  iswomni0  17199  ismkvnnlem  17200  reap0  17206  cndcap  17207