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  1081  ecase23d  1473  raleqbidvv  3302  elrabd  3640  eqeu  3656  euind  3674  reuind  3703  eldifd  3913  eqssd  3953  ssrabdv  4023  psstr  4056  elind  4146  elpwdifsn  4741  prproe  4855  propeqop  5456  issod  5570  wereu  5621  wereu2  5622  relssdmrnOLD  6212  predtrss  6266  ordelord  6329  funun  6535  fnsng  6541  fnprg  6548  fntpg  6549  fununi  6564  fncoOLD  6607  f00  6712  f1ss  6732  f1ssr  6733  f1ssres  6734  focofo  6757  f1f1orn  6783  foimacnv  6789  foun  6790  f1oprswap  6816  rescnvimafod  7012  fvn0ssdmfun  7013  dff3  7037  fmpt  7045  ffnfv  7053  fmpt2d  7058  ffvresb  7059  fprb  7130  fpr2g  7148  nvof1o  7213  fcof1  7220  fcofo  7221  fcof1od  7227  fliftf  7247  soisores  7259  soisoi  7260  isoini2  7271  f1oiso  7283  moriotass  7331  fnoprabg  7464  f1ocnvd  7587  fiun  7858  f1iun  7859  1stcof  7934  2ndcof  7935  1stconst  8013  2ndconst  8014  curry1  8017  curry2  8020  fo2ndf  8034  f1o2ndf1  8035  soxp  8042  wexp  8043  fnwelem  8044  suppssov1  8089  suppssfv  8093  fpr1  8194  wfrlem10OLD  8224  smores2  8260  smo11  8270  smoiso2  8275  tfrlem12  8295  tfrlem13  8296  oalimcl  8467  oaf1o  8470  omlimcl  8485  omeu  8492  oeeulem  8508  oeeui  8509  omsmo  8564  eroveu  8677  fsetfocdm  8725  undifixp  8798  resixpfo  8800  elixpsn  8801  dom2lem  8858  difsnen  8923  omxpenlem  8943  sucdom2OLD  8952  sdomdomtr  8980  domsdomtr  8982  fodomr  8998  xpf1o  9009  ssfi  9043  sdomdomtrfi  9074  domsdomtrfi  9075  sucdom2  9076  php2  9081  php3  9082  phpeqd  9085  php2OLD  9093  php3OLD  9094  phpeqdOLD  9095  1sdom2dom  9117  unxpdomlem3  9122  f1finf1o  9141  f1finf1oOLD  9142  frfi  9158  wofi  9162  nnsdomg  9172  nnsdomgOLD  9173  domunfican  9190  fofinf1o  9197  mapfienlem3  9269  mapfien  9270  marypha1lem  9295  supeu  9316  infeu  9358  ordtypelem2  9381  ordtypelem4  9383  ordtypelem10  9389  oismo  9402  wemaplem2  9409  card2inf  9417  brwdom2  9435  wdom2d  9442  harwdom  9453  cantnfp1lem2  9541  cantnfp1lem3  9542  cantnflem1  9551  cantnflem2  9552  cantnf  9555  cnfcom2lem  9563  cnfcom3lem  9565  ttrcltr  9578  frr1  9621  tskwe  9812  cardsdomelir  9835  cardprclem  9841  cardmin2  9861  en2other2  9871  r0weon  9874  infxpenc  9880  fseqenlem1  9886  fseqenlem2  9887  fodomacn  9918  infpwfien  9924  finnisoeu  9975  iunfictbso  9976  dfac12lem2  10006  cofsmo  10131  cfsmolem  10132  alephsing  10138  sornom  10139  infpssrlem3  10167  infpssrlem5  10169  ssfin4  10172  isfin4p1  10177  fincssdom  10185  fin23lem23  10188  fin23lem28  10202  fin23lem31  10205  fin23lem34  10208  isf32lem9  10223  compssiso  10236  fin1a2lem12  10273  hsmexlem1  10288  hsmexlem4  10291  domtriomlem  10304  cardmin  10426  smobeth  10448  gchen1  10487  gchen2  10488  fpwwe2lem10  10502  fpwwe2lem11  10503  fpwwe2lem12  10504  fpwwe2  10505  canthnum  10511  canthwe  10513  canthp1lem2  10515  canthp1  10516  pwfseqlem5  10525  gchdjuidm  10530  gchxpidm  10531  gchhar  10541  r1wunlim  10599  inar1  10637  inatsk  10640  r1tskina  10644  gruiun  10661  gruima  10664  gruina  10680  addclpi  10754  mulclpi  10755  nqereu  10791  dmrecnq  10830  genpcl  10870  suplem1pr  10914  receu  11726  recgt0  11927  cju  12075  peano5nni  12082  nn0n0n1ge2  12406  nn0ge2m1nn  12408  nnnegz  12428  elnnz  12435  nnssz  12446  msqznn  12508  eluzaddi  12717  eluzsubi  12718  uz2mulcl  12772  elq  12796  nnrp  12847  rpaddcl  12858  rpmulcl  12859  rpdivcl  12861  rpgecl  12864  ge0p1rp  12867  elrpd  12875  nn0rp0  13293  ge0addcl  13298  ge0mulcl  13299  ge0xaddcl  13300  ge0xmulcl  13301  icoshftf1o  13312  xnn0xrge0  13344  peano2fzr  13375  uzsubsubfz  13384  fzsplit2  13387  elfznn  13391  fzss1  13401  fzss2  13402  fzp1elp1  13415  elfz1b  13431  elfz0fzfz0  13467  fz0fzelfz0  13468  difelfznle  13476  elfzofz  13509  prinfzo0  13532  nn0p1elfzo  13536  fzosplitsnm1  13568  ubmelm1fzo  13589  fzofzp1b  13591  elfznelfzo  13598  fzosplitsn  13601  injresinj  13614  flge0nn0  13646  flge1nn  13647  zmodcl  13717  modmuladdnn0  13741  modsumfzodifsn  13770  seqcl2  13847  seqf2  13848  seqfveq2  13851  monoord  13859  seqid2  13875  expcl2lem  13900  expclzlem  13912  zsqcl2  13962  bcval4  14127  bcn1  14133  bccl2  14143  hashnn0n0nn  14211  hashfun  14257  seqcoll  14283  ccatsymb  14390  ccatrn  14397  ccat2s1fvw  14448  ccat2s1fvwOLD  14449  swrds1  14478  swrdccat2  14481  swrdccatin2  14541  pfxccatin12lem2  14543  pfxccatin12lem3  14544  pfxccatin12  14545  pfxccat3  14546  pfxccat3a  14550  spllen  14566  splfv2a  14568  splval2  14569  repswswrd  14596  cshwidxmod  14615  cshwcsh2id  14641  pfx2  14760  2swrd2eqwrdeq  14766  wwlktovfo  14773  wwlktovf1o  14774  shftfn  14884  shftf  14890  sqrlem2  15055  sqrlem7  15060  resqreu  15064  sqrtneg  15079  nn0abscl  15124  nnabscl  15137  abs2dif  15144  sqreu  15172  limsupval2  15289  climuni  15361  2clim  15381  climcn2  15402  rlimdiv  15457  isercolllem2  15477  isercolllem3  15478  isercoll  15479  isercoll2  15480  iseralt  15496  summolem2a  15527  mptfzshft  15590  fsum0diag2  15595  fsumge0  15607  climcndslem1  15661  mertenslem1  15696  ntrivcvgmul  15714  prodmolem2a  15744  fprodser  15759  fprodeq0  15785  fprodge0  15803  binomrisefac  15852  eff2  15908  tanval  15937  rpnnen2lem9  16031  sqrt2irrlem  16057  fzo0dvdseq  16132  oexpneg  16154  oddge22np1  16158  evennn02n  16159  evennn2n  16160  nno  16191  divalglem5  16206  bitsfzolem  16241  bitsinv1lem  16248  bitsinv2  16250  bitsf1ocnv  16251  bitsinvp1  16256  sadcaddlem  16264  sadadd2lem  16266  sadadd3  16268  sadasslem  16277  sadeq  16279  gcdcllem3  16308  divgcdz  16318  sqgcd  16368  lcmneg  16406  lcmfunsnlem2lem2  16442  prmind2  16488  sqnprm  16505  isprm5  16510  isprm6  16517  qgt0numnn  16553  crth  16577  phimullem  16578  eulerthlem1  16580  eulerthlem2  16581  hashgcdlem  16587  oddprm  16609  pythagtriplem6  16620  pythagtriplem11  16624  pythagtriplem13  16626  pythagtriplem19  16632  iserodd  16634  pclem  16637  pcpremul  16642  pceu  16645  pc2dvds  16678  difsqpwdvds  16686  pcadd  16688  oddprmdvds  16702  pockthlem  16704  pockthg  16705  prmreclem3  16717  1arith  16726  4sqlem11  16754  4sqlem12  16755  4sqlem13  16756  4sqlem14  16757  4sqlem17  16760  vdwlem2  16781  vdwlem8  16787  vdwlem12  16791  ramtlecl  16799  ramub1lem1  16825  prmgaplem4  16853  prmgaplem7  16856  cshwshashlem2  16896  cshwrepswhash1  16902  imasaddfnlem  17337  imasaddflem  17339  imasvscafn  17346  imasvscaf  17348  isacs1i  17464  mreacs  17465  catideu  17482  invfun  17574  invf  17578  invf1o  17579  issubc3  17662  cofucl  17701  funcres2c  17715  ffthf1o  17733  fulloppc  17736  fthoppc  17737  ffthoppc  17738  idffth  17747  cofull  17748  cofth  17749  ressffth  17752  initoeu2lem2  17828  setcmon  17900  setcepi  17901  catciso  17924  fthestrcsetc  17965  fullestrcsetc  17966  embedsetcestrclem  17972  fthsetcestrc  17980  fullsetcestrc  17981  hofcllem  18074  hofcl  18075  yonedalem3  18096  yonffthlem  18098  yoniso  18101  poslubd  18229  lubun  18331  isacs5  18364  acsfiindd  18369  mreclatBAD  18379  psss  18396  cnvtsr  18404  mgmsscl  18429  gsumval2  18468  sgrp0  18480  sgrp1  18482  hashfinmndnn  18500  ismndd  18505  mndpfo  18506  mnd1  18524  mhmf1o  18538  0mhm  18556  resmhm  18557  resmhm2  18558  resmhm2b  18559  mhmco  18560  gsumvallem2  18570  frmdss2  18599  efmndmnd  18625  sgrp2nmndlem4  18664  isgrpd2e  18695  grpinvf1o  18742  grpinvnzcl  18744  dfgrp3  18771  grp1  18779  mhmmnd  18794  ghmgrp  18796  subgmulg  18866  issubg4  18871  0subg  18877  isnsg3  18885  nmzsubg  18890  ssnmz  18891  nmznsg  18893  0nsg  18894  nsgid  18895  ghmnsgima  18955  ghmnsgpreima  18956  ghmf1  18960  ghmf1o  18961  conjnmzb  18966  gicref  18984  gafo  18999  gaid  19002  subgga  19003  gass  19004  gasubg  19005  gastacl  19012  orbsta  19016  cntrsubgnsg  19044  invoppggim  19064  symgextf1  19126  symgextfo  19127  symgextf1o  19128  symgfixf1  19142  symgfixfo  19144  symgfixf1o  19145  f1omvdmvd  19148  pmtrprfv  19158  pmtrdifwrdel2  19191  psgneu  19211  psgnvalfi  19219  psgnfieu  19223  psgnprfval  19226  odf1  19266  dfod2  19268  odf1o1  19274  odf1o2  19275  odhash3  19278  sylow1lem2  19301  sylow2blem2  19323  sylow3lem1  19329  sylow3lem2  19330  pj1eu  19398  efglem  19418  efginvrel2  19429  efgsrel  19436  efgsp1  19439  efgsres  19440  efgredleme  19445  efgrelexlemb  19452  efgredeu  19454  efgcpbllemb  19457  isabld  19496  ghmcmn  19529  ghmabl  19530  invghm  19531  cntrabl  19540  torsubg  19551  prdsabld  19559  qusabl  19562  abl1  19563  iscygd  19583  iscygodd  19584  cycsubmcmn  19585  gsumval3a  19599  gsumval3eu  19600  gsumpt  19658  gsummptf1o  19659  dprdcntz  19706  dprdff  19710  dprdfcntz  19713  dprdfadd  19718  dprdlub  19724  dprd2dlem1  19739  dprd2da  19740  dmdprdpr  19747  dprdpr  19748  ablfacrp  19764  ablfac1eu  19771  pgpfaclem1  19779  pgpfaclem2  19780  ablfaclem3  19785  issimpgd  19791  prmgrpsimpgd  19812  ablsimpgprmd  19813  srgfcl  19846  srglmhm  19866  srgrmhm  19867  iscrngd  19920  ringsrg  19923  prdscrngd  19947  dvdsrmul  19985  1unit  19995  unitmulcl  20001  unitgrp  20004  unitabl  20005  unitnegcl  20018  rhmf1o  20072  rimgim  20078  rhmco  20079  kerf1ghm  20085  rhmdvdsr  20089  elrhmunit  20091  isdrng2  20106  isdrngd  20121  subrgcrng  20133  subrguss  20144  subrgunit  20147  issubdrg  20154  resrhm  20158  fldsdrgfld  20172  subdrgint  20177  primefld  20179  isabvd  20186  srngf1o  20220  issrngd  20227  lssneln0  20320  islmhm2  20406  lmhmf1o  20414  pwssplit1  20427  lmimgim  20433  lsslvec  20475  lspabs3  20489  lspsneq  20490  lspfixed  20496  lspexch  20497  lspsolvlem  20510  islbs3  20523  lbsextlem1  20526  lbsextlem3  20528  lbsextlem4  20529  rlmlvec  20582  lidlnz  20605  quscrng  20617  drnglpir  20630  drngnzr  20639  opprnzr  20642  ringelnzr  20643  subrgnzr  20645  0ringnnzr  20646  unitrrg  20670  domnrrg  20677  opprdomn  20678  drngdomn  20680  fldidomOLD  20683  fidomndrng  20685  cnfldfunALT  20716  xrs1mnd  20742  xrs10  20743  cnmsubglem  20767  gzrngunit  20770  zringunit  20794  prmirredlem  20800  expghm  20803  mulgghm2  20804  domnchr  20842  zncyg  20862  znf1o  20865  zntoslem  20870  znfld  20874  znidomb  20875  cygznlem3  20883  psgnghm  20891  pjfo  21028  frlmlvec  21074  frlmphl  21094  uvcf1  21105  frlmssuvc1  21107  frlmsslsp  21109  frlmup4  21114  lindff1  21133  lindfrn  21134  lsslindf  21143  lmimlbs  21149  indlcim  21153  lmimco  21157  isassad  21177  psrbagcon  21239  psrbagconOLD  21240  gsumbagdiaglemOLD  21247  gsumbagdiagOLD  21248  psrass1lemOLD  21249  gsumbagdiaglem  21250  gsumbagdiag  21251  psrass1lem  21252  psrbas  21253  psrcrng  21288  mvrf1  21300  mplsubrglem  21316  mplsubrg  21317  mvrcl  21327  mpllvec  21331  subrgmvrf  21341  mplmon  21342  mplcoe1  21344  mplbas2  21349  opsrtoslem2  21369  mvrf2  21374  evlseu  21399  ply1sclf1  21566  matinvgcell  21690  mat0dimcrng  21725  mat1dimcrng  21732  mat1rngiso  21741  dmatcrng  21757  scmatcrng  21776  scmatfo  21785  scmatf1  21786  scmatf1o  21787  scmatrngiso  21791  mdetunilem9  21875  invrvald  21931  cpmatsubgpmat  21975  mat2pmatf1  21984  mat2pmatghm  21985  m2cpmfo  22011  m2cpmf1o  22012  m2cpmrngiso  22013  pmatcollpwscmatlem2  22045  pm2mpf1  22054  pm2mpfo  22069  pm2mpf1o  22070  pm2mpgrpiso  22072  pm2mprngiso  22077  chfacfisf  22109  chfacfisfcpmat  22110  chfacfscmul0  22113  chfacfpmmul0  22117  chfacfpmmulgsum2  22120  tgcl  22225  tgtopon  22227  indistopon  22257  fctop  22260  cctop  22262  ppttop  22263  epttop  22265  mretopd  22349  toponmre  22350  neiptopuni  22387  neiptoptop  22388  neiptopnei  22389  resttopon  22418  resttopon2  22425  restfpw  22436  perfopn  22442  ordtrest2  22461  cnco  22523  cnpco  22524  lmss  22555  cnt0  22603  cnt1  22607  cnhaus  22611  isnrm2  22615  isnrm3  22616  isreg2  22634  dnsconst  22635  ordtt1  22636  lmfun  22638  dishaus  22639  cncmp  22649  fincmp  22650  tgcmp  22658  cmpcld  22659  uncmp  22660  sscmp  22662  cmpfi  22665  cnconn  22679  conncn  22683  iunconn  22685  conncompss  22690  2ndc1stc  22708  1stcrest  22710  2ndcdisj  22713  1stcelcls  22718  llynlly  22734  restnlly  22739  restlly  22740  islly2  22741  llyrest  22742  nllyrest  22743  llyidm  22745  nllyidm  22746  hausllycmp  22751  cldllycmp  22752  lly1stc  22753  dislly  22754  comppfsc  22789  kgentopon  22795  llycmpkgen2  22807  1stckgen  22811  ptbasfi  22838  txtopon  22848  pttopon  22853  xkotopon  22857  ptclsg  22872  xkoccn  22876  ptcnplem  22878  uptx  22882  txdis1cn  22892  txlly  22893  txnlly  22894  pthaus  22895  ptrescn  22896  txcmp  22900  txhaus  22904  tx1stc  22907  txkgen  22909  xkohaus  22910  txconn  22946  qtoptop2  22956  qtoptopon  22961  qtopkgen  22967  qtopss  22972  qtopeu  22973  qtopomap  22975  qtopcmap  22976  kqreglem1  22998  kqreglem2  22999  kqnrmlem1  23000  kqnrmlem2  23001  nrmr0reg  23006  hmeocnv  23019  hmeof1o2  23020  hmeores  23028  hmeoco  23029  idhmeo  23030  reghmph  23050  nrmhmph  23051  indishmph  23055  ordthmeolem  23058  ordthmeo  23059  txhmeo  23060  txswaphmeo  23062  pt1hmeo  23063  ptunhmeo  23065  xpstopnlem1  23066  xkohmeo  23072  qtopf1  23073  qtophmeo  23074  isfil2  23113  filconn  23140  isufil2  23165  filssufilg  23168  fixufil  23179  uffixfr  23180  fin1aufil  23189  fmf  23202  fmufil  23216  fclsfnflim  23284  ptcmplem3  23311  ptcmplem4  23312  cnextfun  23321  cnextf  23323  cnextfres  23326  grpinvhmeo  23343  tmdgsum2  23353  tgplacthmeo  23360  symgtgp  23363  clsnsg  23367  tgpconncompeqg  23369  tgpconncomp  23370  tgpt0  23376  qustgpopn  23377  prdstgpd  23382  tsmsfbas  23385  tsmsgsum  23396  tsmsres  23401  tsmsinv  23405  tgptsmscls  23407  tsmsxplem1  23410  tsmsxplem2  23411  tsmsxp  23412  tvclvec  23456  ustfilxp  23470  trust  23487  utoptop  23492  utoptopon  23494  utopreg  23510  ressusp  23522  tususp  23530  psmetxrge0  23572  isxmet2d  23586  metres2  23622  prdsdsf  23626  prdsxmetlem  23627  prdsmet  23629  imasdsf1olem  23632  imasf1oxmet  23634  imasf1omet  23635  xmetresbl  23696  tmsxms  23748  tmsms  23749  imasf1oxms  23751  imasf1oms  23752  blcls  23768  comet  23775  stdbdxmet  23777  stdbdmet  23778  met1stc  23783  ressxms  23787  ressms  23788  prdsxms  23792  prdsms  23793  metustto  23815  xmsusp  23831  nrmmetd  23836  tngngp2  23922  nrgdomn  23941  subrgnrg  23943  tngnrg  23944  sranlm  23954  nrginvrcn  23962  nlmtlm  23964  nvctvc  23970  lssnlm  23971  lssnvc  23972  ngpocelbl  23974  nmhmco  24026  nmhmplusg  24027  qdensere  24039  tgioo  24065  xrtgioo  24075  xrsmopn  24081  reperflem  24087  icccmplem1  24091  icccmplem2  24092  reconnlem2  24096  xrge0tsms  24103  metdsf  24117  metdsre  24122  metnrm  24131  mulc1cncf  24174  icchmeo  24210  icopnfcnv  24211  xrhmeo  24215  cnrehmeo  24222  evth  24228  phtpcer  24264  pcohtpy  24289  pi1xfrgim  24327  cvsdiv  24401  cvsdivcl  24402  cphnvc  24446  cphsubrglem  24447  cphreccllem  24448  tcphcph  24507  clsocv  24520  iscmet3lem1  24561  iscmet3  24563  cmetss  24586  relcmpcmet  24588  bcthlem5  24598  cmetcusp1  24623  cmetcusp  24624  cphssphl  24641  cmscsscms  24643  cssbn  24645  cmslsschl  24647  chlcsschl  24648  rrxmet  24678  rrxbasefi  24680  minveclem7  24705  hlhil  24713  ivthlem1  24721  evthicc2  24730  ovolfsf  24741  ovolunlem1a  24766  ovoliunlem1  24772  ovolicc2lem2  24788  ovolicc2lem4  24790  ovolicc2lem5  24791  cmmbl  24804  nulmbl  24805  nulmbl2  24806  unmbl  24807  shftmbl  24808  voliunlem2  24821  ioombl1  24832  uniioombl  24859  dyadmbllem  24869  volcn  24876  vitalilem2  24879  vitalilem5  24882  mbfconst  24903  cncombf  24928  cnmbf  24929  i1fd  24951  i1fmullem  24964  itg1addlem2  24967  i1fmulc  24974  itg1mulc  24975  mbfi1fseqlem1  24986  mbfi1fseqlem4  24989  mbfi1flimlem  24993  xrge0f  25002  itg2const2  25012  itg2mulclem  25017  itg2mono  25024  itg2i1fseq  25026  itg2addlem  25029  itg2gt0  25031  itg2cnlem2  25033  itg2cn  25034  iblss  25075  itgle  25080  itgeqa  25084  iblconst  25088  itgconst  25089  ibladdlem  25090  itgaddlem1  25093  iblabslem  25098  iblabs  25099  iblabsr  25100  iblmulc2  25101  itgmulc2lem1  25102  itgsplit  25106  bddmulibl  25109  bddiblnc  25112  itggt0  25114  itgcn  25115  limciun  25164  perfdvf  25173  dvfre  25221  dvcnvlem  25246  dvexp3  25248  dvferm1lem  25254  dvferm2lem  25256  c1lip2  25268  dvle  25277  dvne0  25281  lhop1lem  25283  dvfsumrlim  25301  ftc1lem5  25310  ftc1cn  25313  ply1nz  25392  ply1nzb  25393  ply1domn  25394  ply1divalg  25408  fta1blem  25439  fta1b  25440  ig1peu  25442  ig1pdvds  25447  ply1lpir  25449  ply1pid  25450  elplyr  25468  plyeq0  25478  coeeu  25492  dgrub  25501  plyreres  25549  plydivalg  25565  fta1lem  25573  elqaalem3  25587  qaa  25589  aareccl  25592  aannenlem1  25594  aalioulem6  25603  taylfvallem1  25622  taylf  25626  tayl0  25627  dvtaylp  25635  ulmss  25662  mtest  25669  radcnvle  25685  psercnlem2  25689  psercn  25691  abelthlem2  25697  abelthlem8  25704  abelth  25706  pilem2  25717  pilem3  25718  efif1olem4  25807  efifo  25809  eff1olem  25810  logdmss  25903  dvloglem  25909  logf1o2  25911  efopnlem2  25918  logtayl  25921  cxpcn2  26005  cxpcn3  26007  loglesqrt  26017  logreclem  26018  relogbcl  26029  relogbreexp  26031  relogbmul  26033  relogbcxp  26041  atanre  26141  asinneg  26142  atandmneg  26162  atandmcj  26165  atandmtan  26176  bndatandm  26185  atansssdm  26189  areaf  26217  rlimcnp  26221  rlimcnp3  26223  xrlimcnp  26224  amgmlem  26245  amgm  26246  emcllem7  26257  dmlogdmgm  26279  rpdmgm  26280  dmgmaddnn0  26282  lgamgulmlem1  26284  lgamgulmlem2  26285  wilthlem2  26324  wilthlem3  26325  wilth  26326  ftalem3  26330  basellem3  26338  basellem4  26339  ppisval  26359  ppisval2  26360  sgmnncl  26402  chtdif  26413  ppidif  26418  ppinncl  26429  ppiltx  26432  sqff1o  26437  muinv  26448  dvdsmulf1o  26449  logexprlim  26479  mersenne  26481  perfectlem2  26484  dchrfi  26509  dchrghm  26510  dchrabs  26514  dchr1re  26517  bcmono  26531  bposlem3  26540  bposlem4  26541  bposlem5  26542  bposlem6  26543  bposlem9  26546  lgsfcl2  26557  lgsval2lem  26561  lgsmod  26577  lgsdirprm  26585  lgsne0  26589  lgsqrlem2  26601  gausslemma2dlem0h  26617  gausslemma2dlem1a  26619  gausslemma2dlem4  26623  lgseisenlem1  26629  lgseisenlem2  26630  lgsquadlem1  26634  lgsquadlem2  26635  lgsquad2lem2  26639  2sqlem8  26680  2sqlem9  26681  2sqlem11  26683  2sqmod  26690  2sqreulem1  26700  2sqreunnlem1  26703  dchrisumlem2  26744  dchrisumlem3  26745  dchrmusum2  26748  dchrvmasumlem2  26752  dchrvmasumiflem1  26755  dchrvmaeq0  26758  dchrisum0flblem2  26763  dchrisum0re  26767  dchrisum0lem1b  26769  dchrisum0lem2  26772  dirith2  26782  2vmadivsumlem  26794  chpdifbndlem1  26807  selberg3lem1  26811  selberg4lem1  26814  pntrlog2bndlem3  26833  pntpbnd1  26840  pntibndlem2  26845  pntlemo  26861  pntlem3  26863  nofnbday  26906  noxp1o  26917  nosepdmlem  26937  nosupno  26957  nosupbday  26959  nosupfv  26960  nosupbnd1  26968  nosupbnd2  26970  noinfno  26972  noinfbday  26974  noinffv  26975  noinfbnd1  26983  noinfbnd2  26985  nocvxmin  27024  conway  27044  scutun12  27055  etasslt  27058  scutbdaybnd2  27061  scutbdaybnd2lim  27062  scutbdaylt  27063  slerec  27064  tglngval  27201  hlcgreu  27268  tglinethrueu  27289  ragncol  27359  foot  27372  mideu  27388  opptgdim2  27395  hlpasch  27406  trgcopyeu  27456  cgraswap  27470  cgracom  27472  cgratr  27473  flatcgra  27474  dfcgra2  27480  acopyeu  27484  cgrg3col4  27503  f1otrg  27521  f1otrge  27522  xmstrkgc  27542  axlowdimlem13  27611  axlowdimlem15  27613  axlowdimlem16  27614  axcontlem2  27622  axcontlem3  27623  axcontlem4  27624  axcontlem10  27630  eengtrkg  27643  eengtrkge  27644  structiedg0val  27681  upgr1elem  27771  umgrislfupgrlem  27781  edglnl  27802  ausgrumgri  27826  usgredgreu  27874  uspgredg2vtxeu  27876  uspgredg2v  27880  usgredg2v  27883  usgr1e  27901  subgruhgredgd  27940  subuhgr  27942  subupgr  27943  subumgr  27944  subusgr  27945  upgrreslem  27960  upgrres  27962  umgrres  27963  nbumgrvtx  28002  nbgrssovtx  28017  nbupgrres  28020  nbusgrf1o0  28025  uvtxnbgrb  28057  cusgr0v  28084  cplgr1v  28086  cusgr1v  28087  cusgrexilem2  28098  cusgrexi  28099  structtocusgr  28102  cusgrres  28104  cusgrfilem2  28112  vtxdgfisf  28132  umgr2v2evd2  28183  ewlkprop  28259  lfgriswlk  28344  trlres  28356  upgrwlkdvdelem  28392  uhgrwkspth  28411  usgr2wlkspth  28415  pthdlem1  28422  crctcshwlkn0lem7  28469  crctcshtrl  28476  crctcsh  28477  wwlknbp  28495  wspthnp  28503  wlkswwlksf1o  28532  wwlksnext  28546  wwlksnextinj  28552  wwlksnextsurj  28553  wwlksnextbij0  28554  wwlksnextproplem3  28564  2trld  28591  2spthd  28594  umgr2adedgwlk  28598  umgr2adedgwlkon  28599  umgr2adedgwlkonALT  28600  umgr2adedgspth  28601  elwwlks2ons3  28608  clwwlkbp  28637  clwwlkccatlem  28641  clwlkclwwlklem2a2  28645  clwlkclwwlklem2fv2  28648  clwlkclwwlklem2a4  28649  clwlkclwwlkfolem  28659  clwlkclwwlkfo  28661  clwlkclwwlkf1  28662  clwlkclwwlkf1o  28663  clwwlkinwwlk  28692  clwwlkel  28698  clwwlkf1  28701  clwwlkfo  28702  clwwlkf1o  28703  wwlksext2clwwlk  28709  wwlksubclwwlk  28710  clwwnisshclwwsn  28711  clwwlknccat  28715  s2elclwwlknon2  28756  clwwlknonex2lem2  28760  clwwlknonex2e  28762  lp1cycl  28804  3trld  28824  3spthd  28828  3cycld  28830  eupthp1  28868  eupth2eucrct  28869  frgr1v  28923  nfrgr2v  28924  3vfriswmgrlem  28929  n4cyclfrgr  28943  frgrncvvdeqlem8  28958  frgrncvvdeqlem9  28959  frgrncvvdeqlem10  28960  frgrwopreglem5  28973  clwwnonrepclwwnon  28997  numclwwlk1lem2f1  29009  numclwwlk1lem2fo  29010  numclwwlk1lem2f1o  29011  numclwlk2lem2f1o  29031  nvex  29261  isnv  29262  isblo3i  29451  ipblnfi  29505  ubthlem2  29521  minvecolem7  29533  htthlem  29567  hlimadd  29843  hhsscms  29928  ocsh  29933  occl  29954  pjhthlem2  30042  pjhtheu  30044  pjpreeq  30048  ococin  30058  chscllem2  30288  chscl  30291  unopf1o  30566  cnvunop  30568  unoplin  30570  counop  30571  hmopadj2  30591  hmoplin  30592  bralnfn  30598  lnopmi  30650  unopbd  30665  hmops  30670  hmopm  30671  hmopco  30673  bdophmi  30682  nlelshi  30710  nlelchi  30711  riesz3i  30712  cnlnadjlem2  30718  adjlnop  30736  hmopidmpji  30802  pjclem4  30849  pj3si  30857  h1da  30999  shatomistici  31011  iundisjf  31213  f1o3d  31247  2ndresdju  31271  2ndresdjuf1o  31272  xppreima2  31273  isoun  31319  f1od2  31341  xrge0infss  31368  xrge0addcld  31370  xrofsup  31375  difioo  31388  fzsplit3  31400  iundisjfi  31402  subne0nn  31420  xreceu  31481  s3f1  31506  ccatf1  31508  swrdf1  31513  posrasymb  31528  resspos  31529  resstos  31530  odutos  31531  mgcf1o  31566  abliso  31590  gsumpart  31600  xrge0tsmsd  31602  cntrcrng  31607  pmtrcnel  31643  pmtrcnelor  31645  cycpmfv2  31666  cycpmcl  31668  cycpmco2lem4  31681  tocyccntz  31696  archiabllem1  31732  archiabllem2c  31734  archiabllem2  31736  suborng  31812  subofld  31813  0nellinds  31861  lindssn  31868  nsgmgc  31892  qsidomlem2  31924  fply1  31962  sradrng  31969  sralvec  31971  rgmoddim  31989  matdim  31994  lmhmlvec2  31998  dimkerim  32004  fedgmul  32008  extdg1id  32034  qtopt1  32081  qtophaus  32082  locfinreflem  32086  cmppcmp  32104  dispcmp  32105  zarmxt1  32126  pstmxmet  32143  xpinpreima2  32153  tpr2rico  32158  ordtrest2NEW  32169  xrmulc1cn  32176  zrhnm  32215  indf1ofs  32290  hashf2  32348  hasheuni  32349  esumcvg  32350  prsiga  32395  pwldsys  32421  ldsysgenld  32424  ldgenpisyslem1  32427  sxsigon  32456  measdivcstALTV  32489  volfiniune  32494  imambfm  32527  dya2iocnrect  32546  omssubaddlem  32564  sibfof  32605  sitgf  32612  oddpwdc  32619  eulerpartlemb  32633  eulerpartlemgvv  32641  sseqmw  32656  sseqf  32657  sseqp1  32660  fibp1  32666  prob01  32678  probfinmeasb  32693  probfinmeasbALTV  32694  probmeasb  32695  dstrvprob  32736  dstfrvel  32738  ballotlemic  32771  ballotlem1c  32772  ballotlemro  32787  ballotlemrc  32795  ballotlemirc  32796  ballotth  32802  plymulx0  32824  signstfvn  32846  signstfvcl  32850  signstfveq0a  32853  signstfveq0  32854  fdvposlt  32877  reprpmtf1o  32904  tgoldbachgnn  32937  bnj951  33052  bnj1379  33107  bnj1422  33114  bnj149  33152  bnj151  33154  bnj908  33208  bnj944  33215  bnj970  33224  bnj1006  33237  bnj1177  33283  bnj1189  33286  bnj1321  33304  bnj1398  33311  bnj1417  33318  bnj1523  33348  srcmpltd  33351  f1resrcmplf1d  33356  pthhashvtx  33386  2cycld  33397  subfacp1lem3  33441  subfacp1lem5  33443  erdszelem8  33457  erdszelem9  33458  cnpconn  33489  txpconn  33491  ptpconn  33492  connpconn  33494  sconnpi1  33498  txsconn  33500  cvxpconn  33501  cvxsconn  33502  iccllysconn  33509  cvmseu  33535  cvmfolem  33538  cvmliftmolem2  33541  cvmliftlem14  33556  cvmlift2lem9a  33562  cvmlift2lem12  33573  cvmlift2lem13  33574  cvmlift3  33587  satfdm  33628  fmla1  33646  fmlaomn0  33649  fmlasucdisj  33658  satff  33669  sategoelfvb  33678  mvrsfpw  33765  mrsubrn  33772  mrsubff1  33773  msubff  33789  msubff1  33815  mvhf1  33818  mclsssvlem  33821  mclsind  33829  mthmpps  33841  lediv2aALT  33932  dfon2  34051  poxp2  34072  frxp2  34073  poxp3  34078  frxp3  34079  cofonr  34112  naddunif  34129  sltlpss  34195  cofcutr  34200  addsval  34227  addsproplem2  34234  addsproplem4  34236  addsproplem5  34237  addsproplem6  34238  addsunif  34256  dfrdg4  34390  altxpsspw  34416  segconeu  34450  btwnconn1lem13  34538  btwnconn1lem14  34539  outsideofeu  34570  outsidele  34571  linerflx1  34588  linethrueu  34595  fwddifval  34601  fwddifnval  34602  nn0prpwlem  34648  neibastop1  34685  neibastop2lem  34686  topjoin  34691  fnemeet1  34692  fnemeet2  34693  fnejoin1  34694  fnejoin2  34695  filnetlem3  34706  onsuctopon  34760  bj-nnfim  35065  bj-nnfand  35068  bj-nnford  35070  bj-dfnnf3  35076  bj-nnfalt  35085  bj-nnfext  35086  bj-elgab  35263  relowlssretop  35688  elxp8  35696  finorwe  35707  finxp1o  35717  pibt2  35742  finixpnum  35916  fin2solem  35917  fin2so  35918  lindsadd  35924  lindsdom  35925  lindsenlbs  35926  ptrecube  35931  poimirlem4  35935  poimirlem7  35938  poimirlem13  35944  poimirlem15  35946  poimirlem16  35947  poimirlem17  35948  poimirlem18  35949  poimirlem19  35950  poimirlem20  35951  poimirlem21  35952  poimirlem24  35955  poimirlem26  35957  poimirlem27  35958  poimirlem29  35960  poimirlem30  35961  poimirlem31  35962  poimirlem32  35963  opnmbllem0  35967  mblfinlem2  35969  itg2gt0cn  35986  ibladdnclem  35987  itgaddnclem1  35989  iblabsnclem  35994  iblabsnc  35995  iblmulc2nc  35996  itgmulc2nclem1  35997  itggt0cn  36001  ftc1cnnc  36003  ftc1anclem3  36006  ftc1anclem4  36007  ftc1anclem5  36008  ftc1anclem6  36009  ftc1anclem7  36010  ftc1anclem8  36011  ftc1anc  36012  areacirclem2  36020  areacirc  36024  unirep  36025  sdclem1  36055  mettrifi  36069  istotbnd3  36083  sstotbnd2  36086  sstotbnd  36087  sstotbnd3  36088  equivtotbnd  36090  isbndx  36094  isbnd3  36096  blbnd  36099  equivbnd  36102  prdsbnd  36105  prdstotbnd  36106  ismtyhmeo  36117  heibor1  36122  heibor  36133  bfp  36136  rrnmet  36141  rrncmslem  36144  rrnequiv  36147  ismrer1  36150  iccbnd  36152  opidonOLD  36164  grpokerinj  36205  isgrpda  36267  isdrngo2  36270  iscringd  36310  crngohomfo  36318  smprngopr  36364  prnc  36379  isfldidl  36380  petlem  37128  prter3  37198  lshpnelb  37300  lsatspn0  37316  lsatssn0  37318  lssats  37328  lsatcv0  37347  lsat0cv  37349  islshpcv  37369  lkr0f  37410  lshpsmreu  37425  lduallvec  37470  lkrlspeqN  37487  cdleme50f1  38860  cdleme50f1o  38863  cdleme  38877  cdlemk56  39288  dvalveclem  39342  dvhlveclem  39425  dvheveccl  39429  cdlemm10N  39435  diaf1oN  39447  dihord4  39575  dihf11lem  39583  dihf11  39584  dihglblem2N  39611  dihglb2  39659  dochvalr  39674  doch2val2  39681  dochocss  39683  dochsat  39700  dochshpncl  39701  dochnel  39710  dvh4dimlem  39760  dochsnkr2cl  39791  dochkr1  39795  lcfl6lem  39815  lcfl9a  39822  lclkrlem1  39823  lclkrlem2l  39835  lclkrlem2o  39838  lclkrlem2q  39840  lclkr  39850  lclkrslem1  39854  lclkrslem2  39855  lcfrlem9  39867  lcfrlem16  39875  lcfrlem17  39876  lcfrlem27  39886  lcfrlem37  39896  lcfrlem38  39897  lcfrlem40  39899  lcdlkreqN  39939  mapdordlem2  39954  mapdrvallem2  39962  mapdn0  39986  mapdpglem20  40008  mapdpglem30  40019  mapdpglem32  40022  mapdpg  40023  mapdindp0  40036  mapdh6aN  40052  mapdh6eN  40057  mapdh6kN  40063  hdmaplem4  40091  hdmap1val  40115  hdmap1l6a  40126  hdmap1l6e  40131  hdmap1l6k  40137  hdmapval3N  40155  hdmap11lem2  40159  hdmapnzcl  40162  hdmaprnlem3eN  40175  hdmap14lem4a  40188  hdmap14lem6  40190  hdmap14lem7  40191  hgmapvvlem2  40241  hgmapvvlem3  40242  hlhilhillem  40281  lcmineqlem15  40354  aks4d1p1  40387  aks4d1p3  40389  xppss12  40505  selvval2lem4  40531  rncrhmcl  40549  frlmsnic  40572  evlsbagval  40584  mhpind  40592  mhphf  40594  posqsqznn  40652  addinvcom  40722  prjspersym  40755  0prjspnlem  40771  dffltz  40782  flt0  40785  flt4lem5e  40804  isnacs3  40843  mzpindd  40879  eldioph  40891  eldioph3  40899  rencldnfilem  40953  irrapxlem1  40955  irrapxlem4  40958  irrapxlem6  40960  pellexlem5  40966  pellfundlb  41017  rmspecnonsq  41040  rmxnn  41085  rmynn  41090  rmynn0  41091  jm2.22  41129  jm2.23  41130  jm2.20nn  41131  jm2.27a  41139  jm2.27c  41141  rmydioph  41148  jm3.1lem3  41153  dford3lem1  41160  rpnnen3lem  41165  harinf  41168  wepwsolem  41179  dnnumch3  41184  fnwe2lem2  41188  fnwe2  41190  dfac11  41199  lnmlsslnm  41218  lnmepi  41222  lmhmlnmsplit  41224  pwssplit4  41226  filnm  41227  imasgim  41237  harn0  41239  lpirlnr  41254  hbtlem7  41262  hbtlem6  41266  hbt  41267  dgraaub  41285  mpaaeu  41287  aaitgo  41299  rgspnmin  41308  proot1ex  41338  deg1mhm  41344  omabs2  41367  ofoafo  41372  naddcnffo  41380  fzunt  41434  fzuntd  41435  fzunt1d  41436  fzuntgd  41437  omssrncard  41519  fiinfi  41552  cotrclrcl  41721  fsovf1od  41995  ntrk2imkb  42018  ntrf  42104  gneispacef2  42117  rr-phpd  42192  expgrowth  42324  binomcxplemdvbinom  42342  binomcxplemnotnn0  42345  ordelordALT  42528  2uasbanh  42552  rfcnnnub  42950  elixpconstg  43009  ssrabdf  43035  wessf1ornlem  43099  disjinfi  43108  projf1o  43113  fconst7  43190  fzisoeu  43224  monoordxrv  43407  iccshift  43442  iooshift  43446  fmul01lt1lem2  43512  ellimciota  43541  mullimc  43543  mullimcf  43550  sumnnodd  43557  addlimc  43575  liminfval2  43695  liminflimsupxrre  43744  icccncfext  43814  dvcosre  43839  dvdivbd  43850  dvdivcncf  43854  ioodvbdlimc1lem2  43859  ioodvbdlimc2lem  43861  itgsinexplem1  43881  iblcncfioo  43905  itgperiod  43908  stoweidlem7  43934  stoweidlem14  43941  stoweidlem16  43943  stoweidlem26  43953  stoweidlem27  43954  stoweidlem31  43958  stoweidlem34  43961  stoweidlem36  43963  stoweidlem46  43973  stoweidlem47  43974  stoweidlem52  43979  stoweidlem57  43984  stoweidlem59  43986  stoweidlem60  43987  wallispilem3  43994  wallispilem4  43995  dirkertrigeqlem3  44027  dirkeritg  44029  dirkercncf  44034  fourierdlem15  44049  fourierdlem20  44054  fourierdlem25  44059  fourierdlem34  44068  fourierdlem37  44071  fourierdlem41  44075  fourierdlem42  44076  fourierdlem47  44080  fourierdlem48  44081  fourierdlem51  44084  fourierdlem52  44085  fourierdlem57  44090  fourierdlem58  44091  fourierdlem59  44092  fourierdlem63  44096  fourierdlem64  44097  fourierdlem65  44098  fourierdlem68  44101  fourierdlem79  44112  fourierdlem80  44113  fourierdlem81  44114  fourierdlem92  44125  fourierdlem104  44137  fourierdlem111  44144  fouriersw  44158  etransclem3  44164  etransclem7  44168  etransclem10  44171  etransclem15  44176  etransclem19  44180  etransclem20  44181  etransclem21  44182  etransclem22  44183  etransclem24  44185  etransclem25  44186  etransclem27  44188  etransclem28  44189  etransclem35  44196  etransclem44  44205  etransclem48  44209  nnfoctbdjlem  44380  preimagelt  44624  preimalegt  44625  fnresfnco  44951  funressnfv  44953  fsetsnf1  44962  fsetsnfo  44963  fsetsnf1o  44964  cfsetsnfsetf1  44969  cfsetsnfsetfo  44970  cfsetsnfsetf1o  44971  fcoresf1  44979  ffnafv  45079  rlimdmafv  45085  dfatco  45164  rlimdmafv2  45166  zm1nn  45210  eluzge0nn0  45220  2elfz2melfz  45226  subsubelfzo0  45234  smonoord  45239  setsnidel  45245  imasetpreimafvbijlemf1  45272  imasetpreimafvbijlemfo  45273  imasetpreimafvbij  45274  iccpartigtl  45291  iccpartgt  45295  iccpartf  45299  icceuelpart  45304  fargshiftf1  45309  fargshiftfo  45310  sprsymrelfolem2  45361  sprsymrelfo  45365  sprsymrelf1o  45366  prproropf1o  45375  sfprmdvdsmersenne  45471  lighneallem4  45478  evenm1odd  45507  evenp1odd  45508  oddp1eveni  45509  oddm1eveni  45510  m2even  45522  oexpnegALTV  45545  opoeALTV  45551  opeoALTV  45552  oddprmALTV  45555  nnoALTV  45563  nn0oALTV  45564  nnpw2evenALTV  45570  perfectALTVlem2  45590  perfectALTV  45591  sbgoldbalt  45649  wtgoldbnnsum4prm  45670  bgoldbnnsum3prm  45672  isomuspgrlem2c  45698  isomuspgrlem2d  45699  isomuspgrlem2e  45700  1hegrlfgr  45710  uspgrsprfo  45726  uspgrsprf1o  45727  mgmhmf1o  45757  idmgmhm  45758  resmgmhm  45768  resmgmhm2  45769  resmgmhm2b  45770  mgmhmco  45771  mgmhmeql  45773  copissgrp  45778  isrnghm2d  45875  rnghmf1o  45877  rnghmco  45881  idrnghm  45882  c0mgm  45883  c0rhm  45886  c0rnghm  45887  c0snmgmhm  45888  c0snmhm  45889  zrrnghm  45891  lidlmsgrp  45900  zlidlring  45902  2zlidl  45908  2zrngamgm  45913  2zrngagrp  45917  2zrngmmgm  45920  rngcinv  45955  rngcinvALTV  45967  ringcinv  46006  ringcinvALTV  46030  nn0eo  46290  blennnelnn  46338  nnpw2blen  46342  dignn0fr  46363  dignn0ldlem  46364  dig2nn1st  46367  1arymaptf1  46404  1arymaptfo  46405  1arymaptf1o  46406  2arymaptf1  46415  2arymaptfo  46416  2arymaptf1o  46417  inlinecirc02p  46549  toslat  46684  topdlat  46706  isthincd  46734  fullthinc  46743  thincfth  46745  thincciso  46746  0thincg  46747  aacllem  46921