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  ofrfidc  7318  2omap  7319  supelti  7343  supsnti  7346  cnvinfex  7359  ordiso2  7376  updjud  7423  djudom  7434  difinfsn  7441  ctssdc  7454  enumctlemm  7455  enumct  7456  nninfninc  7464  enomnilem  7479  fodjuf  7486  ismkvnex  7496  omnimkv  7497  enmkvlem  7502  enwomnilem  7510  nninfdcinf  7512  nninfwlporlem  7514  isnumi  7528  exmidfodomrlemrALT  7556  finacn  7561  djudoml  7576  djudomr  7577  netap  7621  2omotaplemap  7624  2omotaplemst  7625  exmidapne  7627  cc2lem  7633  cc3  7635  ltsopi  7688  pitri3or  7690  ltdcpi  7691  indpi  7710  enqdc  7729  enqdc1  7730  addcmpblnq  7735  mulcanenq  7753  recrecnq  7762  nqtri3or  7764  ltdcnq  7765  ltsonq  7766  ltaddnq  7775  subhalfnqq  7782  archnqq  7785  prarloclemarch2  7787  enq0tr  7802  nqnq0  7809  addcmpblnq0  7811  mulcanenq0ec  7813  nnnq0lem1  7814  nqpnq0nq  7821  nq0m0r  7824  nq02m  7833  prarloclemlt  7861  prarloclemcalc  7870  addlocpr  7904  nqprl  7919  nqpru  7920  addnqprlemrl  7925  addnqprlemru  7926  prmuloclemcalc  7933  mullocprlem  7938  mulnqprlemrl  7941  mulnqprlemru  7942  1idprl  7958  1idpru  7959  ltaddpr  7965  ltexprlemm  7968  ltexprlemopl  7969  ltexprlemopu  7971  ltexprlemdisj  7974  ltexprlemrl  7978  ltexprlemru  7980  addcanprleml  7982  addcanprlemu  7983  addcanprg  7984  prplnqu  7988  recexprlemloc  7999  recexprlem1ssl  8001  recexprlem1ssu  8002  aptiprleml  8007  aptiprlemu  8008  archpr  8011  cauappcvgprlemm  8013  cauappcvgprlemopl  8014  cauappcvgprlemloc  8020  cauappcvgprlemladdfu  8022  cauappcvgprlemladdfl  8023  cauappcvgprlem1  8027  cauappcvgprlem2  8028  caucvgprlemnkj  8034  caucvgprlemopl  8037  caucvgprlemloc  8043  caucvgprlemladdfu  8045  caucvgprlem2  8048  caucvgprprlemnkltj  8057  caucvgprprlemopl  8065  caucvgprprlemloc  8071  caucvgprprlemexbt  8074  caucvgprprlemaddq  8076  caucvgprprlem2  8078  suplocexprlemmu  8086  suplocexprlemru  8087  suplocexprlemloc  8089  suplocexprlemlub  8092  prsrlem1  8110  0idsr  8135  1idsr  8136  recexgt0sr  8141  archsr  8150  prsradd  8154  caucvgsrlemcau  8161  caucvgsrlembound  8162  caucvgsrlemoffgt1  8167  suplocsrlemb  8174  suplocsrlempr  8175  suplocsrlem  8176  pitonnlem1p1  8214  pitonn  8216  pitoregt0  8217  peano2nnnn  8221  recidpirq  8226  axcaucvglemval  8265  leid  8410  nltled  8449  readdcan  8468  addneintrd  8516  addneintr2d  8517  pncan  8534  subsub2  8556  subsub4  8561  negned  8636  subne0d  8648  subneintrd  8683  subneintr2d  8685  subeq0bd  8708  subdi  8714  gt0add  8904  rimul  8916  rereim  8917  ltmul1a  8922  apreim  8934  apirr  8936  mulap0r  8946  msqge0  8947  mulge0  8950  gt0ap0  8957  ltap  8964  subap0d  8975  recexaplem2  8983  mulap0bad  8990  mulap0bbd  8991  mul0eqap  9003  divrecap  9021  div0ap  9035  div1  9036  recrecap  9042  divdivdivap  9046  ddcanap  9059  rerecclap  9063  div2negap  9068  diveqap1bd  9169  recgt0  9183  prodgt0  9185  lemul1a  9191  recp1lt1  9232  squeeze0  9237  peano2nn  9319  div4p1lem1div2  9564  arch  9565  peano2z  9685  peano2zm  9687  ztri3or  9692  nn0n0n1ge2  9720  zextle  9742  gtndiv  9746  suprzclex  9749  nn0ind-raph  9768  uzid  9946  uzneg  9951  uztric  9954  uz11  9955  eluzp1l  9957  qdivcl  10053  irrmul  10058  irrmulap  10059  rpnegap  10098  negelrpd  10100  ledivge1le  10138  mul2lt0rlt0  10171  mul2lt0rgt0  10172  nn0ledivnn  10179  ltpnf  10193  mnflt  10196  pnfge  10202  mnfle  10205  xrlttr  10208  xrltso  10209  xrlttri3  10210  xrleid  10213  xaddass2  10283  xltadd1  10289  xlt2add  10293  xleaddadd  10300  lincmble  10417  iccf1o  10418  fztri3or  10454  fznlem  10456  fzn  10457  fzsplit2  10466  fzsplit3  10469  fznatpl1  10494  uzsplit  10510  fseq1p1m1  10512  fzm1  10518  fznn0sub2  10546  difelfznle  10553  1fv  10557  fzodcel  10571  fzospliti  10596  fzouzsplit  10599  eluzgtdifelfzo  10626  exfzdc  10670  subfzo0  10672  zsupcllemstep  10673  zsupcl  10675  zssinfcl  10676  infssuzex  10677  infssuzcldc  10679  infssfzcldc  10680  infssfzledc  10681  suprzubdc  10682  nninfdcex  10683  qdcle  10692  exbtwnz  10696  qbtwnrelemcalc  10701  flqlelt  10723  flaplelt  10724  qfraclt1  10728  qfracge0  10729  flaplt  10733  flqltnz  10737  btwnzge0  10750  flhalf  10752  fldiv4lem1div2uz2  10756  ceiqle  10765  intfracq  10772  mulqmod0  10782  modqge0  10784  modqlt  10785  modqid  10801  modqid0  10802  m1modge3gt1  10823  modqltm1p1mod  10828  q2txmodxeq0  10836  modaddmodlo  10840  modsumfzodifsn  10848  addmodlteq  10850  frecuzrdgtcl  10864  frecuzrdgtclt  10873  uzennn  10888  uzsinds  10896  seqf  10916  seqf2  10920  monoord2  10938  iseqf1olemqk  10959  iseqf1olemjpcl  10960  iseqf1olemqpcl  10961  seq3f1olemqsumkj  10963  seq3f1olemqsum  10965  seq3f1olemstep  10966  seq3f1oleml  10968  seqf1oglem1  10971  ser3le  10989  exp3vallem  10992  exp3val  10993  expp1  10998  expcllem  11002  ltexp2a  11043  leexp2a  11044  resq01  11110  nn0ltexp2  11163  faclbnd  11195  faclbnd2  11196  faclbnd3  11197  bcval5  11217  bcpasc  11220  bcm1n  11223  hashennn  11235  fihasheqf1oi  11242  hashsng  11253  fihashfn  11256  hashun  11261  fihashss  11273  fihashssdif  11275  hashfz  11278  hashxp  11283  hashmap  11284  hashpwfi  11285  fimaxq  11286  sseqn  11295  hashfibclem  11298  hashf1lem2  11302  hashf1  11303  zfz1isolem1  11308  seq3coll  11310  hashdmprop2dom  11312  wrdf  11326  wrdlenge2n0  11356  fstwrdne0  11360  wrdred1hash  11364  ccatvalfn  11385  ccatsymb  11386  ccatlid  11390  ccatrid  11391  ccatrn  11393  ccatalpha  11397  eqs1  11412  ccats1val2  11424  fzowrddc  11435  swrdlen  11440  swrdnd  11447  swrd0g  11448  swrdfv2  11451  swrdwrdsymbg  11452  pfxn0  11476  pfxwrdsymbg  11478  pfxsuff1eqwrdeq  11487  swrdswrd  11493  ccats1pfxeq  11502  ccats1pfxeqrex  11503  wrdind  11510  wrd2ind  11511  swrdccatin1  11513  pfxccatin12lem4  11514  swrdccatin2  11517  pfxccatin12  11521  pfxccat3a  11526  swrdccat3blem  11527  pfxccatid  11529  swrdccatin2d  11532  shftfn  11605  cjth  11627  cjmulrcl  11668  sq01  11676  reim0bd  11726  rerebd  11727  cjrebd  11728  caucvgre  11763  cvg1nlemcxze  11764  cvg1nlemcau  11766  cvg1nlemres  11767  recvguniq  11777  resqrexlemover  11792  resqrexlemdec  11793  resqrexlemgt0  11802  resqrexlemoverl  11803  resqrexlemglsq  11804  rersqrtthlem  11812  sqrtgt0  11816  leabs  11856  absexpzap  11863  absle  11872  recvalap  11880  abstri  11887  abs2dif  11889  amgm2  11901  absne0d  11970  maxleim  11988  maxabslemab  11989  maxabslemlub  11990  maxltsup  12001  zmaxcl  12007  fimaxre2  12010  minmax  12014  rpmincl  12022  zmincl  12023  bdtrilem  12024  bdtri  12025  xrmaxleim  12029  xrmaxiflemcom  12034  xrmaxltsup  12043  xrmaxadd  12046  xrminmax  12050  xrminrpcl  12059  climconst  12075  climuni  12078  2clim  12086  climcn1  12093  climcn2  12094  reccn2ap  12098  climge0  12110  climle  12119  climsqz  12120  climsqz2  12121  serf0  12137  summodclem3  12166  summodclem2a  12167  fsumcl2lem  12184  sumpr  12199  sumtp  12200  fsum0diaglem  12226  mptfzshft  12228  fsumle  12249  fsumlt  12250  divcnv  12283  trireciplem  12286  expcnvap0  12288  expcnv  12290  explecnv  12291  geosergap  12292  cvgratnnlembern  12309  cvgratnnlemabsle  12313  cvgratnnlemsumlt  12314  cvgratz  12318  cvgratgt0  12319  mertenslemi1  12321  mertenslem2  12322  mertensabs  12323  clim2divap  12326  prodmodclem3  12361  prodmodclem2a  12362  fprodseq  12369  fprodmul  12377  fprodfac  12401  fprodconst  12406  fprodap0  12407  fprodap0f  12422  fprodle  12426  eftcl  12440  ef0lem  12446  efsub  12467  eftlub  12476  eflegeo  12487  tanval2ap  12499  sinadd  12522  cos2t  12536  cos2tsin  12537  sin01bnd  12543  cos01bnd  12544  eirraplem  12563  dvdsval2  12576  dvdsdc  12584  dvds0lem  12587  zdvdsdc  12598  dvdscmulr  12606  dvdsmulcr  12607  fsumdvds  12628  dvdslelemd  12629  divconjdvds  12635  dvdsext  12641  fzm1ndvds  12642  dvdsmod  12648  3dvds  12650  oexpneg  12663  2tp1odd  12670  mulsucdiv2z  12671  2teven  12673  zeo5  12674  opeo  12683  omeo  12684  nn0ob  12694  divalglemnqt  12706  bitsdc  12733  bits0o  12736  bitsfzolem  12740  bitsfzo  12741  bitsmod  12742  bitscmp  12744  bitsinv1lem  12747  gcddvds  12759  dvdslegcd  12760  gcdneg  12778  bezoutlemnewy  12792  bezoutlemstep  12793  bezoutlema  12795  bezoutlemb  12796  bezoutlemmo  12802  bezoutlemle  12804  bezoutlemsup  12805  dfgcd3  12806  bezout  12807  dfgcd2  12810  uzwodc  12833  lcmcllem  12864  lcmneg  12871  lcmgcdlem  12874  lcmdvds  12876  lcmid  12877  3lcm2e6woprm  12883  6lcm4e12  12884  ncoprmgcdne1b  12886  mulgcddvds  12891  divgcdcoprmex  12899  cncongr1  12900  cncongr2  12901  isprm2lem  12913  prmind2  12917  dvdsnprmd  12922  prm2orodd  12923  sqnprm  12934  isprm5lem  12939  rpexp  12951  sqrt2irrlem  12959  nnmaxpwlemparts  12971  sqrt2irraplemnn  12978  qnumdencoprm  12992  qeqnumdivden  12993  nn0gcdsq  12999  nn0sqrtelqelz  13005  nonsq  13006  sqrtrirr  13008  phicl2  13015  phibnd  13018  hashdvds  13022  phiprmpw  13023  phimullem  13026  eulerthlemrprm  13030  eulerthlema  13031  eulerthlemth  13033  prmdiveq  13037  hashgcdlem  13039  odzdvds  13047  modprminv  13051  nnnn0modprm0  13057  modprmn0modprm0  13058  pythagtriplem10  13071  pythagtriplem19  13084  pythagtrip  13085  pcpre1  13094  pcpremul  13095  pceu  13097  pcmul  13103  pcdiv  13104  pcqmul  13105  pcqdiv  13109  pcexp  13111  pcdvdsb  13122  pcidlem  13125  pcdvdstr  13129  pcgcd1  13130  pc2dvds  13132  pcprmpw2  13135  difsqpwdvds  13140  pcaddlem  13141  pcadd  13142  pcadd2  13143  pcmpt  13145  pcmptdvds  13147  pcprod  13148  fldivp1  13150  pcfaclem  13151  pcfac  13152  pcbc  13153  qexpz  13154  pockthlem  13158  pockthg  13159  1arithlem4  13168  1arith  13169  1arith2  13170  4sqlem6  13185  4sqlem8  13187  4sqlem9  13188  4sqlem10  13189  4sqexercise1  13200  4sqexercise2  13201  4sqlemsdc  13202  4sqlem11  13203  4sqlem12  13204  4sqlem15  13207  4sqlem16  13208  4sqlem17  13209  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilemimin  13301  ballotfilem1c  13303  ballotfilemro  13318  ballotfilemfrcn0  13325  znnen  13341  ennnfonelemk  13343  ennnfonelemkh  13355  ennnfonelemhf1o  13356  ennnfonelemrnh  13359  ennnfonelemfun  13360  ennnfonelemf1  13361  ennnfonelemrn  13362  ennnfonelemnn0  13365  ctinfomlemom  13370  ctiunctlemudc  13380  unct  13385  omctfn  13386  ssnnctlemct  13389  nninfdclemp1  13393  nninfdc  13396  structfung  13421  setsfun  13439  setsfun0  13440  setscom  13444  strslfv3  13450  setsslid  13455  imasaddfnlemg  13688  imasaddvallemg  13689  mgmsscl  13734  plusffng  13738  mgmplusf  13739  mgm0  13742  mgm1  13743  opifismgmdc  13744  gzsumfzval  13764  sgrp1  13779  issgrpd  13780  mndpfo  13804  mndfo  13805  mnd1  13815  0subm  13844  mhmima  13851  grpinvfng  13902  isgrpinv  13912  grpinvid  13918  grpinvf1o  13928  grpinvadd  13936  grpsubf  13937  grpsubsub4  13951  grplactcnv  13960  grp1  13964  grp1inv  13965  qusgrp2  13969  mulgfng  13980  subginv  14037  resgrpisgrp  14051  subgintm  14054  0subg  14055  0nsg  14070  qusinv  14092  ghminv  14106  ghmrn  14113  ghmeql  14123  ghmnsgima  14124  kerf1ghm  14130  conjnmz  14135  cntzval  14147  cntz2ss  14162  cntzsubg  14165  cntzmhm  14167  cntzmhm2  14168  gzsumshift  14233  gsumvalfi  14236  gzsumgsum  14239  gsumsncmn  14240  gsump1  14241  gsumf1ofi  14244  gsumsubmclfi  14247  prdsplusgsgrpcl  14274  prdsplusgcl  14276  prdsidlem  14277  prdsinvlem  14280  prdsinvgd  14282  pwsdiagel  14294  pwssnf1o  14295  rngass  14322  rngmneg1  14330  rngmneg2  14331  qusrng  14341  srgideu  14360  srgidmlem  14366  srgpcomp  14378  srg1expzeq1  14383  ringcl  14401  ringideu  14405  ringidmlem  14411  ringnegl  14440  ringnegr  14441  ring1  14448  qusring2  14455  opprringbg  14469  dvdsrd  14485  dvdsr01  14495  isunitd  14497  unitinvcl  14514  unitinvinv  14515  unitnegcl  14521  rhmmul  14555  rhmf1o  14559  nzrunit  14579  lringuplu  14587  subrngintm  14604  subrgsubm  14626  subrgintm  14635  rrgsupp  14658  ringunitap  14677  aprsym  14680  aprnzr  14683  aprlring  14684  drnglring  14691  drngunitap  14692  scaffng  14730  lmodscaf  14731  lsssn0  14791  lss1d  14804  lssintclm  14805  lspval  14811  lspcl  14812  lspsnid  14828  lspprid1  14832  lspsn  14837  sraval  14858  rspcl  14912  rspssid  14913  rspssp  14915  rnglidlmmgm  14917  rnglidlmsgrp  14918  cnfldneg  14994  zringinvg  15023  expghmap  15026  znzrhfo  15067  znf1o  15070  znhash  15075  znidomb  15077  znrrg  15079  psrbagfsupp  15139  psrbagfi  15143  psrbaglecl  15144  psrbagaddclfi  15145  psrbagcon  15146  psrbaglefifi  15147  psraddcl  15156  psrmulclfilem  15161  psr0cl  15163  psrnegcl  15165  psrneg  15169  psr1clfi  15170  mplsubgfilemm  15180  mplsubgfilemcl  15181  baspartn  15242  eltg3i  15248  tgclb  15257  topbas  15259  2basgeng  15274  topcld  15301  0cld  15304  uncld  15305  neif  15333  elnei  15344  0nei  15358  restbasg  15360  iscnp4  15410  cnpnei  15411  cnclima  15415  cncnp  15422  cnrest2r  15429  cndis  15433  lmff  15441  lmtopcnp  15442  txbas  15450  txopn  15457  txcnp  15463  upxp  15464  txdis1cn  15470  cnmpt11  15475  cnmpt21  15483  psmetge0  15523  xmetge0  15557  xmettpos  15562  xmetrtri  15568  metrtri  15569  xblpnfps  15590  xblpnf  15591  blfps  15601  blf  15602  ssblps  15617  ssbl  15618  blbas  15625  metss2  15690  xmettxlem  15701  xmettx  15702  qtopbas  15714  divcnap  15757  cncfss  15775  cdivcncfap  15796  expcncf  15801  cnopnap  15803  maxcncf  15807  mincncf  15808  dedekindeulemuub  15809  dedekindeulemlu  15813  dedekindeu  15815  suplociccex  15817  dedekindicclemuub  15818  dedekindicclemlu  15822  dedekindicclemicc  15824  ivthinclemlopn  15828  ivthinclemuopn  15830  ivthinc  15835  ivthreinc  15837  hoverlt1  15841  ellimc3apf  15852  limcimolemlt  15856  limcimo  15857  limcresi  15858  cnplimclemle  15860  reldvg  15871  dvfgg  15880  dvidlemap  15883  dvidrelem  15884  dvidsslem  15885  dvcjbr  15900  dvcj  15901  dvrecap  15905  dveflem  15918  dvef  15919  elply2  15927  elplyr  15932  plycj  15953  plyreres  15956  reeff1oleme  15964  efap1p  15971  pilem3  15976  sinq34lt0t  16024  cosq14gt0  16025  coseq0q4123  16027  tangtx  16031  sincosq1eq  16032  cosordlem  16042  logdivlti  16075  logdivlt  16088  relogbval  16148  relogbzcl  16149  nnlogbexp  16156  logbgcd1irr  16164  logbgcd1irraplemexp  16165  logbgcd1irraplemap  16166  zprmlogbaplem2  16177  zprmlogbap  16179  birthdaylem2  16187  birthdaylem3  16188  pellexlem1  16190  pellexlem3  16192  wilthlem1  16193  efchtqdvds  16226  ppiqwordi  16229  ppiqeq0  16241  mpodvdsmulf1o  16245  ppiqub  16254  chtqleppi  16255  chtublem  16256  chtqub  16257  mersenne  16258  perfectlem2  16261  perfect  16262  bcmono  16265  bcmax  16266  bposlem1  16272  bposlem2  16273  bposlem3  16274  bposlem6  16277  bposlem7  16278  bposlem9  16280  zabsle1  16284  lgslem1  16285  lgsval  16289  lgsfvalg  16290  lgsfcl2  16291  lgsval2lem  16295  lgscl1  16308  lgsmod  16311  lgsdir2lem5  16317  lgsdir2  16318  lgsdilem2  16321  lgsdi  16322  lgsne0  16323  gausslemma2dlem0c  16336  gausslemma2dlem0h  16341  gausslemma2dlem1a  16343  gausslemma2dlem1f1o  16345  gausslemma2dlem3  16348  lgseisenlem1  16355  lgseisenlem2  16356  lgseisenlem3  16357  lgseisenlem4  16358  lgseisen  16359  lgsquadlem1  16362  lgsquadlem2  16363  lgsquadlem3  16364  lgsquad3  16369  2lgslem3b1  16383  2lgslem3c1  16384  2lgs  16389  2lgsoddprmlem2  16391  2lgsoddprm  16398  2sqlem3  16402  2sqlem8  16408  2sqlem10  16410  structgrssvtx  16449  structgrssiedg  16450  ushgruhgr  16487  uhgrun  16493  incistruhgr  16497  upgrop  16511  upgruhgr  16518  umgrupgr  16519  umgrnloopv  16521  umgredgprv  16522  umgr0e  16525  upgr1edc  16528  umgr1een  16532  upgrun  16533  umgrun  16535  umgrislfupgrdom  16538  upgredg  16551  umgrpredgv  16554  usgrop  16573  usgrausgrien  16576  ausgrumgrien  16577  ausgrusgrien  16578  uspgrupgrushgr  16589  usgrumgr  16591  usgrumgruspgr  16592  usgruspgrben  16593  usgrislfuspgrdom  16597  edgssv2en  16606  usgrf1oedg  16612  usgredg4  16622  usgredg2vlem2  16630  usgredg2v  16631  ushgredgedg  16633  ushgredgedgloop  16635  usgrstrrepeen  16638  usgr0e  16639  uhgr0v0e  16641  uspgr1edc  16647  usgr1e  16648  griedg0ssusgr  16658  subgrprop3  16669  subgruhgredgdm  16677  subuhgr  16679  subupgr  16680  subumgr  16681  subusgr  16682  uhgrspansubgrlem  16683  1loopgrvd2fi  16712  1loopgrvd0fi  16713  1hevtxdg0fi  16714  vdegp1aid  16721  vdegp1bid  16722  wlkm  16746  wlkvtxiedg  16752  wlkvtxiedgg  16753  wlkeq  16761  wlk1walkdom  16766  uspgr2wlkeq  16772  uspgr2wlkeqi  16774  upgr2wlkdc  16784  wlkres  16786  trlreslem  16796  clwwlkccatlem  16807  clwwlkn1loopb  16827  clwwlkext2edg  16829  clwwlknonex2lem1  16844  clwwlknonex2  16846  trlsegvdeglem2  16868  trlsegvdeglem3  16869  eupth2lem3lem4fi  16880  eupth2lemsfi  16885  fnmptd  16998  bj-sels  17106  bj-nnelon  17151  pw1map  17191  pwle2  17194  pwf1oexmid  17195  pw1nct  17199  stnot  17205  nninfall  17218  nninfsellemdc  17219  nninfself  17222  nnnninfex  17231  nninfnfiinf  17232  refeq  17239  isomninnlem  17245  cvgcmp2nlemabs  17247  trilpolemlt1  17257  trirec0  17260  apdifflemf  17262  apdifflemr  17263  apdiff  17264  qdiff  17265  iswomninnlem  17266  iswomni0  17268  ismkvnnlem  17269  reap0  17275  cndcap  17276