Theorem sylanbrc 583

Description: Syllogism inference. (Contributed by Jeff Madsen, 2-Sep-2009.)

Hypotheses

Ref	Expression
sylanbrc.1	⊢ (𝜑 → 𝜓)
sylanbrc.2	⊢ (𝜑 → 𝜒)
sylanbrc.3	⊢ (𝜃 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
sylanbrc	⊢ (𝜑 → 𝜃)

Proof of Theorem sylanbrc

Step	Hyp	Ref	Expression
1		sylanbrc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		sylanbrc.2	. . 3 ⊢ (𝜑 → 𝜒)
3	1, 2	jca 512	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		sylanbrc.3	. 2 ⊢ (𝜃 ↔ (𝜓 ∧ 𝜒))
5	3, 4	sylibr 233	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 397

This theorem is referenced by:  sylanblrc  590  ifpimpda  1080  ecase23d  1472  raleqbidvv  3339  elrabd  3627  eqeu  3642  euind  3660  reuind  3689  eldifd  3899  eqssd  3939  ssrabdv  4008  psstr  4040  elind  4129  elpwdifsn  4723  prproe  4838  propeqop  5422  issod  5537  wereu  5586  wereu2  5587  relssdmrn  6176  predtrss  6229  ordelord  6292  funun  6487  fnsng  6493  fnprg  6500  fntpg  6501  fununi  6516  fncoOLD  6559  f00  6665  f1ss  6685  f1ssr  6686  f1ssres  6687  focofo  6710  f1f1orn  6736  foimacnv  6742  foun  6743  f1oprswap  6769  rescnvimafod  6960  fvn0ssdmfun  6961  dff3  6985  fmpt  6993  ffnfv  7001  fmpt2d  7006  ffvresb  7007  fprb  7078  fpr2g  7096  nvof1o  7161  fcof1  7168  fcofo  7169  fcof1od  7175  fliftf  7195  soisores  7207  soisoi  7208  isoini2  7219  f1oiso  7231  moriotass  7274  fnoprabg  7406  f1ocnvd  7529  fiun  7794  f1iun  7795  1stcof  7870  2ndcof  7871  1stconst  7949  2ndconst  7950  curry1  7953  curry2  7956  fo2ndf  7971  f1o2ndf1  7972  soxp  7979  wexp  7980  fnwelem  7981  suppssov1  8023  suppssfv  8027  fpr1  8128  wfrlem10OLD  8158  smores2  8194  smo11  8204  smoiso2  8209  tfrlem12  8229  tfrlem13  8230  oalimcl  8400  oaf1o  8403  omlimcl  8418  omeu  8425  oeeulem  8441  oeeui  8442  omsmo  8497  eroveu  8610  fsetfocdm  8658  undifixp  8731  resixpfo  8733  elixpsn  8734  dom2lem  8789  difsnen  8849  omxpenlem  8869  sucdom2OLD  8878  sdomdomtr  8906  domsdomtr  8908  fodomr  8924  xpf1o  8935  ssfi  8965  sdomdomtrfi  8996  domsdomtrfi  8997  sucdom2  8998  php2  9003  php3  9004  phpeqd  9007  php2OLD  9015  php3OLD  9016  phpeqdOLD  9017  unxpdomlem3  9038  f1finf1o  9055  frfi  9068  wofi  9072  nnsdomg  9082  domunfican  9096  fofinf1o  9103  mapfienlem3  9175  mapfien  9176  marypha1lem  9201  supeu  9222  infeu  9264  ordtypelem2  9287  ordtypelem4  9289  ordtypelem10  9295  oismo  9308  wemaplem2  9315  card2inf  9323  brwdom2  9341  wdom2d  9348  harwdom  9359  cantnfp1lem2  9446  cantnfp1lem3  9447  cantnflem1  9456  cantnflem2  9457  cantnf  9460  cnfcom2lem  9468  cnfcom3lem  9470  ttrcltr  9483  frr1  9526  tskwe  9717  cardsdomelir  9740  cardprclem  9746  cardmin2  9766  en2other2  9774  r0weon  9777  infxpenc  9783  fseqenlem1  9789  fseqenlem2  9790  fodomacn  9821  infpwfien  9827  finnisoeu  9878  iunfictbso  9879  dfac12lem2  9909  cofsmo  10034  cfsmolem  10035  alephsing  10041  sornom  10042  infpssrlem3  10070  infpssrlem5  10072  ssfin4  10075  isfin4p1  10080  fincssdom  10088  fin23lem23  10091  fin23lem28  10105  fin23lem31  10108  fin23lem34  10111  isf32lem9  10126  compssiso  10139  fin1a2lem12  10176  hsmexlem1  10191  hsmexlem4  10194  domtriomlem  10207  cardmin  10329  smobeth  10351  gchen1  10390  gchen2  10391  fpwwe2lem10  10405  fpwwe2lem11  10406  fpwwe2lem12  10407  fpwwe2  10408  canthnum  10414  canthwe  10416  canthp1lem2  10418  canthp1  10419  pwfseqlem5  10428  gchdjuidm  10433  gchxpidm  10434  gchhar  10444  r1wunlim  10502  inar1  10540  inatsk  10543  r1tskina  10547  gruiun  10564  gruima  10567  gruina  10583  addclpi  10657  mulclpi  10658  nqereu  10694  dmrecnq  10733  genpcl  10773  suplem1pr  10817  receu  11629  recgt0  11830  cju  11978  peano5nni  11985  nn0n0n1ge2  12309  nn0ge2m1nn  12311  nnnegz  12331  elnnz  12338  nnssz  12349  msqznn  12411  eluzaddi  12620  eluzsubi  12621  uz2mulcl  12675  elq  12699  nnrp  12750  rpaddcl  12761  rpmulcl  12762  rpdivcl  12764  rpgecl  12767  ge0p1rp  12770  elrpd  12778  nn0rp0  13196  ge0addcl  13201  ge0mulcl  13202  ge0xaddcl  13203  ge0xmulcl  13204  icoshftf1o  13215  xnn0xrge0  13247  peano2fzr  13278  uzsubsubfz  13287  fzsplit2  13290  elfznn  13294  fzss1  13304  fzss2  13305  fzp1elp1  13318  elfz1b  13334  elfz0fzfz0  13370  fz0fzelfz0  13371  difelfznle  13379  elfzofz  13412  prinfzo0  13435  nn0p1elfzo  13439  fzosplitsnm1  13471  ubmelm1fzo  13492  fzofzp1b  13494  elfznelfzo  13501  fzosplitsn  13504  injresinj  13517  flge0nn0  13549  flge1nn  13550  zmodcl  13620  modmuladdnn0  13644  modsumfzodifsn  13673  seqcl2  13750  seqf2  13751  seqfveq2  13754  monoord  13762  seqid2  13778  expcl2lem  13803  expclzlem  13815  zsqcl2  13865  bcval4  14030  bcn1  14036  bccl2  14046  hashnn0n0nn  14115  hashfun  14161  seqcoll  14187  ccatsymb  14296  ccatrn  14303  ccat2s1fvw  14358  ccat2s1fvwOLD  14359  swrds1  14388  swrdccat2  14391  swrdccatin2  14451  pfxccatin12lem2  14453  pfxccatin12lem3  14454  pfxccatin12  14455  pfxccat3  14456  pfxccat3a  14460  spllen  14476  splfv2a  14478  splval2  14479  repswswrd  14506  cshwidxmod  14525  cshwcsh2id  14550  pfx2  14669  2swrd2eqwrdeq  14675  wwlktovfo  14682  wwlktovf1o  14683  shftfn  14793  shftf  14799  sqrlem2  14964  sqrlem7  14969  resqreu  14973  sqrtneg  14988  nn0abscl  15033  nnabscl  15046  abs2dif  15053  sqreu  15081  limsupval2  15198  climuni  15270  2clim  15290  climcn2  15311  rlimdiv  15366  isercolllem2  15386  isercolllem3  15387  isercoll  15388  isercoll2  15389  iseralt  15405  summolem2a  15436  mptfzshft  15499  fsum0diag2  15504  fsumge0  15516  climcndslem1  15570  mertenslem1  15605  ntrivcvgmul  15623  prodmolem2a  15653  fprodser  15668  fprodeq0  15694  fprodge0  15712  binomrisefac  15761  eff2  15817  tanval  15846  rpnnen2lem9  15940  sqrt2irrlem  15966  fzo0dvdseq  16041  oexpneg  16063  oddge22np1  16067  evennn02n  16068  evennn2n  16069  nno  16100  divalglem5  16115  bitsfzolem  16150  bitsinv1lem  16157  bitsinv2  16159  bitsf1ocnv  16160  bitsinvp1  16165  sadcaddlem  16173  sadadd2lem  16175  sadadd3  16177  sadasslem  16186  sadeq  16188  gcdcllem3  16217  divgcdz  16227  sqgcd  16279  lcmneg  16317  lcmfunsnlem2lem2  16353  prmind2  16399  sqnprm  16416  isprm5  16421  isprm6  16428  qgt0numnn  16464  crth  16488  phimullem  16489  eulerthlem1  16491  eulerthlem2  16492  hashgcdlem  16498  oddprm  16520  pythagtriplem6  16531  pythagtriplem11  16535  pythagtriplem13  16537  pythagtriplem19  16543  iserodd  16545  pclem  16548  pcpremul  16553  pceu  16556  pc2dvds  16589  difsqpwdvds  16597  pcadd  16599  oddprmdvds  16613  pockthlem  16615  pockthg  16616  prmreclem3  16628  1arith  16637  4sqlem11  16665  4sqlem12  16666  4sqlem13  16667  4sqlem14  16668  4sqlem17  16671  vdwlem2  16692  vdwlem8  16698  vdwlem12  16702  ramtlecl  16710  ramub1lem1  16736  prmgaplem4  16764  prmgaplem7  16767  cshwshashlem2  16807  cshwrepswhash1  16813  imasaddfnlem  17248  imasaddflem  17250  imasvscafn  17257  imasvscaf  17259  isacs1i  17375  mreacs  17376  catideu  17393  invfun  17485  invf  17489  invf1o  17490  issubc3  17573  cofucl  17612  funcres2c  17626  ffthf1o  17644  fulloppc  17647  fthoppc  17648  ffthoppc  17649  idffth  17658  cofull  17659  cofth  17660  ressffth  17663  initoeu2lem2  17739  setcmon  17811  setcepi  17812  catciso  17835  fthestrcsetc  17876  fullestrcsetc  17877  embedsetcestrclem  17883  fthsetcestrc  17891  fullsetcestrc  17892  hofcllem  17985  hofcl  17986  yonedalem3  18007  yonffthlem  18009  yoniso  18012  poslubd  18140  lubun  18242  isacs5  18275  acsfiindd  18280  mreclatBAD  18290  psss  18307  cnvtsr  18315  mgmsscl  18340  gsumval2  18379  sgrp0  18391  sgrp1  18393  hashfinmndnn  18411  ismndd  18416  mndpfo  18417  mnd1  18435  mhmf1o  18449  0mhm  18467  resmhm  18468  resmhm2  18469  resmhm2b  18470  mhmco  18471  gsumvallem2  18481  frmdss2  18511  efmndmnd  18537  sgrp2nmndlem4  18576  isgrpd2e  18607  grpinvf1o  18654  grpinvnzcl  18656  dfgrp3  18683  grp1  18691  mhmmnd  18706  ghmgrp  18708  subgmulg  18778  issubg4  18783  0subg  18789  isnsg3  18797  nmzsubg  18802  ssnmz  18803  nmznsg  18805  0nsg  18806  nsgid  18807  ghmnsgima  18867  ghmnsgpreima  18868  ghmf1  18872  ghmf1o  18873  conjnmzb  18878  gicref  18896  gafo  18911  gaid  18914  subgga  18915  gass  18916  gasubg  18917  gastacl  18924  orbsta  18928  cntrsubgnsg  18956  invoppggim  18976  symgextf1  19038  symgextfo  19039  symgextf1o  19040  symgfixf1  19054  symgfixfo  19056  symgfixf1o  19057  f1omvdmvd  19060  pmtrprfv  19070  pmtrdifwrdel2  19103  psgneu  19123  psgnvalfi  19131  psgnfieu  19135  psgnprfval  19138  odf1  19178  dfod2  19180  odf1o1  19186  odf1o2  19187  odhash3  19190  sylow1lem2  19213  sylow2blem2  19235  sylow3lem1  19241  sylow3lem2  19242  pj1eu  19311  efglem  19331  efginvrel2  19342  efgsrel  19349  efgsp1  19352  efgsres  19353  efgredleme  19358  efgrelexlemb  19365  efgredeu  19367  efgcpbllemb  19370  isabld  19409  ghmcmn  19442  ghmabl  19443  invghm  19444  cntrabl  19453  torsubg  19464  prdsabld  19472  qusabl  19475  abl1  19476  iscygd  19496  iscygodd  19497  cycsubmcmn  19498  gsumval3a  19513  gsumval3eu  19514  gsumpt  19572  gsummptf1o  19573  dprdcntz  19620  dprdff  19624  dprdfcntz  19627  dprdfadd  19632  dprdlub  19638  dprd2dlem1  19653  dprd2da  19654  dmdprdpr  19661  dprdpr  19662  ablfacrp  19678  ablfac1eu  19685  pgpfaclem1  19693  pgpfaclem2  19694  ablfaclem3  19699  issimpgd  19705  prmgrpsimpgd  19726  ablsimpgprmd  19727  srgfcl  19760  srglmhm  19780  srgrmhm  19781  iscrngd  19834  ringsrg  19837  prdscrngd  19861  dvdsrmul  19899  1unit  19909  unitmulcl  19915  unitgrp  19918  unitabl  19919  unitnegcl  19932  rhmf1o  19985  rimgim  19989  rhmco  19990  kerf1ghm  19996  isdrng2  20010  isdrngd  20025  subrgcrng  20037  subrguss  20048  subrgunit  20051  issubdrg  20058  resrhm  20062  subdrgint  20080  primefld  20082  isabvd  20089  srngf1o  20123  issrngd  20130  lssneln0  20223  islmhm2  20309  lmhmf1o  20317  pwssplit1  20330  lmimgim  20336  lsslvec  20378  lspabs3  20392  lspsneq  20393  lspfixed  20399  lspexch  20400  lspsolvlem  20413  islbs3  20426  lbsextlem1  20429  lbsextlem3  20431  lbsextlem4  20432  rlmlvec  20485  lidlnz  20508  quscrng  20520  drnglpir  20533  drngnzr  20542  opprnzr  20545  ringelnzr  20546  subrgnzr  20548  0ringnnzr  20549  unitrrg  20573  domnrrg  20580  opprdomn  20581  drngdomn  20583  fldidomOLD  20586  fidomndrng  20588  cnfldfunALT  20619  xrs1mnd  20645  xrs10  20646  cnmsubglem  20670  gzrngunit  20673  zringunit  20697  prmirredlem  20703  expghm  20706  mulgghm2  20707  domnchr  20745  zncyg  20765  znf1o  20768  zntoslem  20773  znfld  20777  znidomb  20778  cygznlem3  20786  psgnghm  20794  pjfo  20931  frlmlvec  20977  frlmphl  20997  uvcf1  21008  frlmssuvc1  21010  frlmsslsp  21012  frlmup4  21017  lindff1  21036  lindfrn  21037  lsslindf  21046  lmimlbs  21052  indlcim  21056  lmimco  21060  isassad  21080  psrbagcon  21142  psrbagconOLD  21143  gsumbagdiaglemOLD  21150  gsumbagdiagOLD  21151  psrass1lemOLD  21152  gsumbagdiaglem  21153  gsumbagdiag  21154  psrass1lem  21155  psrbas  21156  psrcrng  21191  mvrf1  21203  mplsubrglem  21219  mplsubrg  21220  mvrcl  21230  mpllvec  21234  subrgmvrf  21244  mplmon  21245  mplcoe1  21247  mplbas2  21252  opsrtoslem2  21272  mvrf2  21277  evlseu  21302  ply1sclf1  21469  matinvgcell  21593  mat0dimcrng  21628  mat1dimcrng  21635  dmatcrng  21660  scmatcrng  21679  scmatfo  21688  scmatf1  21689  scmatf1o  21690  mdetunilem9  21778  invrvald  21834  cpmatsubgpmat  21878  mat2pmatf1  21887  mat2pmatghm  21888  m2cpmfo  21914  m2cpmf1o  21915  pmatcollpwscmatlem2  21948  pm2mpf1  21957  pm2mpfo  21972  pm2mpf1o  21973  pm2mpgrpiso  21975  chfacfisf  22012  chfacfisfcpmat  22013  chfacfscmul0  22016  chfacfpmmul0  22020  chfacfpmmulgsum2  22023  tgcl  22128  tgtopon  22130  indistopon  22160  fctop  22163  cctop  22165  ppttop  22166  epttop  22168  mretopd  22252  toponmre  22253  neiptopuni  22290  neiptoptop  22291  neiptopnei  22292  resttopon  22321  resttopon2  22328  restfpw  22339  perfopn  22345  ordtrest2  22364  cnco  22426  cnpco  22427  lmss  22458  cnt0  22506  cnt1  22510  cnhaus  22514  isnrm2  22518  isnrm3  22519  isreg2  22537  dnsconst  22538  ordtt1  22539  lmfun  22541  dishaus  22542  cncmp  22552  fincmp  22553  tgcmp  22561  cmpcld  22562  uncmp  22563  sscmp  22565  cmpfi  22568  cnconn  22582  conncn  22586  iunconn  22588  conncompss  22593  2ndc1stc  22611  1stcrest  22613  2ndcdisj  22616  1stcelcls  22621  llynlly  22637  restnlly  22642  restlly  22643  islly2  22644  llyrest  22645  nllyrest  22646  llyidm  22648  nllyidm  22649  hausllycmp  22654  cldllycmp  22655  lly1stc  22656  dislly  22657  comppfsc  22692  kgentopon  22698  llycmpkgen2  22710  1stckgen  22714  ptbasfi  22741  txtopon  22751  pttopon  22756  xkotopon  22760  ptclsg  22775  xkoccn  22779  ptcnplem  22781  uptx  22785  txdis1cn  22795  txlly  22796  txnlly  22797  pthaus  22798  ptrescn  22799  txcmp  22803  txhaus  22807  tx1stc  22810  txkgen  22812  xkohaus  22813  txconn  22849  qtoptop2  22859  qtoptopon  22864  qtopkgen  22870  qtopss  22875  qtopeu  22876  qtopomap  22878  qtopcmap  22879  kqreglem1  22901  kqreglem2  22902  kqnrmlem1  22903  kqnrmlem2  22904  nrmr0reg  22909  hmeocnv  22922  hmeof1o2  22923  hmeores  22931  hmeoco  22932  idhmeo  22933  reghmph  22953  nrmhmph  22954  indishmph  22958  ordthmeolem  22961  ordthmeo  22962  txhmeo  22963  txswaphmeo  22965  pt1hmeo  22966  ptunhmeo  22968  xpstopnlem1  22969  xkohmeo  22975  qtopf1  22976  qtophmeo  22977  isfil2  23016  filconn  23043  isufil2  23068  filssufilg  23071  fixufil  23082  uffixfr  23083  fin1aufil  23092  fmf  23105  fmufil  23119  fclsfnflim  23187  ptcmplem3  23214  ptcmplem4  23215  cnextfun  23224  cnextf  23226  cnextfres  23229  grpinvhmeo  23246  tmdgsum2  23256  tgplacthmeo  23263  symgtgp  23266  clsnsg  23270  tgpconncompeqg  23272  tgpconncomp  23273  tgpt0  23279  qustgpopn  23280  prdstgpd  23285  tsmsfbas  23288  tsmsgsum  23299  tsmsres  23304  tsmsinv  23308  tgptsmscls  23310  tsmsxplem1  23313  tsmsxplem2  23314  tsmsxp  23315  tvclvec  23359  ustfilxp  23373  trust  23390  utoptop  23395  utoptopon  23397  utopreg  23413  ressusp  23425  tususp  23433  psmetxrge0  23475  isxmet2d  23489  metres2  23525  prdsdsf  23529  prdsxmetlem  23530  prdsmet  23532  imasdsf1olem  23535  imasf1oxmet  23537  imasf1omet  23538  xmetresbl  23599  tmsxms  23651  tmsms  23652  imasf1oxms  23654  imasf1oms  23655  blcls  23671  comet  23678  stdbdxmet  23680  stdbdmet  23681  met1stc  23686  ressxms  23690  ressms  23691  prdsxms  23695  prdsms  23696  metustto  23718  xmsusp  23734  nrmmetd  23739  tngngp2  23825  nrgdomn  23844  subrgnrg  23846  tngnrg  23847  sranlm  23857  nrginvrcn  23865  nlmtlm  23867  nvctvc  23873  lssnlm  23874  lssnvc  23875  ngpocelbl  23877  nmhmco  23929  nmhmplusg  23930  qdensere  23942  tgioo  23968  xrtgioo  23978  xrsmopn  23984  reperflem  23990  icccmplem1  23994  icccmplem2  23995  reconnlem2  23999  xrge0tsms  24006  metdsf  24020  metdsre  24025  metnrm  24034  mulc1cncf  24077  icchmeo  24113  icopnfcnv  24114  xrhmeo  24118  cnrehmeo  24125  evth  24131  phtpcer  24167  pcohtpy  24192  pi1xfrgim  24230  cvsdiv  24304  cvsdivcl  24305  cphnvc  24349  cphsubrglem  24350  cphreccllem  24351  tcphcph  24410  clsocv  24423  iscmet3lem1  24464  iscmet3  24466  cmetss  24489  relcmpcmet  24491  bcthlem5  24501  cmetcusp1  24526  cmetcusp  24527  cphssphl  24544  cmscsscms  24546  cssbn  24548  cmslsschl  24550  chlcsschl  24551  rrxmet  24581  rrxbasefi  24583  minveclem7  24608  hlhil  24616  ivthlem1  24624  evthicc2  24633  ovolfsf  24644  ovolunlem1a  24669  ovoliunlem1  24675  ovolicc2lem2  24691  ovolicc2lem4  24693  ovolicc2lem5  24694  cmmbl  24707  nulmbl  24708  nulmbl2  24709  unmbl  24710  shftmbl  24711  voliunlem2  24724  ioombl1  24735  uniioombl  24762  dyadmbllem  24772  volcn  24779  vitalilem2  24782  vitalilem5  24785  mbfconst  24806  cncombf  24831  cnmbf  24832  i1fd  24854  i1fmullem  24867  itg1addlem2  24870  i1fmulc  24877  itg1mulc  24878  mbfi1fseqlem1  24889  mbfi1fseqlem4  24892  mbfi1flimlem  24896  xrge0f  24905  itg2const2  24915  itg2mulclem  24920  itg2mono  24927  itg2i1fseq  24929  itg2addlem  24932  itg2gt0  24934  itg2cnlem2  24936  itg2cn  24937  iblss  24978  itgle  24983  itgeqa  24987  iblconst  24991  itgconst  24992  ibladdlem  24993  itgaddlem1  24996  iblabslem  25001  iblabs  25002  iblabsr  25003  iblmulc2  25004  itgmulc2lem1  25005  itgsplit  25009  bddmulibl  25012  bddiblnc  25015  itggt0  25017  itgcn  25018  limciun  25067  perfdvf  25076  dvfre  25124  dvcnvlem  25149  dvexp3  25151  dvferm1lem  25157  dvferm2lem  25159  c1lip2  25171  dvle  25180  dvne0  25184  lhop1lem  25186  dvfsumrlim  25204  ftc1lem5  25213  ftc1cn  25216  ply1nz  25295  ply1nzb  25296  ply1domn  25297  ply1divalg  25311  fta1blem  25342  fta1b  25343  ig1peu  25345  ig1pdvds  25350  ply1lpir  25352  ply1pid  25353  elplyr  25371  plyeq0  25381  coeeu  25395  dgrub  25404  plyreres  25452  plydivalg  25468  fta1lem  25476  elqaalem3  25490  qaa  25492  aareccl  25495  aannenlem1  25497  aalioulem6  25506  taylfvallem1  25525  taylf  25529  tayl0  25530  dvtaylp  25538  ulmss  25565  mtest  25572  radcnvle  25588  psercnlem2  25592  psercn  25594  abelthlem2  25600  abelthlem8  25607  abelth  25609  pilem2  25620  pilem3  25621  efif1olem4  25710  efifo  25712  eff1olem  25713  logdmss  25806  dvloglem  25812  logf1o2  25814  efopnlem2  25821  logtayl  25824  cxpcn2  25908  cxpcn3  25910  loglesqrt  25920  logreclem  25921  relogbcl  25932  relogbreexp  25934  relogbmul  25936  relogbcxp  25944  atanre  26044  asinneg  26045  atandmneg  26065  atandmcj  26068  atandmtan  26079  bndatandm  26088  atansssdm  26092  areaf  26120  rlimcnp  26124  rlimcnp3  26126  xrlimcnp  26127  amgmlem  26148  amgm  26149  emcllem7  26160  dmlogdmgm  26182  rpdmgm  26183  dmgmaddnn0  26185  lgamgulmlem1  26187  lgamgulmlem2  26188  wilthlem2  26227  wilthlem3  26228  wilth  26229  ftalem3  26233  basellem3  26241  basellem4  26242  ppisval  26262  ppisval2  26263  sgmnncl  26305  chtdif  26316  ppidif  26321  ppinncl  26332  ppiltx  26335  sqff1o  26340  muinv  26351  dvdsmulf1o  26352  logexprlim  26382  mersenne  26384  perfectlem2  26387  dchrfi  26412  dchrghm  26413  dchrabs  26417  dchr1re  26420  bcmono  26434  bposlem3  26443  bposlem4  26444  bposlem5  26445  bposlem6  26446  bposlem9  26449  lgsfcl2  26460  lgsval2lem  26464  lgsmod  26480  lgsdirprm  26488  lgsne0  26492  lgsqrlem2  26504  gausslemma2dlem0h  26520  gausslemma2dlem1a  26522  gausslemma2dlem4  26526  lgseisenlem1  26532  lgseisenlem2  26533  lgsquadlem1  26537  lgsquadlem2  26538  lgsquad2lem2  26542  2sqlem8  26583  2sqlem9  26584  2sqlem11  26586  2sqmod  26593  2sqreulem1  26603  2sqreunnlem1  26606  dchrisumlem2  26647  dchrisumlem3  26648  dchrmusum2  26651  dchrvmasumlem2  26655  dchrvmasumiflem1  26658  dchrvmaeq0  26661  dchrisum0flblem2  26666  dchrisum0re  26670  dchrisum0lem1b  26672  dchrisum0lem2  26675  dirith2  26685  2vmadivsumlem  26697  chpdifbndlem1  26710  selberg3lem1  26714  selberg4lem1  26717  pntrlog2bndlem3  26736  pntpbnd1  26743  pntibndlem2  26748  pntlemo  26764  pntlem3  26766  tglngval  26921  hlcgreu  26988  tglinethrueu  27009  ragncol  27079  foot  27092  mideu  27108  opptgdim2  27115  hlpasch  27126  trgcopyeu  27176  cgraswap  27190  cgracom  27192  cgratr  27193  flatcgra  27194  dfcgra2  27200  acopyeu  27204  cgrg3col4  27223  f1otrg  27241  f1otrge  27242  xmstrkgc  27262  axlowdimlem13  27331  axlowdimlem15  27333  axlowdimlem16  27334  axcontlem2  27342  axcontlem3  27343  axcontlem4  27344  axcontlem10  27350  eengtrkg  27363  eengtrkge  27364  structiedg0val  27401  upgr1elem  27491  umgrislfupgrlem  27501  edglnl  27522  ausgrumgri  27546  usgredgreu  27594  uspgredg2vtxeu  27596  uspgredg2v  27600  usgredg2v  27603  usgr1e  27621  subgruhgredgd  27660  subuhgr  27662  subupgr  27663  subumgr  27664  subusgr  27665  upgrreslem  27680  upgrres  27682  umgrres  27683  nbumgrvtx  27722  nbgrssovtx  27737  nbupgrres  27740  nbusgrf1o0  27745  uvtxnbgrb  27777  cusgr0v  27804  cplgr1v  27806  cusgr1v  27807  cusgrexilem2  27818  cusgrexi  27819  structtocusgr  27822  cusgrres  27824  cusgrfilem2  27832  vtxdgfisf  27852  umgr2v2evd2  27903  ewlkprop  27979  lfgriswlk  28065  trlres  28077  upgrwlkdvdelem  28113  uhgrwkspth  28132  usgr2wlkspth  28136  pthdlem1  28143  crctcshwlkn0lem7  28190  crctcshtrl  28197  crctcsh  28198  wwlknbp  28216  wspthnp  28224  wlkswwlksf1o  28253  wwlksnext  28267  wwlksnextinj  28273  wwlksnextsurj  28274  wwlksnextbij0  28275  wwlksnextproplem3  28285  2trld  28312  2spthd  28315  umgr2adedgwlk  28319  umgr2adedgwlkon  28320  umgr2adedgwlkonALT  28321  umgr2adedgspth  28322  elwwlks2ons3  28329  clwwlkbp  28358  clwwlkccatlem  28362  clwlkclwwlklem2a2  28366  clwlkclwwlklem2fv2  28369  clwlkclwwlklem2a4  28370  clwlkclwwlkfolem  28380  clwlkclwwlkfo  28382  clwlkclwwlkf1  28383  clwlkclwwlkf1o  28384  clwwlkinwwlk  28413  clwwlkel  28419  clwwlkf1  28422  clwwlkfo  28423  clwwlkf1o  28424  wwlksext2clwwlk  28430  wwlksubclwwlk  28431  clwwnisshclwwsn  28432  clwwlknccat  28436  s2elclwwlknon2  28477  clwwlknonex2lem2  28481  clwwlknonex2e  28483  lp1cycl  28525  3trld  28545  3spthd  28549  3cycld  28551  eupthp1  28589  eupth2eucrct  28590  frgr1v  28644  nfrgr2v  28645  3vfriswmgrlem  28650  n4cyclfrgr  28664  frgrncvvdeqlem8  28679  frgrncvvdeqlem9  28680  frgrncvvdeqlem10  28681  frgrwopreglem5  28694  clwwnonrepclwwnon  28718  numclwwlk1lem2f1  28730  numclwwlk1lem2fo  28731  numclwwlk1lem2f1o  28732  numclwlk2lem2f1o  28752  nvex  28982  isnv  28983  isblo3i  29172  ipblnfi  29226  ubthlem2  29242  minvecolem7  29254  htthlem  29288  hlimadd  29564  hhsscms  29649  ocsh  29654  occl  29675  pjhthlem2  29763  pjhtheu  29765  pjpreeq  29769  ococin  29779  chscllem2  30009  chscl  30012  unopf1o  30287  cnvunop  30289  unoplin  30291  counop  30292  hmopadj2  30312  hmoplin  30313  bralnfn  30319  lnopmi  30371  unopbd  30386  hmops  30391  hmopm  30392  hmopco  30394  bdophmi  30403  nlelshi  30431  nlelchi  30432  riesz3i  30433  cnlnadjlem2  30439  adjlnop  30457  hmopidmpji  30523  pjclem4  30570  pj3si  30578  h1da  30720  shatomistici  30732  iundisjf  30937  f1o3d  30971  2ndresdju  30995  2ndresdjuf1o  30996  xppreima2  30997  isoun  31043  f1od2  31065  xrge0infss  31092  xrge0addcld  31094  xrofsup  31099  difioo  31112  fzsplit3  31124  iundisjfi  31126  subne0nn  31144  xreceu  31205  s3f1  31230  ccatf1  31232  swrdf1  31237  posrasymb  31252  resspos  31253  resstos  31254  odutos  31255  mgcf1o  31290  abliso  31314  gsumpart  31324  xrge0tsmsd  31326  cntrcrng  31331  pmtrcnel  31367  pmtrcnelor  31369  cycpmfv2  31390  cycpmcl  31392  cycpmco2lem4  31405  tocyccntz  31420  archiabllem1  31456  archiabllem2c  31458  archiabllem2  31460  suborng  31523  subofld  31524  rhmdvdsr  31526  elrhmunit  31528  0nellinds  31575  lindssn  31582  nsgmgc  31606  qsidomlem2  31638  fply1  31676  sradrng  31682  sralvec  31684  rgmoddim  31702  matdim  31707  lmhmlvec2  31711  dimkerim  31717  fedgmul  31721  extdg1id  31747  qtopt1  31794  qtophaus  31795  locfinreflem  31799  cmppcmp  31817  dispcmp  31818  zarmxt1  31839  pstmxmet  31856  xpinpreima2  31866  tpr2rico  31871  ordtrest2NEW  31882  xrmulc1cn  31889  zrhnm  31928  indf1ofs  32003  hashf2  32061  hasheuni  32062  esumcvg  32063  prsiga  32108  pwldsys  32134  ldsysgenld  32137  ldgenpisyslem1  32140  sxsigon  32169  measdivcstALTV  32202  volfiniune  32207  imambfm  32238  dya2iocnrect  32257  omssubaddlem  32275  sibfof  32316  sitgf  32323  oddpwdc  32330  eulerpartlemb  32344  eulerpartlemgvv  32352  sseqmw  32367  sseqf  32368  sseqp1  32371  fibp1  32377  prob01  32389  probfinmeasb  32404  probfinmeasbALTV  32405  probmeasb  32406  dstrvprob  32447  dstfrvel  32449  ballotlemic  32482  ballotlem1c  32483  ballotlemro  32498  ballotlemrc  32506  ballotlemirc  32507  ballotth  32513  plymulx0  32535  signstfvn  32557  signstfvcl  32561  signstfveq0a  32564  signstfveq0  32565  fdvposlt  32588  reprpmtf1o  32615  tgoldbachgnn  32648  bnj951  32764  bnj1379  32819  bnj1422  32826  bnj149  32864  bnj151  32866  bnj908  32920  bnj944  32927  bnj970  32936  bnj1006  32949  bnj1177  32995  bnj1189  32998  bnj1321  33016  bnj1398  33023  bnj1417  33030  bnj1523  33060  srcmpltd  33063  f1resrcmplf1d  33068  pthhashvtx  33098  2cycld  33109  subfacp1lem3  33153  subfacp1lem5  33155  erdszelem8  33169  erdszelem9  33170  cnpconn  33201  txpconn  33203  ptpconn  33204  connpconn  33206  sconnpi1  33210  txsconn  33212  cvxpconn  33213  cvxsconn  33214  iccllysconn  33221  cvmseu  33247  cvmfolem  33250  cvmliftmolem2  33253  cvmliftlem14  33268  cvmlift2lem9a  33274  cvmlift2lem12  33285  cvmlift2lem13  33286  cvmlift3  33299  satfdm  33340  fmla1  33358  fmlaomn0  33361  fmlasucdisj  33370  satff  33381  sategoelfvb  33390  mvrsfpw  33477  mrsubrn  33484  mrsubff1  33485  msubff  33501  msubff1  33527  mvhf1  33530  mclsssvlem  33533  mclsind  33541  mthmpps  33553  lediv2aALT  33644  dfon2  33777  poxp2  33799  frxp2  33800  poxp3  33805  frxp3  33806  nofnbday  33864  noxp1o  33875  nosepdmlem  33895  nosupno  33915  nosupbday  33917  nosupfv  33918  nosupbnd1  33926  nosupbnd2  33928  noinfno  33930  noinfbday  33932  noinffv  33933  noinfbnd1  33941  noinfbnd2  33943  nocvxmin  33982  conway  34002  scutun12  34013  etasslt  34016  scutbdaybnd2  34019  scutbdaybnd2lim  34020  scutbdaylt  34021  slerec  34022  sltlpss  34096  cofcutr  34101  addsval  34135  dfrdg4  34262  altxpsspw  34288  segconeu  34322  btwnconn1lem13  34410  btwnconn1lem14  34411  outsideofeu  34442  outsidele  34443  linerflx1  34460  linethrueu  34467  fwddifval  34473  fwddifnval  34474  nn0prpwlem  34520  neibastop1  34557  neibastop2lem  34558  topjoin  34563  fnemeet1  34564  fnemeet2  34565  fnejoin1  34566  fnejoin2  34567  filnetlem3  34578  onsuctopon  34632  bj-nnfim  34937  bj-nnfand  34940  bj-nnford  34942  bj-dfnnf3  34948  bj-nnfalt  34957  bj-nnfext  34958  bj-elgab  35136  relowlssretop  35543  elxp8  35551  finorwe  35562  finxp1o  35572  pibt2  35597  finixpnum  35771  fin2solem  35772  fin2so  35773  lindsadd  35779  lindsdom  35780  lindsenlbs  35781  ptrecube  35786  poimirlem4  35790  poimirlem7  35793  poimirlem13  35799  poimirlem15  35801  poimirlem16  35802  poimirlem17  35803  poimirlem18  35804  poimirlem19  35805  poimirlem20  35806  poimirlem21  35807  poimirlem24  35810  poimirlem26  35812  poimirlem27  35813  poimirlem29  35815  poimirlem30  35816  poimirlem31  35817  poimirlem32  35818  opnmbllem0  35822  mblfinlem2  35824  itg2gt0cn  35841  ibladdnclem  35842  itgaddnclem1  35844  iblabsnclem  35849  iblabsnc  35850  iblmulc2nc  35851  itgmulc2nclem1  35852  itggt0cn  35856  ftc1cnnc  35858  ftc1anclem3  35861  ftc1anclem4  35862  ftc1anclem5  35863  ftc1anclem6  35864  ftc1anclem7  35865  ftc1anclem8  35866  ftc1anc  35867  areacirclem2  35875  areacirc  35879  unirep  35880  sdclem1  35910  mettrifi  35924  istotbnd3  35938  sstotbnd2  35941  sstotbnd  35942  sstotbnd3  35943  equivtotbnd  35945  isbndx  35949  isbnd3  35951  blbnd  35954  equivbnd  35957  prdsbnd  35960  prdstotbnd  35961  ismtyhmeo  35972  heibor1  35977  heibor  35988  bfp  35991  rrnmet  35996  rrncmslem  35999  rrnequiv  36002  ismrer1  36005  iccbnd  36007  opidonOLD  36019  grpokerinj  36060  isgrpda  36122  isdrngo2  36125  iscringd  36165  crngohomfo  36173  smprngopr  36219  prnc  36234  isfldidl  36235  prter3  36903  lshpnelb  37005  lsatspn0  37021  lsatssn0  37023  lssats  37033  lsatcv0  37052  lsat0cv  37054  islshpcv  37074  lkr0f  37115  lshpsmreu  37130  lduallvec  37175  lkrlspeqN  37192  cdleme50f1  38564  cdleme50f1o  38567  cdleme  38581  cdlemk56  38992  dvalveclem  39046  dvhlveclem  39129  dvheveccl  39133  cdlemm10N  39139  diaf1oN  39151  dihord4  39279  dihf11lem  39287  dihf11  39288  dihglblem2N  39315  dihglb2  39363  dochvalr  39378  doch2val2  39385  dochocss  39387  dochsat  39404  dochshpncl  39405  dochnel  39414  dvh4dimlem  39464  dochsnkr2cl  39495  dochkr1  39499  lcfl6lem  39519  lcfl9a  39526  lclkrlem1  39527  lclkrlem2l  39539  lclkrlem2o  39542  lclkrlem2q  39544  lclkr  39554  lclkrslem1  39558  lclkrslem2  39559  lcfrlem9  39571  lcfrlem16  39579  lcfrlem17  39580  lcfrlem27  39590  lcfrlem37  39600  lcfrlem38  39601  lcfrlem40  39603  lcdlkreqN  39643  mapdordlem2  39658  mapdrvallem2  39666  mapdn0  39690  mapdpglem20  39712  mapdpglem30  39723  mapdpglem32  39726  mapdpg  39727  mapdindp0  39740  mapdh6aN  39756  mapdh6eN  39761  mapdh6kN  39767  hdmaplem4  39795  hdmap1val  39819  hdmap1l6a  39830  hdmap1l6e  39835  hdmap1l6k  39841  hdmapval3N  39859  hdmap11lem2  39863  hdmapnzcl  39866  hdmaprnlem3eN  39879  hdmap14lem4a  39892  hdmap14lem6  39894  hdmap14lem7  39895  hgmapvvlem2  39945  hgmapvvlem3  39946  hlhilhillem  39985  lcmineqlem15  40058  aks4d1p1  40091  aks4d1p3  40093  xppss12  40211  selvval2lem4  40235  frlmsnic  40270  evlsbagval  40282  mhpind  40290  mhphf  40292  posqsqznn  40350  addinvcom  40420  prjspersym  40453  0prjspnlem  40467  dffltz  40478  flt0  40481  flt4lem5e  40500  isnacs3  40539  mzpindd  40575  eldioph  40587  eldioph3  40595  rencldnfilem  40649  irrapxlem1  40651  irrapxlem4  40654  irrapxlem6  40656  pellexlem5  40662  pellfundlb  40713  rmspecnonsq  40736  rmxnn  40780  rmynn  40785  rmynn0  40786  jm2.22  40824  jm2.23  40825  jm2.20nn  40826  jm2.27a  40834  jm2.27c  40836  rmydioph  40843  jm3.1lem3  40848  dford3lem1  40855  rpnnen3lem  40860  harinf  40863  wepwsolem  40874  dnnumch3  40879  fnwe2lem2  40883  fnwe2  40885  dfac11  40894  lnmlsslnm  40913  lnmepi  40917  lmhmlnmsplit  40919  pwssplit4  40921  filnm  40922  imasgim  40932  harn0  40934  lpirlnr  40949  hbtlem7  40957  hbtlem6  40961  hbt  40962  dgraaub  40980  mpaaeu  40982  aaitgo  40994  rgspnmin  41003  proot1ex  41033  deg1mhm  41039  fzunt  41069  fzuntd  41070  fzunt1d  41071  fzuntgd  41072  omssrncard  41154  fiinfi  41187  cotrclrcl  41357  fsovf1od  41631  ntrk2imkb  41654  ntrf  41740  gneispacef2  41753  rr-phpd  41828  expgrowth  41960  binomcxplemdvbinom  41978  binomcxplemnotnn0  41981  ordelordALT  42164  2uasbanh  42188  rfcnnnub  42586  elixpconstg  42646  wessf1ornlem  42729  disjinfi  42738  projf1o  42743  fconst7  42819  fzisoeu  42846  monoordxrv  43029  iccshift  43063  iooshift  43067  fmul01lt1lem2  43133  ellimciota  43162  mullimc  43164  mullimcf  43171  sumnnodd  43178  addlimc  43196  liminfval2  43316  liminflimsupxrre  43365  icccncfext  43435  dvcosre  43460  dvdivbd  43471  dvdivcncf  43475  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  itgsinexplem1  43502  iblcncfioo  43526  itgperiod  43529  stoweidlem7  43555  stoweidlem14  43562  stoweidlem16  43564  stoweidlem26  43574  stoweidlem27  43575  stoweidlem31  43579  stoweidlem34  43582  stoweidlem36  43584  stoweidlem46  43594  stoweidlem47  43595  stoweidlem52  43600  stoweidlem57  43605  stoweidlem59  43607  stoweidlem60  43608  wallispilem3  43615  wallispilem4  43616  dirkertrigeqlem3  43648  dirkeritg  43650  dirkercncf  43655  fourierdlem15  43670  fourierdlem20  43675  fourierdlem25  43680  fourierdlem34  43689  fourierdlem37  43692  fourierdlem41  43696  fourierdlem42  43697  fourierdlem47  43701  fourierdlem48  43702  fourierdlem51  43705  fourierdlem52  43706  fourierdlem57  43711  fourierdlem58  43712  fourierdlem59  43713  fourierdlem63  43717  fourierdlem64  43718  fourierdlem65  43719  fourierdlem68  43722  fourierdlem79  43733  fourierdlem80  43734  fourierdlem81  43735  fourierdlem92  43746  fourierdlem104  43758  fourierdlem111  43765  fouriersw  43779  etransclem3  43785  etransclem7  43789  etransclem10  43792  etransclem15  43797  etransclem19  43801  etransclem20  43802  etransclem21  43803  etransclem22  43804  etransclem24  43806  etransclem25  43807  etransclem27  43809  etransclem28  43810  etransclem35  43817  etransclem44  43826  etransclem48  43830  nnfoctbdjlem  44000  preimagelt  44244  preimalegt  44245  fnresfnco  44546  funressnfv  44548  fsetsnf1  44557  fsetsnfo  44558  fsetsnf1o  44559  cfsetsnfsetf1  44564  cfsetsnfsetfo  44565  cfsetsnfsetf1o  44566  fcoresf1  44574  ffnafv  44674  rlimdmafv  44680  dfatco  44759  rlimdmafv2  44761  zm1nn  44805  eluzge0nn0  44815  2elfz2melfz  44821  subsubelfzo0  44829  smonoord  44834  setsnidel  44840  imasetpreimafvbijlemf1  44867  imasetpreimafvbijlemfo  44868  imasetpreimafvbij  44869  iccpartigtl  44886  iccpartgt  44890  iccpartf  44894  icceuelpart  44899  fargshiftf1  44904  fargshiftfo  44905  sprsymrelfolem2  44956  sprsymrelfo  44960  sprsymrelf1o  44961  prproropf1o  44970  sfprmdvdsmersenne  45066  lighneallem4  45073  evenm1odd  45102  evenp1odd  45103  oddp1eveni  45104  oddm1eveni  45105  m2even  45117  oexpnegALTV  45140  opoeALTV  45146  opeoALTV  45147  oddprmALTV  45150  nnoALTV  45158  nn0oALTV  45159  nnpw2evenALTV  45165  perfectALTVlem2  45185  perfectALTV  45186  sbgoldbalt  45244  wtgoldbnnsum4prm  45265  bgoldbnnsum3prm  45267  isomuspgrlem2c  45293  isomuspgrlem2d  45294  isomuspgrlem2e  45295  1hegrlfgr  45305  uspgrsprfo  45321  uspgrsprf1o  45322  mgmhmf1o  45352  idmgmhm  45353  resmgmhm  45363  resmgmhm2  45364  resmgmhm2b  45365  mgmhmco  45366  mgmhmeql  45368  copissgrp  45373  isrnghm2d  45470  rnghmf1o  45472  rnghmco  45476  idrnghm  45477  c0mgm  45478  c0rhm  45481  c0rnghm  45482  c0snmgmhm  45483  c0snmhm  45484  zrrnghm  45486  lidlmsgrp  45495  zlidlring  45497  2zlidl  45503  2zrngamgm  45508  2zrngagrp  45512  2zrngmmgm  45515  rngcinv  45550  rngcinvALTV  45562  ringcinv  45601  ringcinvALTV  45625  nn0eo  45885  blennnelnn  45933  nnpw2blen  45937  dignn0fr  45958  dignn0ldlem  45959  dig2nn1st  45962  1arymaptf1  45999  1arymaptfo  46000  1arymaptf1o  46001  2arymaptf1  46010  2arymaptfo  46011  2arymaptf1o  46012  inlinecirc02p  46144  toslat  46279  topdlat  46301  isthincd  46329  fullthinc  46338  thincfth  46340  thincciso  46341  0thincg  46342  aacllem  46516