Theorem sylanbrc 584

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 513	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
4		sylanbrc.3	. 2 ⊢ (𝜃 ↔ (𝜓 ∧ 𝜒))
5	3, 4	sylibr 233	1 ⊢ (𝜑 → 𝜃)

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

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 398

This theorem is referenced by:  sylanblrc  591  ifpimpda  1082  ecase23d  1474  raleqbidvvOLD  3331  elrabd  3685  eqeu  3702  euind  3720  reuind  3749  eldifd  3959  eqssd  3999  ssrabdv  4071  psstr  4104  elind  4194  elpwdifsn  4792  prproe  4906  propeqop  5507  issod  5621  wereu  5672  wereu2  5673  relssdmrnOLD  6266  predtrss  6321  ordelord  6384  funun  6592  fnsng  6598  fnprg  6605  fntpg  6606  fununi  6621  fncoOLD  6666  f00  6771  f1ss  6791  f1ssr  6792  f1ssres  6793  focofo  6816  f1f1orn  6842  foimacnv  6848  foun  6849  f1oprswap  6875  rescnvimafod  7073  fvn0ssdmfun  7074  dff3  7099  fmpt  7107  ffnfv  7115  fmpt2d  7120  ffvresb  7121  fprb  7192  fpr2g  7210  nvof1o  7275  fcof1  7282  fcofo  7283  fcof1od  7289  fliftf  7309  soisores  7321  soisoi  7322  isoini2  7333  f1oiso  7345  moriotass  7395  fnoprabg  7528  f1ocnvd  7654  fiun  7926  f1iun  7927  1stcof  8002  2ndcof  8003  1stconst  8083  2ndconst  8084  curry1  8087  curry2  8090  fo2ndf  8104  f1o2ndf1  8105  soxp  8112  wexp  8113  fnwelem  8114  poxp2  8126  frxp2  8127  poxp3  8133  frxp3  8134  suppssov1  8180  suppssfv  8184  fpr1  8285  wfrlem10OLD  8315  smores2  8351  smo11  8361  smoiso2  8366  tfrlem12  8386  tfrlem13  8387  oalimcl  8557  oaf1o  8560  omlimcl  8575  omeu  8582  oeeulem  8598  oeeui  8599  omsmo  8654  cofonr  8670  naddunif  8689  eroveu  8803  fsetfocdm  8852  undifixp  8925  resixpfo  8927  elixpsn  8928  dom2lem  8985  difsnen  9050  omxpenlem  9070  sucdom2OLD  9079  sdomdomtr  9107  domsdomtr  9109  fodomr  9125  xpf1o  9136  ssfi  9170  sdomdomtrfi  9201  domsdomtrfi  9202  sucdom2  9203  php2  9208  php3  9209  phpeqd  9212  php2OLD  9220  php3OLD  9221  phpeqdOLD  9222  1sdom2dom  9244  unxpdomlem3  9249  f1finf1o  9268  f1finf1oOLD  9269  frfi  9285  wofi  9289  nnsdomg  9299  nnsdomgOLD  9300  domunfican  9317  fofinf1o  9324  mapfienlem3  9399  mapfien  9400  marypha1lem  9425  supeu  9446  infeu  9488  ordtypelem2  9511  ordtypelem4  9513  ordtypelem10  9519  oismo  9532  wemaplem2  9539  card2inf  9547  brwdom2  9565  wdom2d  9572  harwdom  9583  cantnfp1lem2  9671  cantnfp1lem3  9672  cantnflem1  9681  cantnflem2  9682  cantnf  9685  cnfcom2lem  9693  cnfcom3lem  9695  ttrcltr  9708  frr1  9751  tskwe  9942  cardsdomelir  9965  cardprclem  9971  cardmin2  9991  en2other2  10001  r0weon  10004  infxpenc  10010  fseqenlem1  10016  fseqenlem2  10017  fodomacn  10048  infpwfien  10054  finnisoeu  10105  iunfictbso  10106  dfac12lem2  10136  cofsmo  10261  cfsmolem  10262  alephsing  10268  sornom  10269  infpssrlem3  10297  infpssrlem5  10299  ssfin4  10302  isfin4p1  10307  fincssdom  10315  fin23lem23  10318  fin23lem28  10332  fin23lem31  10335  fin23lem34  10338  isf32lem9  10353  compssiso  10366  fin1a2lem12  10403  hsmexlem1  10418  hsmexlem4  10421  domtriomlem  10434  cardmin  10556  smobeth  10578  gchen1  10617  gchen2  10618  fpwwe2lem10  10632  fpwwe2lem11  10633  fpwwe2lem12  10634  fpwwe2  10635  canthnum  10641  canthwe  10643  canthp1lem2  10645  canthp1  10646  pwfseqlem5  10655  gchdjuidm  10660  gchxpidm  10661  gchhar  10671  r1wunlim  10729  inar1  10767  inatsk  10770  r1tskina  10774  gruiun  10791  gruima  10794  gruina  10810  addclpi  10884  mulclpi  10885  nqereu  10921  dmrecnq  10960  genpcl  11000  suplem1pr  11044  receu  11856  recgt0  12057  cju  12205  peano5nni  12212  nn0n0n1ge2  12536  nn0ge2m1nn  12538  nnnegz  12558  elnnz  12565  nnz  12576  msqznn  12641  eluzaddiOLD  12851  eluzsubiOLD  12853  uz2mulcl  12907  elq  12931  nnrp  12982  rpaddcl  12993  rpmulcl  12994  rpdivcl  12996  rpgecl  12999  ge0p1rp  13002  elrpd  13010  nn0rp0  13429  ge0addcl  13434  ge0mulcl  13435  ge0xaddcl  13436  ge0xmulcl  13437  icoshftf1o  13448  xnn0xrge0  13480  peano2fzr  13511  uzsubsubfz  13520  fzsplit2  13523  elfznn  13527  fzss1  13537  fzss2  13538  fzp1elp1  13551  elfz1b  13567  elfz0fzfz0  13603  fz0fzelfz0  13604  difelfznle  13612  elfzofz  13645  prinfzo0  13668  nn0p1elfzo  13672  fzosplitsnm1  13704  ubmelm1fzo  13725  fzofzp1b  13727  elfznelfzo  13734  fzosplitsn  13737  injresinj  13750  flge0nn0  13782  flge1nn  13783  zmodcl  13853  modmuladdnn0  13877  modsumfzodifsn  13906  seqcl2  13983  seqf2  13984  seqfveq2  13987  monoord  13995  seqid2  14011  expcl2lem  14036  expclzlem  14046  zsqcl2  14100  bcval4  14264  bcn1  14270  bccl2  14280  hashnn0n0nn  14348  hashfun  14394  seqcoll  14422  ccatsymb  14529  ccatrn  14536  ccat2s1fvw  14585  swrds1  14613  swrdccat2  14616  swrdccatin2  14676  pfxccatin12lem2  14678  pfxccatin12lem3  14679  pfxccatin12  14680  pfxccat3  14681  pfxccat3a  14685  spllen  14701  splfv2a  14703  splval2  14704  repswswrd  14731  cshwidxmod  14750  cshwcsh2id  14776  pfx2  14895  2swrd2eqwrdeq  14901  wwlktovfo  14906  wwlktovf1o  14907  shftfn  15017  shftf  15023  01sqrexlem2  15187  01sqrexlem7  15192  resqreu  15196  sqrtneg  15211  nn0abscl  15256  nnabscl  15269  abs2dif  15276  sqreu  15304  limsupval2  15421  climuni  15493  2clim  15513  climcn2  15534  rlimdiv  15589  isercolllem2  15609  isercolllem3  15610  isercoll  15611  isercoll2  15612  iseralt  15628  summolem2a  15658  mptfzshft  15721  fsum0diag2  15726  fsumge0  15738  climcndslem1  15792  mertenslem1  15827  ntrivcvgmul  15845  prodmolem2a  15875  fprodser  15890  fprodeq0  15916  fprodge0  15934  binomrisefac  15983  eff2  16039  tanval  16068  rpnnen2lem9  16162  sqrt2irrlem  16188  fzo0dvdseq  16263  oexpneg  16285  oddge22np1  16289  evennn02n  16290  evennn2n  16291  nno  16322  divalglem5  16337  bitsfzolem  16372  bitsinv1lem  16379  bitsinv2  16381  bitsf1ocnv  16382  bitsinvp1  16387  sadcaddlem  16395  sadadd2lem  16397  sadadd3  16399  sadasslem  16408  sadeq  16410  gcdcllem3  16439  divgcdz  16449  sqgcd  16499  lcmneg  16537  lcmfunsnlem2lem2  16573  prmind2  16619  sqnprm  16636  isprm5  16641  isprm6  16648  qgt0numnn  16684  crth  16708  phimullem  16709  eulerthlem1  16711  eulerthlem2  16712  hashgcdlem  16718  oddprm  16740  pythagtriplem6  16751  pythagtriplem11  16755  pythagtriplem13  16757  pythagtriplem19  16763  iserodd  16765  pclem  16768  pcpremul  16773  pceu  16776  pc2dvds  16809  difsqpwdvds  16817  pcadd  16819  oddprmdvds  16833  pockthlem  16835  pockthg  16836  prmreclem3  16848  1arith  16857  4sqlem11  16885  4sqlem12  16886  4sqlem13  16887  4sqlem14  16888  4sqlem17  16891  vdwlem2  16912  vdwlem8  16918  vdwlem12  16922  ramtlecl  16930  ramub1lem1  16956  prmgaplem4  16984  prmgaplem7  16987  cshwshashlem2  17027  cshwrepswhash1  17033  imasaddfnlem  17471  imasaddflem  17473  imasvscafn  17480  imasvscaf  17482  isacs1i  17598  mreacs  17599  catideu  17616  invfun  17708  invf  17712  invf1o  17713  issubc3  17796  cofucl  17835  funcres2c  17849  ffthf1o  17867  fulloppc  17870  fthoppc  17871  ffthoppc  17872  idffth  17881  cofull  17882  cofth  17883  ressffth  17886  initoeu2lem2  17962  setcmon  18034  setcepi  18035  catciso  18058  fthestrcsetc  18099  fullestrcsetc  18100  embedsetcestrclem  18106  fthsetcestrc  18114  fullsetcestrc  18115  hofcllem  18208  hofcl  18209  yonedalem3  18230  yonffthlem  18232  yoniso  18235  poslubd  18363  lubun  18465  isacs5  18498  acsfiindd  18503  mreclatBAD  18513  psss  18530  cnvtsr  18538  mgmsscl  18563  gsumval2  18602  sgrp0  18615  sgrp1  18617  hashfinmndnn  18639  ismndd  18644  mndpfo  18645  mnd1  18664  mhmf1o  18679  0mhm  18697  resmhm  18698  resmhm2  18699  resmhm2b  18700  mhmco  18701  gsumvallem2  18712  frmdss2  18741  efmndmnd  18767  sgrp2nmndlem4  18806  isgrpd2e  18838  grpinvf1o  18890  grpinvnzcl  18892  dfgrp3  18919  grp1  18927  mhmmnd  18942  ghmgrp  18944  subgmulg  19015  issubg4  19020  0subgOLD  19027  isnsg3  19035  nmzsubg  19040  ssnmz  19041  nmznsg  19043  0nsg  19044  nsgid  19045  ghmnsgima  19111  ghmnsgpreima  19112  ghmf1  19116  ghmf1o  19117  conjnmzb  19122  gicref  19140  gafo  19155  gaid  19158  subgga  19159  gass  19160  gasubg  19161  gastacl  19168  orbsta  19172  cntrsubgnsg  19202  invoppggim  19222  symgextf1  19284  symgextfo  19285  symgextf1o  19286  symgfixf1  19300  symgfixfo  19302  symgfixf1o  19303  f1omvdmvd  19306  pmtrprfv  19316  pmtrdifwrdel2  19349  psgneu  19369  psgnvalfi  19377  psgnfieu  19381  psgnprfval  19384  odf1  19425  dfod2  19427  odf1o1  19435  odf1o2  19436  odhash3  19439  sylow1lem2  19462  sylow2blem2  19484  sylow3lem1  19490  sylow3lem2  19491  pj1eu  19559  efglem  19579  efginvrel2  19590  efgsrel  19597  efgsp1  19600  efgsres  19601  efgredleme  19606  efgrelexlemb  19613  efgredeu  19615  efgcpbllemb  19618  isabld  19658  ghmcmn  19694  ghmabl  19695  invghm  19696  cntrabl  19706  torsubg  19717  prdsabld  19725  qusabl  19728  abl1  19729  iscygd  19750  iscygodd  19751  cycsubmcmn  19752  gsumval3a  19766  gsumval3eu  19767  gsumpt  19825  gsummptf1o  19826  dprdcntz  19873  dprdff  19877  dprdfcntz  19880  dprdfadd  19885  dprdlub  19891  dprd2dlem1  19906  dprd2da  19907  dmdprdpr  19914  dprdpr  19915  ablfacrp  19931  ablfac1eu  19938  pgpfaclem1  19946  pgpfaclem2  19947  ablfaclem3  19952  issimpgd  19958  prmgrpsimpgd  19979  ablsimpgprmd  19980  srgfcl  20013  srglmhm  20038  srgrmhm  20039  iscrngd  20100  ringsrg  20103  prdscrngd  20129  xpsringd  20139  dvdsrmul  20171  1unit  20181  unitmulcl  20187  unitgrp  20190  unitabl  20191  unitnegcl  20204  rhmf1o  20262  rimgim  20268  rhmco  20269  kerf1ghm  20275  rhmdvdsr  20280  elrhmunit  20282  opprnzr  20292  ringelnzr  20293  0ringnnzr  20295  isdrng2  20322  drngnzr  20328  isdrngd  20341  isdrngdOLD  20343  subrgcrng  20360  subrguss  20371  subrgunit  20374  subrgnzr  20378  issubdrg  20382  resrhm  20386  imadrhmcl  20406  fldsdrgfld  20407  subdrgint  20412  primefld  20414  isabvd  20421  srngf1o  20455  issrngd  20462  lssneln0  20556  islmhm2  20642  lmhmf1o  20650  pwssplit1  20663  lmimgim  20669  lsslvec  20712  lspabs3  20727  lspsneq  20728  lspfixed  20734  lspexch  20735  lspsolvlem  20748  islbs3  20761  lbsextlem1  20764  lbsextlem3  20766  lbsextlem4  20767  rlmlvec  20821  lidlnz  20846  quscrng  20871  drnglpir  20884  unitrrg  20902  domnrrg  20909  opprdomn  20912  drngdomn  20914  fldidomOLD  20917  fidomndrng  20919  cnfldfunALT  20950  xrs1mnd  20976  xrs10  20977  cnmsubglem  21001  gzrngunit  21004  zringunit  21028  prmirredlem  21034  expghm  21037  mulgghm2  21038  domnchr  21076  zncyg  21096  znf1o  21099  zntoslem  21104  znfld  21108  znidomb  21109  cygznlem3  21117  psgnghm  21125  pjfo  21262  frlmlvec  21308  frlmphl  21328  uvcf1  21339  frlmssuvc1  21341  frlmsslsp  21343  frlmup4  21348  lindff1  21367  lindfrn  21368  lsslindf  21377  lmimlbs  21383  indlcim  21387  lmimco  21391  isassad  21411  sraassab  21414  psrbagcon  21475  psrbagconOLD  21476  gsumbagdiaglemOLD  21483  gsumbagdiagOLD  21484  psrass1lemOLD  21485  gsumbagdiaglem  21486  gsumbagdiag  21487  psrass1lem  21488  psrbas  21489  psrcrng  21525  mvrf1  21537  mvrcl  21543  mvrf2  21544  mplsubrglem  21555  mplsubrg  21556  mpllvec  21571  subrgmvrf  21581  mplmon  21582  mplcoe1  21584  mplbas2  21589  opsrtoslem2  21609  evlseu  21638  ply1sclf1  21803  matinvgcell  21929  mat0dimcrng  21964  mat1dimcrng  21971  mat1rngiso  21980  dmatcrng  21996  scmatcrng  22015  scmatfo  22024  scmatf1  22025  scmatf1o  22026  scmatrngiso  22030  mdetunilem9  22114  invrvald  22170  cpmatsubgpmat  22214  mat2pmatf1  22223  mat2pmatghm  22224  m2cpmfo  22250  m2cpmf1o  22251  m2cpmrngiso  22252  pmatcollpwscmatlem2  22284  pm2mpf1  22293  pm2mpfo  22308  pm2mpf1o  22309  pm2mpgrpiso  22311  pm2mprngiso  22316  chfacfisf  22348  chfacfisfcpmat  22349  chfacfscmul0  22352  chfacfpmmul0  22356  chfacfpmmulgsum2  22359  tgcl  22464  tgtopon  22466  indistopon  22496  fctop  22499  cctop  22501  ppttop  22502  epttop  22504  mretopd  22588  toponmre  22589  neiptopuni  22626  neiptoptop  22627  neiptopnei  22628  resttopon  22657  resttopon2  22664  restfpw  22675  perfopn  22681  ordtrest2  22700  cnco  22762  cnpco  22763  lmss  22794  cnt0  22842  cnt1  22846  cnhaus  22850  isnrm2  22854  isnrm3  22855  isreg2  22873  dnsconst  22874  ordtt1  22875  lmfun  22877  dishaus  22878  cncmp  22888  fincmp  22889  tgcmp  22897  cmpcld  22898  uncmp  22899  sscmp  22901  cmpfi  22904  cnconn  22918  conncn  22922  iunconn  22924  conncompss  22929  2ndc1stc  22947  1stcrest  22949  2ndcdisj  22952  1stcelcls  22957  llynlly  22973  restnlly  22978  restlly  22979  islly2  22980  llyrest  22981  nllyrest  22982  llyidm  22984  nllyidm  22985  hausllycmp  22990  cldllycmp  22991  lly1stc  22992  dislly  22993  comppfsc  23028  kgentopon  23034  llycmpkgen2  23046  1stckgen  23050  ptbasfi  23077  txtopon  23087  pttopon  23092  xkotopon  23096  ptclsg  23111  xkoccn  23115  ptcnplem  23117  uptx  23121  txdis1cn  23131  txlly  23132  txnlly  23133  pthaus  23134  ptrescn  23135  txcmp  23139  txhaus  23143  tx1stc  23146  txkgen  23148  xkohaus  23149  txconn  23185  qtoptop2  23195  qtoptopon  23200  qtopkgen  23206  qtopss  23211  qtopeu  23212  qtopomap  23214  qtopcmap  23215  kqreglem1  23237  kqreglem2  23238  kqnrmlem1  23239  kqnrmlem2  23240  nrmr0reg  23245  hmeocnv  23258  hmeof1o2  23259  hmeores  23267  hmeoco  23268  idhmeo  23269  reghmph  23289  nrmhmph  23290  indishmph  23294  ordthmeolem  23297  ordthmeo  23298  txhmeo  23299  txswaphmeo  23301  pt1hmeo  23302  ptunhmeo  23304  xpstopnlem1  23305  xkohmeo  23311  qtopf1  23312  qtophmeo  23313  isfil2  23352  filconn  23379  isufil2  23404  filssufilg  23407  fixufil  23418  uffixfr  23419  fin1aufil  23428  fmf  23441  fmufil  23455  fclsfnflim  23523  ptcmplem3  23550  ptcmplem4  23551  cnextfun  23560  cnextf  23562  cnextfres  23565  grpinvhmeo  23582  tmdgsum2  23592  tgplacthmeo  23599  symgtgp  23602  clsnsg  23606  tgpconncompeqg  23608  tgpconncomp  23609  tgpt0  23615  qustgpopn  23616  prdstgpd  23621  tsmsfbas  23624  tsmsgsum  23635  tsmsres  23640  tsmsinv  23644  tgptsmscls  23646  tsmsxplem1  23649  tsmsxplem2  23650  tsmsxp  23651  tvclvec  23695  ustfilxp  23709  trust  23726  utoptop  23731  utoptopon  23733  utopreg  23749  ressusp  23761  tususp  23769  psmetxrge0  23811  isxmet2d  23825  metres2  23861  prdsdsf  23865  prdsxmetlem  23866  prdsmet  23868  imasdsf1olem  23871  imasf1oxmet  23873  imasf1omet  23874  xmetresbl  23935  tmsxms  23987  tmsms  23988  imasf1oxms  23990  imasf1oms  23991  blcls  24007  comet  24014  stdbdxmet  24016  stdbdmet  24017  met1stc  24022  ressxms  24026  ressms  24027  prdsxms  24031  prdsms  24032  metustto  24054  xmsusp  24070  nrmmetd  24075  tngngp2  24161  nrgdomn  24180  subrgnrg  24182  tngnrg  24183  sranlm  24193  nrginvrcn  24201  nlmtlm  24203  nvctvc  24209  lssnlm  24210  lssnvc  24211  ngpocelbl  24213  nmhmco  24265  nmhmplusg  24266  qdensere  24278  tgioo  24304  xrtgioo  24314  xrsmopn  24320  reperflem  24326  icccmplem1  24330  icccmplem2  24331  reconnlem2  24335  xrge0tsms  24342  metdsf  24356  metdsre  24361  metnrm  24370  mulc1cncf  24413  icchmeo  24449  icopnfcnv  24450  xrhmeo  24454  cnrehmeo  24461  evth  24467  phtpcer  24503  pcohtpy  24528  pi1xfrgim  24566  cvsdiv  24640  cvsdivcl  24641  cphnvc  24685  cphsubrglem  24686  cphreccllem  24687  tcphcph  24746  clsocv  24759  iscmet3lem1  24800  iscmet3  24802  cmetss  24825  relcmpcmet  24827  bcthlem5  24837  cmetcusp1  24862  cmetcusp  24863  cphssphl  24880  cmscsscms  24882  cssbn  24884  cmslsschl  24886  chlcsschl  24887  rrxmet  24917  rrxbasefi  24919  minveclem7  24944  hlhil  24952  ivthlem1  24960  evthicc2  24969  ovolfsf  24980  ovolunlem1a  25005  ovoliunlem1  25011  ovolicc2lem2  25027  ovolicc2lem4  25029  ovolicc2lem5  25030  cmmbl  25043  nulmbl  25044  nulmbl2  25045  unmbl  25046  shftmbl  25047  voliunlem2  25060  ioombl1  25071  uniioombl  25098  dyadmbllem  25108  volcn  25115  vitalilem2  25118  vitalilem5  25121  mbfconst  25142  cncombf  25167  cnmbf  25168  i1fd  25190  i1fmullem  25203  itg1addlem2  25206  i1fmulc  25213  itg1mulc  25214  mbfi1fseqlem1  25225  mbfi1fseqlem4  25228  mbfi1flimlem  25232  xrge0f  25241  itg2const2  25251  itg2mulclem  25256  itg2mono  25263  itg2i1fseq  25265  itg2addlem  25268  itg2gt0  25270  itg2cnlem2  25272  itg2cn  25273  iblss  25314  itgle  25319  itgeqa  25323  iblconst  25327  itgconst  25328  ibladdlem  25329  itgaddlem1  25332  iblabslem  25337  iblabs  25338  iblabsr  25339  iblmulc2  25340  itgmulc2lem1  25341  itgsplit  25345  bddmulibl  25348  bddiblnc  25351  itggt0  25353  itgcn  25354  limciun  25403  perfdvf  25412  dvfre  25460  dvcnvlem  25485  dvexp3  25487  dvferm1lem  25493  dvferm2lem  25495  c1lip2  25507  dvle  25516  dvne0  25520  lhop1lem  25522  dvfsumrlim  25540  ftc1lem5  25549  ftc1cn  25552  ply1nz  25631  ply1nzb  25632  ply1domn  25633  ply1divalg  25647  fta1blem  25678  fta1b  25679  ig1peu  25681  ig1pdvds  25686  ply1lpir  25688  ply1pid  25689  elplyr  25707  plyeq0  25717  coeeu  25731  dgrub  25740  plyreres  25788  plydivalg  25804  fta1lem  25812  elqaalem3  25826  qaa  25828  aareccl  25831  aannenlem1  25833  aalioulem6  25842  taylfvallem1  25861  taylf  25865  tayl0  25866  dvtaylp  25874  ulmss  25901  mtest  25908  radcnvle  25924  psercnlem2  25928  psercn  25930  abelthlem2  25936  abelthlem8  25943  abelth  25945  pilem2  25956  pilem3  25957  efif1olem4  26046  efifo  26048  eff1olem  26049  logdmss  26142  dvloglem  26148  logf1o2  26150  efopnlem2  26157  logtayl  26160  cxpcn2  26244  cxpcn3  26246  loglesqrt  26256  logreclem  26257  relogbcl  26268  relogbreexp  26270  relogbmul  26272  relogbcxp  26280  atanre  26380  asinneg  26381  atandmneg  26401  atandmcj  26404  atandmtan  26415  bndatandm  26424  atansssdm  26428  areaf  26456  rlimcnp  26460  rlimcnp3  26462  xrlimcnp  26463  amgmlem  26484  amgm  26485  emcllem7  26496  dmlogdmgm  26518  rpdmgm  26519  dmgmaddnn0  26521  lgamgulmlem1  26523  lgamgulmlem2  26524  wilthlem2  26563  wilthlem3  26564  wilth  26565  ftalem3  26569  basellem3  26577  basellem4  26578  ppisval  26598  ppisval2  26599  sgmnncl  26641  chtdif  26652  ppidif  26657  ppinncl  26668  ppiltx  26671  sqff1o  26676  muinv  26687  dvdsmulf1o  26688  logexprlim  26718  mersenne  26720  perfectlem2  26723  dchrfi  26748  dchrghm  26749  dchrabs  26753  dchr1re  26756  bcmono  26770  bposlem3  26779  bposlem4  26780  bposlem5  26781  bposlem6  26782  bposlem9  26785  lgsfcl2  26796  lgsval2lem  26800  lgsmod  26816  lgsdirprm  26824  lgsne0  26828  lgsqrlem2  26840  gausslemma2dlem0h  26856  gausslemma2dlem1a  26858  gausslemma2dlem4  26862  lgseisenlem1  26868  lgseisenlem2  26869  lgsquadlem1  26873  lgsquadlem2  26874  lgsquad2lem2  26878  2sqlem8  26919  2sqlem9  26920  2sqlem11  26922  2sqmod  26929  2sqreulem1  26939  2sqreunnlem1  26942  dchrisumlem2  26983  dchrisumlem3  26984  dchrmusum2  26987  dchrvmasumlem2  26991  dchrvmasumiflem1  26994  dchrvmaeq0  26997  dchrisum0flblem2  27002  dchrisum0re  27006  dchrisum0lem1b  27008  dchrisum0lem2  27011  dirith2  27021  2vmadivsumlem  27033  chpdifbndlem1  27046  selberg3lem1  27050  selberg4lem1  27053  pntrlog2bndlem3  27072  pntpbnd1  27079  pntibndlem2  27084  pntlemo  27100  pntlem3  27102  nofnbday  27145  noxp1o  27156  nosepdmlem  27176  nosupno  27196  nosupbday  27198  nosupfv  27199  nosupbnd1  27207  nosupbnd2  27209  noinfno  27211  noinfbday  27213  noinffv  27214  noinfbnd1  27222  noinfbnd2  27224  nocvxmin  27270  conway  27290  scutun12  27301  etasslt  27304  scutbdaybnd2  27307  scutbdaybnd2lim  27308  scutbdaylt  27309  slerec  27310  sltlpss  27391  0elleft  27393  0elright  27394  cofcutr  27401  addsval  27436  addsproplem2  27444  addsproplem4  27446  addsproplem5  27447  addsproplem6  27448  addsuniflem  27474  negsproplem2  27493  negsproplem4  27495  negsproplem5  27496  negsproplem6  27497  mulsproplem5  27566  mulsproplem6  27567  mulsproplem7  27568  mulsproplem8  27569  mulsproplem12  27573  mulsuniflem  27594  noreceuw  27629  tglngval  27792  hlcgreu  27859  tglinethrueu  27880  ragncol  27950  foot  27963  mideu  27979  opptgdim2  27986  hlpasch  27997  trgcopyeu  28047  cgraswap  28061  cgracom  28063  cgratr  28064  flatcgra  28065  dfcgra2  28071  acopyeu  28075  cgrg3col4  28094  f1otrg  28112  f1otrge  28113  xmstrkgc  28133  axlowdimlem13  28202  axlowdimlem15  28204  axlowdimlem16  28205  axcontlem2  28213  axcontlem3  28214  axcontlem4  28215  axcontlem10  28221  eengtrkg  28234  eengtrkge  28235  structiedg0val  28272  upgr1elem  28362  umgrislfupgrlem  28372  edglnl  28393  ausgrumgri  28417  usgredgreu  28465  uspgredg2vtxeu  28467  uspgredg2v  28471  usgredg2v  28474  usgr1e  28492  subgruhgredgd  28531  subuhgr  28533  subupgr  28534  subumgr  28535  subusgr  28536  upgrreslem  28551  upgrres  28553  umgrres  28554  nbumgrvtx  28593  nbgrssovtx  28608  nbupgrres  28611  nbusgrf1o0  28616  uvtxnbgrb  28648  cusgr0v  28675  cplgr1v  28677  cusgr1v  28678  cusgrexilem2  28689  cusgrexi  28690  structtocusgr  28693  cusgrres  28695  cusgrfilem2  28703  vtxdgfisf  28723  umgr2v2evd2  28774  ewlkprop  28850  lfgriswlk  28935  trlres  28947  upgrwlkdvdelem  28983  uhgrwkspth  29002  usgr2wlkspth  29006  pthdlem1  29013  crctcshwlkn0lem7  29060  crctcshtrl  29067  crctcsh  29068  wwlknbp  29086  wspthnp  29094  wlkswwlksf1o  29123  wwlksnext  29137  wwlksnextinj  29143  wwlksnextsurj  29144  wwlksnextbij0  29145  wwlksnextproplem3  29155  2trld  29182  2spthd  29185  umgr2adedgwlk  29189  umgr2adedgwlkon  29190  umgr2adedgwlkonALT  29191  umgr2adedgspth  29192  elwwlks2ons3  29199  clwwlkbp  29228  clwwlkccatlem  29232  clwlkclwwlklem2a2  29236  clwlkclwwlklem2fv2  29239  clwlkclwwlklem2a4  29240  clwlkclwwlkfolem  29250  clwlkclwwlkfo  29252  clwlkclwwlkf1  29253  clwlkclwwlkf1o  29254  clwwlkinwwlk  29283  clwwlkel  29289  clwwlkf1  29292  clwwlkfo  29293  clwwlkf1o  29294  wwlksext2clwwlk  29300  wwlksubclwwlk  29301  clwwnisshclwwsn  29302  clwwlknccat  29306  s2elclwwlknon2  29347  clwwlknonex2lem2  29351  clwwlknonex2e  29353  lp1cycl  29395  3trld  29415  3spthd  29419  3cycld  29421  eupthp1  29459  eupth2eucrct  29460  frgr1v  29514  nfrgr2v  29515  3vfriswmgrlem  29520  n4cyclfrgr  29534  frgrncvvdeqlem8  29549  frgrncvvdeqlem9  29550  frgrncvvdeqlem10  29551  frgrwopreglem5  29564  clwwnonrepclwwnon  29588  numclwwlk1lem2f1  29600  numclwwlk1lem2fo  29601  numclwwlk1lem2f1o  29602  numclwlk2lem2f1o  29622  nvex  29852  isnv  29853  isblo3i  30042  ipblnfi  30096  ubthlem2  30112  minvecolem7  30124  htthlem  30158  hlimadd  30434  hhsscms  30519  ocsh  30524  occl  30545  pjhthlem2  30633  pjhtheu  30635  pjpreeq  30639  ococin  30649  chscllem2  30879  chscl  30882  unopf1o  31157  cnvunop  31159  unoplin  31161  counop  31162  hmopadj2  31182  hmoplin  31183  bralnfn  31189  lnopmi  31241  unopbd  31256  hmops  31261  hmopm  31262  hmopco  31264  bdophmi  31273  nlelshi  31301  nlelchi  31302  riesz3i  31303  cnlnadjlem2  31309  adjlnop  31327  hmopidmpji  31393  pjclem4  31440  pj3si  31448  h1da  31590  shatomistici  31602  iundisjf  31808  f1o3d  31839  2ndresdju  31862  2ndresdjuf1o  31863  xppreima2  31864  isoun  31911  f1od2  31934  xrge0infss  31961  xrge0addcld  31963  xrofsup  31968  difioo  31981  fzsplit3  31993  iundisjfi  31995  subne0nn  32015  xreceu  32076  s3f1  32101  ccatf1  32103  swrdf1  32108  posrasymb  32123  resspos  32124  resstos  32125  odutos  32126  mgcf1o  32161  abliso  32185  gsumpart  32195  xrge0tsmsd  32197  cntrcrng  32202  pmtrcnel  32238  pmtrcnelor  32240  cycpmfv2  32261  cycpmcl  32263  cycpmco2lem4  32276  tocyccntz  32291  archiabllem1  32327  archiabllem2c  32329  archiabllem2  32331  isdrng4  32384  suborng  32422  subofld  32423  quslvec  32460  0nellinds  32472  dvdsruasso  32479  lindssn  32483  nsgmgc  32512  ghmqusker  32521  lmhmqusker  32523  rhmqusker  32533  drngidlhash  32541  qsidomlem2  32561  qsnzr  32563  mxidlirredi  32576  drngmxidl  32582  fply1  32626  ply1lvec  32627  sradrng  32662  sralvec  32664  rlmdim  32683  rgmoddimOLD  32684  matdim  32689  lmhmlvec2  32693  ply1degltdimlem  32696  ply1degltdim  32697  dimkerim  32701  fedgmul  32705  extdg1id  32731  irngnzply1  32744  qtopt1  32804  qtophaus  32805  locfinreflem  32809  cmppcmp  32827  dispcmp  32828  zarmxt1  32849  pstmxmet  32866  xpinpreima2  32876  tpr2rico  32881  ordtrest2NEW  32892  xrmulc1cn  32899  zrhnm  32938  indf1ofs  33013  hashf2  33071  hasheuni  33072  esumcvg  33073  prsiga  33118  pwldsys  33144  ldsysgenld  33147  ldgenpisyslem1  33150  sxsigon  33179  measdivcstALTV  33212  volfiniune  33217  imambfm  33250  dya2iocnrect  33269  omssubaddlem  33287  sibfof  33328  sitgf  33335  oddpwdc  33342  eulerpartlemb  33356  eulerpartlemgvv  33364  sseqmw  33379  sseqf  33380  sseqp1  33383  fibp1  33389  prob01  33401  probfinmeasb  33416  probfinmeasbALTV  33417  probmeasb  33418  dstrvprob  33459  dstfrvel  33461  ballotlemic  33494  ballotlem1c  33495  ballotlemro  33510  ballotlemrc  33518  ballotlemirc  33519  ballotth  33525  plymulx0  33547  signstfvn  33569  signstfvcl  33573  signstfveq0a  33576  signstfveq0  33577  fdvposlt  33600  reprpmtf1o  33627  tgoldbachgnn  33660  bnj951  33775  bnj1379  33830  bnj1422  33837  bnj149  33875  bnj151  33877  bnj908  33931  bnj944  33938  bnj970  33947  bnj1006  33960  bnj1177  34006  bnj1189  34009  bnj1321  34027  bnj1398  34034  bnj1417  34041  bnj1523  34071  srcmpltd  34074  f1resrcmplf1d  34079  pthhashvtx  34107  2cycld  34118  subfacp1lem3  34162  subfacp1lem5  34164  erdszelem8  34178  erdszelem9  34179  cnpconn  34210  txpconn  34212  ptpconn  34213  connpconn  34215  sconnpi1  34219  txsconn  34221  cvxpconn  34222  cvxsconn  34223  iccllysconn  34230  cvmseu  34256  cvmfolem  34259  cvmliftmolem2  34262  cvmliftlem14  34277  cvmlift2lem9a  34283  cvmlift2lem12  34294  cvmlift2lem13  34295  cvmlift3  34308  satfdm  34349  fmla1  34367  fmlaomn0  34370  fmlasucdisj  34379  satff  34390  sategoelfvb  34399  mvrsfpw  34486  mrsubrn  34493  mrsubff1  34494  msubff  34510  msubff1  34536  mvhf1  34539  mclsssvlem  34542  mclsind  34550  mthmpps  34562  lediv2aALT  34651  dfon2  34753  dfrdg4  34912  altxpsspw  34938  segconeu  34972  btwnconn1lem13  35060  btwnconn1lem14  35061  outsideofeu  35092  outsidele  35093  linerflx1  35110  linethrueu  35117  fwddifval  35123  fwddifnval  35124  gg-icchmeo  35159  gg-cnrehmeo  35160  nn0prpwlem  35196  neibastop1  35233  neibastop2lem  35234  topjoin  35239  fnemeet1  35240  fnemeet2  35241  fnejoin1  35242  fnejoin2  35243  filnetlem3  35254  onsuctopon  35308  bj-nnfim  35613  bj-nnfand  35616  bj-nnford  35618  bj-dfnnf3  35624  bj-nnfalt  35633  bj-nnfext  35634  bj-elgab  35808  relowlssretop  36233  elxp8  36241  finorwe  36252  finxp1o  36262  pibt2  36287  finixpnum  36462  fin2solem  36463  fin2so  36464  lindsadd  36470  lindsdom  36471  lindsenlbs  36472  ptrecube  36477  poimirlem4  36481  poimirlem7  36484  poimirlem13  36490  poimirlem15  36492  poimirlem16  36493  poimirlem17  36494  poimirlem18  36495  poimirlem19  36496  poimirlem20  36497  poimirlem21  36498  poimirlem24  36501  poimirlem26  36503  poimirlem27  36504  poimirlem29  36506  poimirlem30  36507  poimirlem31  36508  poimirlem32  36509  opnmbllem0  36513  mblfinlem2  36515  itg2gt0cn  36532  ibladdnclem  36533  itgaddnclem1  36535  iblabsnclem  36540  iblabsnc  36541  iblmulc2nc  36542  itgmulc2nclem1  36543  itggt0cn  36547  ftc1cnnc  36549  ftc1anclem3  36552  ftc1anclem4  36553  ftc1anclem5  36554  ftc1anclem6  36555  ftc1anclem7  36556  ftc1anclem8  36557  ftc1anc  36558  areacirclem2  36566  areacirc  36570  unirep  36571  sdclem1  36600  mettrifi  36614  istotbnd3  36628  sstotbnd2  36631  sstotbnd  36632  sstotbnd3  36633  equivtotbnd  36635  isbndx  36639  isbnd3  36641  blbnd  36644  equivbnd  36647  prdsbnd  36650  prdstotbnd  36651  ismtyhmeo  36662  heibor1  36667  heibor  36678  bfp  36681  rrnmet  36686  rrncmslem  36689  rrnequiv  36692  ismrer1  36695  iccbnd  36697  opidonOLD  36709  grpokerinj  36750  isgrpda  36812  isdrngo2  36815  iscringd  36855  crngohomfo  36863  smprngopr  36909  prnc  36924  isfldidl  36925  petlem  37671  prter3  37741  lshpnelb  37843  lsatspn0  37859  lsatssn0  37861  lssats  37871  lsatcv0  37890  lsat0cv  37892  islshpcv  37912  lkr0f  37953  lshpsmreu  37968  lduallvec  38013  lkrlspeqN  38030  cdleme50f1  39403  cdleme50f1o  39406  cdleme  39420  cdlemk56  39831  dvalveclem  39885  dvhlveclem  39968  dvheveccl  39972  cdlemm10N  39978  diaf1oN  39990  dihord4  40118  dihf11lem  40126  dihf11  40127  dihglblem2N  40154  dihglb2  40202  dochvalr  40217  doch2val2  40224  dochocss  40226  dochsat  40243  dochshpncl  40244  dochnel  40253  dvh4dimlem  40303  dochsnkr2cl  40334  dochkr1  40338  lcfl6lem  40358  lcfl9a  40365  lclkrlem1  40366  lclkrlem2l  40378  lclkrlem2o  40381  lclkrlem2q  40383  lclkr  40393  lclkrslem1  40397  lclkrslem2  40398  lcfrlem9  40410  lcfrlem16  40418  lcfrlem17  40419  lcfrlem27  40429  lcfrlem37  40439  lcfrlem38  40440  lcfrlem40  40442  lcdlkreqN  40482  mapdordlem2  40497  mapdrvallem2  40505  mapdn0  40529  mapdpglem20  40551  mapdpglem30  40562  mapdpglem32  40565  mapdpg  40566  mapdindp0  40579  mapdh6aN  40595  mapdh6eN  40600  mapdh6kN  40606  hdmaplem4  40634  hdmap1val  40658  hdmap1l6a  40669  hdmap1l6e  40674  hdmap1l6k  40680  hdmapval3N  40698  hdmap11lem2  40702  hdmapnzcl  40705  hdmaprnlem3eN  40718  hdmap14lem4a  40731  hdmap14lem6  40733  hdmap14lem7  40734  hgmapvvlem2  40784  hgmapvvlem3  40785  hlhilhillem  40824  lcmineqlem15  40897  aks4d1p1  40930  aks4d1p3  40932  xppss12  41044  imacrhmcl  41087  frlmsnic  41108  mhmcompl  41118  evlsbagval  41136  mhpind  41164  posqsqznn  41230  addinvcom  41301  prjspersym  41346  0prjspnlem  41362  dffltz  41373  flt0  41376  flt4lem5e  41395  isnacs3  41434  mzpindd  41470  eldioph  41482  eldioph3  41490  rencldnfilem  41544  irrapxlem1  41546  irrapxlem4  41549  irrapxlem6  41551  pellexlem5  41557  pellfundlb  41608  rmspecnonsq  41631  rmxnn  41676  rmynn  41681  rmynn0  41682  jm2.22  41720  jm2.23  41721  jm2.20nn  41722  jm2.27a  41730  jm2.27c  41732  rmydioph  41739  jm3.1lem3  41744  dford3lem1  41751  rpnnen3lem  41756  harinf  41759  wepwsolem  41770  dnnumch3  41775  fnwe2lem2  41779  fnwe2  41781  dfac11  41790  lnmlsslnm  41809  lnmepi  41813  lmhmlnmsplit  41815  pwssplit4  41817  filnm  41818  imasgim  41828  harn0  41830  lpirlnr  41845  hbtlem7  41853  hbtlem6  41857  hbt  41858  dgraaub  41876  mpaaeu  41878  aaitgo  41890  rgspnmin  41899  proot1ex  41929  deg1mhm  41935  onsucelab  41999  onsucf1olem  42006  cantnfub2  42058  omabs2  42068  tfsconcatlem  42072  tfsconcatfo  42079  ofoafo  42092  naddcnffo  42100  oaun3lem1  42110  oaun3lem3  42112  nadd2rabord  42121  nadd2rabon  42123  nadd1rabord  42125  nadd1rabon  42127  naddwordnexlem4  42138  fzunt  42192  fzuntd  42193  fzunt1d  42194  fzuntgd  42195  omssrncard  42277  fiinfi  42310  cotrclrcl  42479  fsovf1od  42753  ntrk2imkb  42774  ntrf  42860  gneispacef2  42873  rr-phpd  42948  expgrowth  43080  binomcxplemdvbinom  43098  binomcxplemnotnn0  43101  ordelordALT  43284  2uasbanh  43308  rfcnnnub  43706  elixpconstg  43764  ssrabdf  43790  rabidd  43835  wessf1ornlem  43868  disjinfi  43877  projf1o  43882  fconst7  43956  fzisoeu  43997  monoordxrv  44179  iccshift  44218  iooshift  44222  fmul01lt1lem2  44288  ellimciota  44317  mullimc  44319  mullimcf  44326  sumnnodd  44333  addlimc  44351  liminfval2  44471  liminflimsupxrre  44520  icccncfext  44590  dvcosre  44615  dvdivbd  44626  dvdivcncf  44630  ioodvbdlimc1lem2  44635  ioodvbdlimc2lem  44637  itgsinexplem1  44657  iblcncfioo  44681  itgperiod  44684  stoweidlem7  44710  stoweidlem14  44717  stoweidlem16  44719  stoweidlem26  44729  stoweidlem27  44730  stoweidlem31  44734  stoweidlem34  44737  stoweidlem36  44739  stoweidlem46  44749  stoweidlem47  44750  stoweidlem52  44755  stoweidlem57  44760  stoweidlem59  44762  stoweidlem60  44763  wallispilem3  44770  wallispilem4  44771  dirkertrigeqlem3  44803  dirkeritg  44805  dirkercncf  44810  fourierdlem15  44825  fourierdlem20  44830  fourierdlem25  44835  fourierdlem34  44844  fourierdlem37  44847  fourierdlem41  44851  fourierdlem42  44852  fourierdlem47  44856  fourierdlem48  44857  fourierdlem51  44860  fourierdlem52  44861  fourierdlem57  44866  fourierdlem58  44867  fourierdlem59  44868  fourierdlem63  44872  fourierdlem64  44873  fourierdlem65  44874  fourierdlem68  44877  fourierdlem79  44888  fourierdlem80  44889  fourierdlem81  44890  fourierdlem92  44901  fourierdlem104  44913  fourierdlem111  44920  fouriersw  44934  etransclem3  44940  etransclem7  44944  etransclem10  44947  etransclem15  44952  etransclem19  44956  etransclem20  44957  etransclem21  44958  etransclem22  44959  etransclem24  44961  etransclem25  44962  etransclem27  44964  etransclem28  44965  etransclem35  44972  etransclem44  44981  etransclem48  44985  nnfoctbdjlem  45158  preimagelt  45402  preimalegt  45403  fnresfnco  45738  funressnfv  45740  fsetsnf1  45749  fsetsnfo  45750  fsetsnf1o  45751  cfsetsnfsetf1  45756  cfsetsnfsetfo  45757  cfsetsnfsetf1o  45758  fcoresf1  45766  ffnafv  45866  rlimdmafv  45872  dfatco  45951  rlimdmafv2  45953  zm1nn  45997  eluzge0nn0  46007  2elfz2melfz  46013  subsubelfzo0  46021  smonoord  46026  setsnidel  46032  imasetpreimafvbijlemf1  46059  imasetpreimafvbijlemfo  46060  imasetpreimafvbij  46061  iccpartigtl  46078  iccpartgt  46082  iccpartf  46086  icceuelpart  46091  fargshiftf1  46096  fargshiftfo  46097  sprsymrelfolem2  46148  sprsymrelfo  46152  sprsymrelf1o  46153  prproropf1o  46162  sfprmdvdsmersenne  46258  lighneallem4  46265  evenm1odd  46294  evenp1odd  46295  oddp1eveni  46296  oddm1eveni  46297  m2even  46309  oexpnegALTV  46332  opoeALTV  46338  opeoALTV  46339  oddprmALTV  46342  nnoALTV  46350  nn0oALTV  46351  nnpw2evenALTV  46357  perfectALTVlem2  46377  perfectALTV  46378  sbgoldbalt  46436  wtgoldbnnsum4prm  46457  bgoldbnnsum3prm  46459  isomuspgrlem2c  46485  isomuspgrlem2d  46486  isomuspgrlem2e  46487  1hegrlfgr  46497  uspgrsprfo  46513  uspgrsprf1o  46514  mgmhmf1o  46544  idmgmhm  46545  resmgmhm  46555  resmgmhm2  46556  resmgmhm2b  46557  mgmhmco  46558  mgmhmeql  46560  copissgrp  46565  xpsrngd  46667  isrnghm2d  46685  rnghmf1o  46687  rnghmco  46692  idrnghm  46693  c0mgm  46694  c0rhm  46697  c0rnghm  46698  c0snmgmhm  46699  c0snmhm  46700  zrrnghm  46702  rngisomring  46705  subrngringnsg  46717  rnglidlmsgrp  46740  rngqiprngimfo  46767  rngqiprngim  46770  zlidlring  46780  2zlidl  46786  2zrngamgm  46791  2zrngagrp  46795  2zrngmmgm  46798  rngcinv  46833  rngcinvALTV  46845  ringcinv  46884  ringcinvALTV  46908  nn0eo  47168  blennnelnn  47216  nnpw2blen  47220  dignn0fr  47241  dignn0ldlem  47242  dig2nn1st  47245  1arymaptf1  47282  1arymaptfo  47283  1arymaptf1o  47284  2arymaptf1  47293  2arymaptfo  47294  2arymaptf1o  47295  inlinecirc02p  47427  toslat  47561  topdlat  47583  isthincd  47611  fullthinc  47620  thincfth  47622  thincciso  47623  0thincg  47624  aacllem  47802