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  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  flqltnz  10736  btwnzge0  10749  flhalf  10751  fldiv4lem1div2uz2  10755  ceiqle  10764  intfracq  10771  mulqmod0  10781  modqge0  10783  modqlt  10784  modqid  10800  modqid0  10801  m1modge3gt1  10822  modqltm1p1mod  10827  q2txmodxeq0  10835  modaddmodlo  10839  modsumfzodifsn  10847  addmodlteq  10849  frecuzrdgtcl  10863  frecuzrdgtclt  10872  uzennn  10887  uzsinds  10895  seqf  10915  seqf2  10919  monoord2  10937  iseqf1olemqk  10958  iseqf1olemjpcl  10959  iseqf1olemqpcl  10960  seq3f1olemqsumkj  10962  seq3f1olemqsum  10964  seq3f1olemstep  10965  seq3f1oleml  10967  seqf1oglem1  10970  ser3le  10988  exp3vallem  10991  exp3val  10992  expp1  10997  expcllem  11001  ltexp2a  11042  leexp2a  11043  resq01  11109  nn0ltexp2  11162  faclbnd  11194  faclbnd2  11195  faclbnd3  11196  bcval5  11216  bcpasc  11219  bcm1n  11222  hashennn  11234  fihasheqf1oi  11241  hashsng  11252  fihashfn  11255  hashun  11260  fihashss  11272  fihashssdif  11274  hashfz  11277  hashxp  11282  hashmap  11283  hashpwfi  11284  fimaxq  11285  sseqn  11294  hashfibclem  11297  hashf1lem2  11301  hashf1  11302  zfz1isolem1  11307  seq3coll  11309  hashdmprop2dom  11311  wrdf  11325  wrdlenge2n0  11355  fstwrdne0  11359  wrdred1hash  11363  ccatvalfn  11384  ccatsymb  11385  ccatlid  11389  ccatrid  11390  ccatrn  11392  ccatalpha  11396  eqs1  11411  ccats1val2  11423  fzowrddc  11434  swrdlen  11439  swrdnd  11446  swrd0g  11447  swrdfv2  11450  swrdwrdsymbg  11451  pfxn0  11475  pfxwrdsymbg  11477  pfxsuff1eqwrdeq  11486  swrdswrd  11492  ccats1pfxeq  11501  ccats1pfxeqrex  11502  wrdind  11509  wrd2ind  11510  swrdccatin1  11512  pfxccatin12lem4  11513  swrdccatin2  11516  pfxccatin12  11520  pfxccat3a  11525  swrdccat3blem  11526  pfxccatid  11528  swrdccatin2d  11531  shftfn  11604  cjth  11626  cjmulrcl  11667  sq01  11675  reim0bd  11725  rerebd  11726  cjrebd  11727  caucvgre  11762  cvg1nlemcxze  11763  cvg1nlemcau  11765  cvg1nlemres  11766  recvguniq  11776  resqrexlemover  11791  resqrexlemdec  11792  resqrexlemgt0  11801  resqrexlemoverl  11802  resqrexlemglsq  11803  rersqrtthlem  11811  sqrtgt0  11815  leabs  11855  absexpzap  11862  absle  11871  recvalap  11879  abstri  11886  abs2dif  11888  amgm2  11900  absne0d  11969  maxleim  11987  maxabslemab  11988  maxabslemlub  11989  maxltsup  12000  zmaxcl  12006  fimaxre2  12009  minmax  12013  rpmincl  12021  zmincl  12022  bdtrilem  12023  bdtri  12024  xrmaxleim  12028  xrmaxiflemcom  12033  xrmaxltsup  12042  xrmaxadd  12045  xrminmax  12049  xrminrpcl  12058  climconst  12074  climuni  12077  2clim  12085  climcn1  12092  climcn2  12093  reccn2ap  12097  climge0  12109  climle  12118  climsqz  12119  climsqz2  12120  serf0  12136  summodclem3  12165  summodclem2a  12166  fsumcl2lem  12183  sumpr  12198  sumtp  12199  fsum0diaglem  12225  mptfzshft  12227  fsumle  12248  fsumlt  12249  divcnv  12282  trireciplem  12285  expcnvap0  12287  expcnv  12289  explecnv  12290  geosergap  12291  cvgratnnlembern  12308  cvgratnnlemabsle  12312  cvgratnnlemsumlt  12313  cvgratz  12317  cvgratgt0  12318  mertenslemi1  12320  mertenslem2  12321  mertensabs  12322  clim2divap  12325  prodmodclem3  12360  prodmodclem2a  12361  fprodseq  12368  fprodmul  12376  fprodfac  12400  fprodconst  12405  fprodap0  12406  fprodap0f  12421  fprodle  12425  eftcl  12439  ef0lem  12445  efsub  12466  eftlub  12475  eflegeo  12486  tanval2ap  12498  sinadd  12521  cos2t  12535  cos2tsin  12536  sin01bnd  12542  cos01bnd  12543  eirraplem  12562  dvdsval2  12575  dvdsdc  12583  dvds0lem  12586  zdvdsdc  12597  dvdscmulr  12605  dvdsmulcr  12606  fsumdvds  12627  dvdslelemd  12628  divconjdvds  12634  dvdsext  12640  fzm1ndvds  12641  dvdsmod  12647  3dvds  12649  oexpneg  12662  2tp1odd  12669  mulsucdiv2z  12670  2teven  12672  zeo5  12673  opeo  12682  omeo  12683  nn0ob  12693  divalglemnqt  12705  bitsdc  12732  bits0o  12735  bitsfzolem  12739  bitsfzo  12740  bitsmod  12741  bitscmp  12743  bitsinv1lem  12746  gcddvds  12758  dvdslegcd  12759  gcdneg  12777  bezoutlemnewy  12791  bezoutlemstep  12792  bezoutlema  12794  bezoutlemb  12795  bezoutlemmo  12801  bezoutlemle  12803  bezoutlemsup  12804  dfgcd3  12805  bezout  12806  dfgcd2  12809  uzwodc  12832  lcmcllem  12863  lcmneg  12870  lcmgcdlem  12873  lcmdvds  12875  lcmid  12876  3lcm2e6woprm  12882  6lcm4e12  12883  ncoprmgcdne1b  12885  mulgcddvds  12890  divgcdcoprmex  12898  cncongr1  12899  cncongr2  12900  isprm2lem  12912  prmind2  12916  dvdsnprmd  12921  prm2orodd  12922  sqnprm  12933  isprm5lem  12938  rpexp  12950  sqrt2irrlem  12958  nnmaxpwlemparts  12970  sqrt2irraplemnn  12977  qnumdencoprm  12991  qeqnumdivden  12992  nn0gcdsq  12998  nn0sqrtelqelz  13004  nonsq  13005  sqrtrirr  13007  phicl2  13014  phibnd  13017  hashdvds  13021  phiprmpw  13022  phimullem  13025  eulerthlemrprm  13029  eulerthlema  13030  eulerthlemth  13032  prmdiveq  13036  hashgcdlem  13038  odzdvds  13046  modprminv  13050  nnnn0modprm0  13056  modprmn0modprm0  13057  pythagtriplem10  13070  pythagtriplem19  13083  pythagtrip  13084  pcpre1  13093  pcpremul  13094  pceu  13096  pcmul  13102  pcdiv  13103  pcqmul  13104  pcqdiv  13108  pcexp  13110  pcdvdsb  13121  pcidlem  13124  pcdvdstr  13128  pcgcd1  13129  pc2dvds  13131  pcprmpw2  13134  difsqpwdvds  13139  pcaddlem  13140  pcadd  13141  pcadd2  13142  pcmpt  13144  pcmptdvds  13146  pcprod  13147  fldivp1  13149  pcfaclem  13150  pcfac  13151  pcbc  13152  qexpz  13153  pockthlem  13157  pockthg  13158  1arithlem4  13167  1arith  13168  1arith2  13169  4sqlem6  13184  4sqlem8  13186  4sqlem9  13187  4sqlem10  13188  4sqexercise1  13199  4sqexercise2  13200  4sqlemsdc  13201  4sqlem11  13202  4sqlem12  13203  4sqlem15  13206  4sqlem16  13207  4sqlem17  13208  ballotfilemfc0  13283  ballotfilemfcc  13284  ballotfilemimin  13300  ballotfilem1c  13302  ballotfilemro  13317  ballotfilemfrcn0  13324  znnen  13340  ennnfonelemk  13342  ennnfonelemkh  13354  ennnfonelemhf1o  13355  ennnfonelemrnh  13358  ennnfonelemfun  13359  ennnfonelemf1  13360  ennnfonelemrn  13361  ennnfonelemnn0  13364  ctinfomlemom  13369  ctiunctlemudc  13379  unct  13384  omctfn  13385  ssnnctlemct  13388  nninfdclemp1  13392  nninfdc  13395  structfung  13420  setsfun  13438  setsfun0  13439  setscom  13443  strslfv3  13449  setsslid  13454  imasaddfnlemg  13686  imasaddvallemg  13687  mgmsscl  13732  plusffng  13736  mgmplusf  13737  mgm0  13740  mgm1  13741  opifismgmdc  13742  gzsumfzval  13762  sgrp1  13777  issgrpd  13778  mndpfo  13802  mndfo  13803  mnd1  13813  0subm  13842  mhmima  13849  grpinvfng  13900  isgrpinv  13910  grpinvid  13916  grpinvf1o  13926  grpinvadd  13934  grpsubf  13935  grpsubsub4  13949  grplactcnv  13958  grp1  13962  grp1inv  13963  qusgrp2  13967  mulgfng  13978  subginv  14035  resgrpisgrp  14049  subgintm  14052  0subg  14053  0nsg  14068  qusinv  14090  ghminv  14104  ghmrn  14111  ghmeql  14121  ghmnsgima  14122  kerf1ghm  14128  conjnmz  14133  gzsumshift  14200  gsumvalfi  14203  gzsumgsum  14206  gsumsncmn  14207  gsump1  14208  gsumf1ofi  14211  gsumsubmclfi  14214  prdsplusgsgrpcl  14241  prdsplusgcl  14243  prdsidlem  14244  prdsinvlem  14247  prdsinvgd  14249  pwsdiagel  14261  pwssnf1o  14262  rngass  14289  rngmneg1  14297  rngmneg2  14298  qusrng  14308  srgideu  14327  srgidmlem  14333  srgpcomp  14345  srg1expzeq1  14350  ringcl  14368  ringideu  14372  ringidmlem  14378  ringnegl  14407  ringnegr  14408  ring1  14415  qusring2  14422  opprringbg  14436  dvdsrd  14452  dvdsr01  14462  isunitd  14464  unitinvcl  14481  unitinvinv  14482  unitnegcl  14488  rhmmul  14522  rhmf1o  14526  nzrunit  14546  lringuplu  14554  subrngintm  14571  subrgsubm  14593  subrgintm  14602  rrgsupp  14625  ringunitap  14644  aprsym  14647  aprnzr  14650  aprlring  14651  drnglring  14658  drngunitap  14659  scaffng  14697  lmodscaf  14698  lsssn0  14758  lss1d  14771  lssintclm  14772  lspval  14778  lspcl  14779  lspsnid  14795  lspprid1  14799  lspsn  14804  sraval  14825  rspcl  14879  rspssid  14880  rspssp  14882  rnglidlmmgm  14884  rnglidlmsgrp  14885  cnfldneg  14961  zringinvg  14990  expghmap  14993  znzrhfo  15034  znf1o  15037  znhash  15042  znidomb  15044  znrrg  15046  psrbagfsupp  15106  psrbagfi  15110  psrbaglecl  15111  psrbagaddclfi  15112  psrbagcon  15113  psrbaglefifi  15114  psraddcl  15123  psr0cl  15124  psrnegcl  15126  psrneg  15130  psr1clfi  15131  mplsubgfilemm  15141  mplsubgfilemcl  15142  baspartn  15203  eltg3i  15209  tgclb  15218  topbas  15220  2basgeng  15235  topcld  15262  0cld  15265  uncld  15266  neif  15294  elnei  15305  0nei  15319  restbasg  15321  iscnp4  15371  cnpnei  15372  cnclima  15376  cncnp  15383  cnrest2r  15390  cndis  15394  lmff  15402  lmtopcnp  15403  txbas  15411  txopn  15418  txcnp  15424  upxp  15425  txdis1cn  15431  cnmpt11  15436  cnmpt21  15444  psmetge0  15484  xmetge0  15518  xmettpos  15523  xmetrtri  15529  metrtri  15530  xblpnfps  15551  xblpnf  15552  blfps  15562  blf  15563  ssblps  15578  ssbl  15579  blbas  15586  metss2  15651  xmettxlem  15662  xmettx  15663  qtopbas  15675  divcnap  15718  cncfss  15736  cdivcncfap  15757  expcncf  15762  cnopnap  15764  maxcncf  15768  mincncf  15769  dedekindeulemuub  15770  dedekindeulemlu  15774  dedekindeu  15776  suplociccex  15778  dedekindicclemuub  15779  dedekindicclemlu  15783  dedekindicclemicc  15785  ivthinclemlopn  15789  ivthinclemuopn  15791  ivthinc  15796  ivthreinc  15798  hoverlt1  15802  ellimc3apf  15813  limcimolemlt  15817  limcimo  15818  limcresi  15819  cnplimclemle  15821  reldvg  15832  dvfgg  15841  dvidlemap  15844  dvidrelem  15845  dvidsslem  15846  dvcjbr  15861  dvcj  15862  dvrecap  15866  dveflem  15879  dvef  15880  elply2  15888  elplyr  15893  plycj  15914  plyreres  15917  reeff1oleme  15925  efap1p  15932  pilem3  15937  sinq34lt0t  15985  cosq14gt0  15986  coseq0q4123  15988  tangtx  15992  sincosq1eq  15993  cosordlem  16003  logdivlti  16036  logdivlt  16049  relogbval  16109  relogbzcl  16110  nnlogbexp  16117  logbgcd1irr  16125  logbgcd1irraplemexp  16126  logbgcd1irraplemap  16127  zprmlogbaplem2  16138  zprmlogbap  16140  birthdaylem2  16148  birthdaylem3  16149  pellexlem1  16151  pellexlem3  16153  wilthlem1  16154  efchtqdvds  16187  ppiqwordi  16190  ppiqeq0  16202  mpodvdsmulf1o  16206  ppiqub  16215  chtqleppi  16216  chtublem  16217  chtqub  16218  mersenne  16219  perfectlem2  16222  perfect  16223  bcmono  16226  bcmax  16227  bposlem1  16233  bposlem2  16234  bposlem3  16235  zabsle1  16240  lgslem1  16241  lgsval  16245  lgsfvalg  16246  lgsfcl2  16247  lgsval2lem  16251  lgscl1  16264  lgsmod  16267  lgsdir2lem5  16273  lgsdir2  16274  lgsdilem2  16277  lgsdi  16278  lgsne0  16279  gausslemma2dlem0c  16292  gausslemma2dlem0h  16297  gausslemma2dlem1a  16299  gausslemma2dlem1f1o  16301  gausslemma2dlem3  16304  lgseisenlem1  16311  lgseisenlem2  16312  lgseisenlem3  16313  lgseisenlem4  16314  lgseisen  16315  lgsquadlem1  16318  lgsquadlem2  16319  lgsquadlem3  16320  lgsquad3  16325  2lgslem3b1  16339  2lgslem3c1  16340  2lgs  16345  2lgsoddprmlem2  16347  2lgsoddprm  16354  2sqlem3  16358  2sqlem8  16364  2sqlem10  16366  structgrssvtx  16405  structgrssiedg  16406  ushgruhgr  16443  uhgrun  16449  incistruhgr  16453  upgrop  16467  upgruhgr  16474  umgrupgr  16475  umgrnloopv  16477  umgredgprv  16478  umgr0e  16481  upgr1edc  16484  umgr1een  16488  upgrun  16489  umgrun  16491  umgrislfupgrdom  16494  upgredg  16507  umgrpredgv  16510  usgrop  16529  usgrausgrien  16532  ausgrumgrien  16533  ausgrusgrien  16534  uspgrupgrushgr  16545  usgrumgr  16547  usgrumgruspgr  16548  usgruspgrben  16549  usgrislfuspgrdom  16553  edgssv2en  16562  usgrf1oedg  16568  usgredg4  16578  usgredg2vlem2  16586  usgredg2v  16587  ushgredgedg  16589  ushgredgedgloop  16591  usgrstrrepeen  16594  usgr0e  16595  uhgr0v0e  16597  uspgr1edc  16603  usgr1e  16604  griedg0ssusgr  16614  subgrprop3  16625  subgruhgredgdm  16633  subuhgr  16635  subupgr  16636  subumgr  16637  subusgr  16638  uhgrspansubgrlem  16639  1loopgrvd2fi  16668  1loopgrvd0fi  16669  1hevtxdg0fi  16670  vdegp1aid  16677  vdegp1bid  16678  wlkm  16702  wlkvtxiedg  16708  wlkvtxiedgg  16709  wlkeq  16717  wlk1walkdom  16722  uspgr2wlkeq  16728  uspgr2wlkeqi  16730  upgr2wlkdc  16740  wlkres  16742  trlreslem  16752  clwwlkccatlem  16763  clwwlkn1loopb  16783  clwwlkext2edg  16785  clwwlknonex2lem1  16800  clwwlknonex2  16802  trlsegvdeglem2  16824  trlsegvdeglem3  16825  eupth2lem3lem4fi  16836  eupth2lemsfi  16841  fnmptd  16954  bj-sels  17062  bj-nnelon  17107  pw1map  17147  pwle2  17150  pwf1oexmid  17151  pw1nct  17155  stnot  17161  nninfall  17174  nninfsellemdc  17175  nninfself  17178  nnnninfex  17187  nninfnfiinf  17188  refeq  17195  isomninnlem  17201  cvgcmp2nlemabs  17203  trilpolemlt1  17212  trirec0  17215  apdifflemf  17217  apdifflemr  17218  apdiff  17219  qdiff  17220  iswomninnlem  17221  iswomni0  17223  ismkvnnlem  17224  reap0  17230  cndcap  17231