Theorem sylanbrc 582

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

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

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 396

This theorem is referenced by:  sylanblrc  589  ifpimpda  1079  ecase23d  1471  raleqbidvv  3329  elrabd  3619  eqeu  3636  euind  3654  reuind  3683  eldifd  3894  eqssd  3934  ssrabdv  4003  psstr  4035  elind  4124  elpwdifsn  4719  prproe  4834  propeqop  5415  issod  5527  wereu  5576  wereu2  5577  relssdmrn  6161  predtrss  6214  ordelord  6273  funun  6464  fnsng  6470  fnprg  6477  fntpg  6478  fununi  6493  fncoOLD  6534  f00  6640  f1ss  6660  f1ssr  6661  f1ssres  6662  focofo  6685  f1f1orn  6711  foimacnv  6717  foun  6718  f1oprswap  6743  rescnvimafod  6933  fvn0ssdmfun  6934  dff3  6958  fmpt  6966  ffnfv  6974  fmpt2d  6979  ffvresb  6980  fprb  7051  fpr2g  7069  nvof1o  7133  fcof1  7139  fcofo  7140  fcof1od  7146  fliftf  7166  soisores  7178  soisoi  7179  isoini2  7190  f1oiso  7202  moriotass  7245  fnoprabg  7375  f1ocnvd  7498  fiun  7759  f1iun  7760  1stcof  7834  2ndcof  7835  1stconst  7911  2ndconst  7912  curry1  7915  curry2  7918  fo2ndf  7933  f1o2ndf1  7934  soxp  7941  wexp  7942  fnwelem  7943  suppssov1  7985  suppssfv  7989  fpr1  8090  wfrlem10OLD  8120  smores2  8156  smo11  8166  smoiso2  8171  tfrlem12  8191  tfrlem13  8192  oalimcl  8353  oaf1o  8356  omlimcl  8371  omeu  8378  oeeulem  8394  oeeui  8395  omsmo  8448  eroveu  8559  fsetfocdm  8607  undifixp  8680  resixpfo  8682  elixpsn  8683  dom2lem  8735  difsnen  8794  omxpenlem  8813  sucdom2  8822  sdomdomtr  8846  domsdomtr  8848  fodomr  8864  xpf1o  8875  php2  8898  php3  8899  phpeqd  8902  ssfi  8918  unxpdomlem3  8958  f1finf1o  8975  frfi  8989  wofi  8993  nnsdomg  9003  domunfican  9017  fofinf1o  9024  mapfienlem3  9096  mapfien  9097  marypha1lem  9122  supeu  9143  infeu  9185  ordtypelem2  9208  ordtypelem4  9210  ordtypelem10  9216  oismo  9229  wemaplem2  9236  card2inf  9244  brwdom2  9262  wdom2d  9269  harwdom  9280  cantnfp1lem2  9367  cantnfp1lem3  9368  cantnflem1  9377  cantnflem2  9378  cantnf  9381  cnfcom2lem  9389  cnfcom3lem  9391  frr1  9448  tskwe  9639  cardsdomelir  9662  cardprclem  9668  cardmin2  9688  en2other2  9696  r0weon  9699  infxpenc  9705  fseqenlem1  9711  fseqenlem2  9712  fodomacn  9743  infpwfien  9749  finnisoeu  9800  iunfictbso  9801  dfac12lem2  9831  cofsmo  9956  cfsmolem  9957  alephsing  9963  sornom  9964  infpssrlem3  9992  infpssrlem5  9994  ssfin4  9997  isfin4p1  10002  fincssdom  10010  fin23lem23  10013  fin23lem28  10027  fin23lem31  10030  fin23lem34  10033  isf32lem9  10048  compssiso  10061  fin1a2lem12  10098  hsmexlem1  10113  hsmexlem4  10116  domtriomlem  10129  cardmin  10251  smobeth  10273  gchen1  10312  gchen2  10313  fpwwe2lem10  10327  fpwwe2lem11  10328  fpwwe2lem12  10329  fpwwe2  10330  canthnum  10336  canthwe  10338  canthp1lem2  10340  canthp1  10341  pwfseqlem5  10350  gchdjuidm  10355  gchxpidm  10356  gchhar  10366  r1wunlim  10424  inar1  10462  inatsk  10465  r1tskina  10469  gruiun  10486  gruima  10489  gruina  10505  addclpi  10579  mulclpi  10580  nqereu  10616  dmrecnq  10655  genpcl  10695  suplem1pr  10739  receu  11550  recgt0  11751  cju  11899  peano5nni  11906  nn0n0n1ge2  12230  nn0ge2m1nn  12232  nnnegz  12252  elnnz  12259  nnssz  12270  msqznn  12332  eluzaddi  12540  eluzsubi  12541  uz2mulcl  12595  elq  12619  nnrp  12670  rpaddcl  12681  rpmulcl  12682  rpdivcl  12684  rpgecl  12687  ge0p1rp  12690  elrpd  12698  nn0rp0  13116  ge0addcl  13121  ge0mulcl  13122  ge0xaddcl  13123  ge0xmulcl  13124  icoshftf1o  13135  xnn0xrge0  13167  peano2fzr  13198  uzsubsubfz  13207  fzsplit2  13210  elfznn  13214  fzss1  13224  fzss2  13225  fzp1elp1  13238  elfz1b  13254  elfz0fzfz0  13290  fz0fzelfz0  13291  difelfznle  13299  elfzofz  13331  prinfzo0  13354  nn0p1elfzo  13358  fzosplitsnm1  13390  ubmelm1fzo  13411  fzofzp1b  13413  elfznelfzo  13420  fzosplitsn  13423  injresinj  13436  flge0nn0  13468  flge1nn  13469  zmodcl  13539  modmuladdnn0  13563  modsumfzodifsn  13592  seqcl2  13669  seqf2  13670  seqfveq2  13673  monoord  13681  seqid2  13697  expcl2lem  13722  expclzlem  13734  zsqcl2  13784  bcval4  13949  bcn1  13955  bccl2  13965  hashnn0n0nn  14034  hashfun  14080  seqcoll  14106  ccatsymb  14215  ccatrn  14222  ccat2s1fvw  14277  ccat2s1fvwOLD  14278  swrds1  14307  swrdccat2  14310  swrdccatin2  14370  pfxccatin12lem2  14372  pfxccatin12lem3  14373  pfxccatin12  14374  pfxccat3  14375  pfxccat3a  14379  spllen  14395  splfv2a  14397  splval2  14398  repswswrd  14425  cshwidxmod  14444  cshwcsh2id  14469  pfx2  14588  2swrd2eqwrdeq  14594  wwlktovfo  14601  wwlktovf1o  14602  shftfn  14712  shftf  14718  sqrlem2  14883  sqrlem7  14888  resqreu  14892  sqrtneg  14907  nn0abscl  14952  nnabscl  14965  abs2dif  14972  sqreu  15000  limsupval2  15117  climuni  15189  2clim  15209  climcn2  15230  rlimdiv  15285  isercolllem2  15305  isercolllem3  15306  isercoll  15307  isercoll2  15308  iseralt  15324  summolem2a  15355  mptfzshft  15418  fsum0diag2  15423  fsumge0  15435  climcndslem1  15489  mertenslem1  15524  ntrivcvgmul  15542  prodmolem2a  15572  fprodser  15587  fprodeq0  15613  fprodge0  15631  binomrisefac  15680  eff2  15736  tanval  15765  rpnnen2lem9  15859  sqrt2irrlem  15885  fzo0dvdseq  15960  oexpneg  15982  oddge22np1  15986  evennn02n  15987  evennn2n  15988  nno  16019  divalglem5  16034  bitsfzolem  16069  bitsinv1lem  16076  bitsinv2  16078  bitsf1ocnv  16079  bitsinvp1  16084  sadcaddlem  16092  sadadd2lem  16094  sadadd3  16096  sadasslem  16105  sadeq  16107  gcdcllem3  16136  divgcdz  16146  sqgcd  16198  lcmneg  16236  lcmfunsnlem2lem2  16272  prmind2  16318  sqnprm  16335  isprm5  16340  isprm6  16347  qgt0numnn  16383  crth  16407  phimullem  16408  eulerthlem1  16410  eulerthlem2  16411  hashgcdlem  16417  oddprm  16439  pythagtriplem6  16450  pythagtriplem11  16454  pythagtriplem13  16456  pythagtriplem19  16462  iserodd  16464  pclem  16467  pcpremul  16472  pceu  16475  pc2dvds  16508  difsqpwdvds  16516  pcadd  16518  oddprmdvds  16532  pockthlem  16534  pockthg  16535  prmreclem3  16547  1arith  16556  4sqlem11  16584  4sqlem12  16585  4sqlem13  16586  4sqlem14  16587  4sqlem17  16590  vdwlem2  16611  vdwlem8  16617  vdwlem12  16621  ramtlecl  16629  ramub1lem1  16655  prmgaplem4  16683  prmgaplem7  16686  cshwshashlem2  16726  cshwrepswhash1  16732  imasaddfnlem  17156  imasaddflem  17158  imasvscafn  17165  imasvscaf  17167  isacs1i  17283  mreacs  17284  catideu  17301  invfun  17393  invf  17397  invf1o  17398  issubc3  17480  cofucl  17519  funcres2c  17533  ffthf1o  17551  fulloppc  17554  fthoppc  17555  ffthoppc  17556  idffth  17565  cofull  17566  cofth  17567  ressffth  17570  initoeu2lem2  17646  setcmon  17718  setcepi  17719  catciso  17742  fthestrcsetc  17783  fullestrcsetc  17784  embedsetcestrclem  17790  fthsetcestrc  17798  fullsetcestrc  17799  hofcllem  17892  hofcl  17893  yonedalem3  17914  yonffthlem  17916  yoniso  17919  poslubd  18046  lubun  18148  isacs5  18181  acsfiindd  18186  mreclatBAD  18196  psss  18213  cnvtsr  18221  mgmsscl  18246  gsumval2  18285  sgrp0  18297  sgrp1  18299  hashfinmndnn  18317  ismndd  18322  mndpfo  18323  mnd1  18341  mhmf1o  18355  0mhm  18373  resmhm  18374  resmhm2  18375  resmhm2b  18376  mhmco  18377  gsumvallem2  18387  frmdss2  18417  efmndmnd  18443  sgrp2nmndlem4  18482  isgrpd2e  18513  grpinvf1o  18560  grpinvnzcl  18562  dfgrp3  18589  grp1  18597  mhmmnd  18612  ghmgrp  18614  subgmulg  18684  issubg4  18689  0subg  18695  isnsg3  18703  nmzsubg  18708  ssnmz  18709  nmznsg  18711  0nsg  18712  nsgid  18713  ghmnsgima  18773  ghmnsgpreima  18774  ghmf1  18778  ghmf1o  18779  conjnmzb  18784  gicref  18802  gafo  18817  gaid  18820  subgga  18821  gass  18822  gasubg  18823  gastacl  18830  orbsta  18834  cntrsubgnsg  18862  invoppggim  18882  symgextf1  18944  symgextfo  18945  symgextf1o  18946  symgfixf1  18960  symgfixfo  18962  symgfixf1o  18963  f1omvdmvd  18966  pmtrprfv  18976  pmtrdifwrdel2  19009  psgneu  19029  psgnvalfi  19037  psgnfieu  19041  psgnprfval  19044  odf1  19084  dfod2  19086  odf1o1  19092  odf1o2  19093  odhash3  19096  sylow1lem2  19119  sylow2blem2  19141  sylow3lem1  19147  sylow3lem2  19148  pj1eu  19217  efglem  19237  efginvrel2  19248  efgsrel  19255  efgsp1  19258  efgsres  19259  efgredleme  19264  efgrelexlemb  19271  efgredeu  19273  efgcpbllemb  19276  isabld  19315  ghmcmn  19348  ghmabl  19349  invghm  19350  cntrabl  19359  torsubg  19370  prdsabld  19378  qusabl  19381  abl1  19382  iscygd  19402  iscygodd  19403  cycsubmcmn  19404  gsumval3a  19419  gsumval3eu  19420  gsumpt  19478  gsummptf1o  19479  dprdcntz  19526  dprdff  19530  dprdfcntz  19533  dprdfadd  19538  dprdlub  19544  dprd2dlem1  19559  dprd2da  19560  dmdprdpr  19567  dprdpr  19568  ablfacrp  19584  ablfac1eu  19591  pgpfaclem1  19599  pgpfaclem2  19600  ablfaclem3  19605  issimpgd  19611  prmgrpsimpgd  19632  ablsimpgprmd  19633  srgfcl  19666  srglmhm  19686  srgrmhm  19687  iscrngd  19740  ringsrg  19743  prdscrngd  19767  dvdsrmul  19805  1unit  19815  unitmulcl  19821  unitgrp  19824  unitabl  19825  unitnegcl  19838  rhmf1o  19891  rimgim  19895  rhmco  19896  kerf1ghm  19902  isdrng2  19916  isdrngd  19931  subrgcrng  19943  subrguss  19954  subrgunit  19957  issubdrg  19964  resrhm  19968  subdrgint  19986  primefld  19988  isabvd  19995  srngf1o  20029  issrngd  20036  lssneln0  20129  islmhm2  20215  lmhmf1o  20223  pwssplit1  20236  lmimgim  20242  lsslvec  20284  lspabs3  20298  lspsneq  20299  lspfixed  20305  lspexch  20306  lspsolvlem  20319  islbs3  20332  lbsextlem1  20335  lbsextlem3  20337  lbsextlem4  20338  rlmlvec  20389  lidlnz  20412  quscrng  20424  drnglpir  20437  drngnzr  20446  opprnzr  20449  ringelnzr  20450  subrgnzr  20452  0ringnnzr  20453  unitrrg  20477  domnrrg  20484  opprdomn  20485  drngdomn  20487  fldidomOLD  20490  fidomndrng  20492  xrs1mnd  20548  xrs10  20549  cnmsubglem  20573  gzrngunit  20576  zringunit  20600  prmirredlem  20606  expghm  20609  mulgghm2  20610  domnchr  20648  zncyg  20668  znf1o  20671  zntoslem  20676  znfld  20680  znidomb  20681  cygznlem3  20689  psgnghm  20697  pjfo  20832  frlmlvec  20878  frlmphl  20898  uvcf1  20909  frlmssuvc1  20911  frlmsslsp  20913  frlmup4  20918  lindff1  20937  lindfrn  20938  lsslindf  20947  lmimlbs  20953  indlcim  20957  lmimco  20961  isassad  20981  psrbagcon  21043  psrbagconOLD  21044  gsumbagdiaglemOLD  21051  gsumbagdiagOLD  21052  psrass1lemOLD  21053  gsumbagdiaglem  21054  gsumbagdiag  21055  psrass1lem  21056  psrbas  21057  psrcrng  21092  mvrf1  21104  mplsubrglem  21120  mplsubrg  21121  mvrcl  21131  mpllvec  21135  subrgmvrf  21145  mplmon  21146  mplcoe1  21148  mplbas2  21153  opsrtoslem2  21173  mvrf2  21178  evlseu  21203  ply1sclf1  21370  matinvgcell  21492  mat0dimcrng  21527  mat1dimcrng  21534  dmatcrng  21559  scmatcrng  21578  scmatfo  21587  scmatf1  21588  scmatf1o  21589  mdetunilem9  21677  invrvald  21733  cpmatsubgpmat  21777  mat2pmatf1  21786  mat2pmatghm  21787  m2cpmfo  21813  m2cpmf1o  21814  pmatcollpwscmatlem2  21847  pm2mpf1  21856  pm2mpfo  21871  pm2mpf1o  21872  pm2mpgrpiso  21874  chfacfisf  21911  chfacfisfcpmat  21912  chfacfscmul0  21915  chfacfpmmul0  21919  chfacfpmmulgsum2  21922  tgcl  22027  tgtopon  22029  indistopon  22059  fctop  22062  cctop  22064  ppttop  22065  epttop  22067  mretopd  22151  toponmre  22152  neiptopuni  22189  neiptoptop  22190  neiptopnei  22191  resttopon  22220  resttopon2  22227  restfpw  22238  perfopn  22244  ordtrest2  22263  cnco  22325  cnpco  22326  lmss  22357  cnt0  22405  cnt1  22409  cnhaus  22413  isnrm2  22417  isnrm3  22418  isreg2  22436  dnsconst  22437  ordtt1  22438  lmfun  22440  dishaus  22441  cncmp  22451  fincmp  22452  tgcmp  22460  cmpcld  22461  uncmp  22462  sscmp  22464  cmpfi  22467  cnconn  22481  conncn  22485  iunconn  22487  conncompss  22492  2ndc1stc  22510  1stcrest  22512  2ndcdisj  22515  1stcelcls  22520  llynlly  22536  restnlly  22541  restlly  22542  islly2  22543  llyrest  22544  nllyrest  22545  llyidm  22547  nllyidm  22548  hausllycmp  22553  cldllycmp  22554  lly1stc  22555  dislly  22556  comppfsc  22591  kgentopon  22597  llycmpkgen2  22609  1stckgen  22613  ptbasfi  22640  txtopon  22650  pttopon  22655  xkotopon  22659  ptclsg  22674  xkoccn  22678  ptcnplem  22680  uptx  22684  txdis1cn  22694  txlly  22695  txnlly  22696  pthaus  22697  ptrescn  22698  txcmp  22702  txhaus  22706  tx1stc  22709  txkgen  22711  xkohaus  22712  txconn  22748  qtoptop2  22758  qtoptopon  22763  qtopkgen  22769  qtopss  22774  qtopeu  22775  qtopomap  22777  qtopcmap  22778  kqreglem1  22800  kqreglem2  22801  kqnrmlem1  22802  kqnrmlem2  22803  nrmr0reg  22808  hmeocnv  22821  hmeof1o2  22822  hmeores  22830  hmeoco  22831  idhmeo  22832  reghmph  22852  nrmhmph  22853  indishmph  22857  ordthmeolem  22860  ordthmeo  22861  txhmeo  22862  txswaphmeo  22864  pt1hmeo  22865  ptunhmeo  22867  xpstopnlem1  22868  xkohmeo  22874  qtopf1  22875  qtophmeo  22876  isfil2  22915  filconn  22942  isufil2  22967  filssufilg  22970  fixufil  22981  uffixfr  22982  fin1aufil  22991  fmf  23004  fmufil  23018  fclsfnflim  23086  ptcmplem3  23113  ptcmplem4  23114  cnextfun  23123  cnextf  23125  cnextfres  23128  grpinvhmeo  23145  tmdgsum2  23155  tgplacthmeo  23162  symgtgp  23165  clsnsg  23169  tgpconncompeqg  23171  tgpconncomp  23172  tgpt0  23178  qustgpopn  23179  prdstgpd  23184  tsmsfbas  23187  tsmsgsum  23198  tsmsres  23203  tsmsinv  23207  tgptsmscls  23209  tsmsxplem1  23212  tsmsxplem2  23213  tsmsxp  23214  tvclvec  23258  ustfilxp  23272  trust  23289  utoptop  23294  utoptopon  23296  utopreg  23312  ressusp  23324  tususp  23332  psmetxrge0  23374  isxmet2d  23388  metres2  23424  prdsdsf  23428  prdsxmetlem  23429  prdsmet  23431  imasdsf1olem  23434  imasf1oxmet  23436  imasf1omet  23437  xmetresbl  23498  tmsxms  23548  tmsms  23549  imasf1oxms  23551  imasf1oms  23552  blcls  23568  comet  23575  stdbdxmet  23577  stdbdmet  23578  met1stc  23583  ressxms  23587  ressms  23588  prdsxms  23592  prdsms  23593  metustto  23615  xmsusp  23631  nrmmetd  23636  tngngp2  23722  nrgdomn  23741  subrgnrg  23743  tngnrg  23744  sranlm  23754  nrginvrcn  23762  nlmtlm  23764  nvctvc  23770  lssnlm  23771  lssnvc  23772  ngpocelbl  23774  nmhmco  23826  nmhmplusg  23827  qdensere  23839  tgioo  23865  xrtgioo  23875  xrsmopn  23881  reperflem  23887  icccmplem1  23891  icccmplem2  23892  reconnlem2  23896  xrge0tsms  23903  metdsf  23917  metdsre  23922  metnrm  23931  mulc1cncf  23974  icchmeo  24010  icopnfcnv  24011  xrhmeo  24015  cnrehmeo  24022  evth  24028  phtpcer  24064  pcohtpy  24089  pi1xfrgim  24127  cvsdiv  24201  cvsdivcl  24202  cphnvc  24245  cphsubrglem  24246  cphreccllem  24247  tcphcph  24306  clsocv  24319  iscmet3lem1  24360  iscmet3  24362  cmetss  24385  relcmpcmet  24387  bcthlem5  24397  cmetcusp1  24422  cmetcusp  24423  cphssphl  24440  cmscsscms  24442  cssbn  24444  cmslsschl  24446  chlcsschl  24447  rrxmet  24477  rrxbasefi  24479  minveclem7  24504  hlhil  24512  ivthlem1  24520  evthicc2  24529  ovolfsf  24540  ovolunlem1a  24565  ovoliunlem1  24571  ovolicc2lem2  24587  ovolicc2lem4  24589  ovolicc2lem5  24590  cmmbl  24603  nulmbl  24604  nulmbl2  24605  unmbl  24606  shftmbl  24607  voliunlem2  24620  ioombl1  24631  uniioombl  24658  dyadmbllem  24668  volcn  24675  vitalilem2  24678  vitalilem5  24681  mbfconst  24702  cncombf  24727  cnmbf  24728  i1fd  24750  i1fmullem  24763  itg1addlem2  24766  i1fmulc  24773  itg1mulc  24774  mbfi1fseqlem1  24785  mbfi1fseqlem4  24788  mbfi1flimlem  24792  xrge0f  24801  itg2const2  24811  itg2mulclem  24816  itg2mono  24823  itg2i1fseq  24825  itg2addlem  24828  itg2gt0  24830  itg2cnlem2  24832  itg2cn  24833  iblss  24874  itgle  24879  itgeqa  24883  iblconst  24887  itgconst  24888  ibladdlem  24889  itgaddlem1  24892  iblabslem  24897  iblabs  24898  iblabsr  24899  iblmulc2  24900  itgmulc2lem1  24901  itgsplit  24905  bddmulibl  24908  bddiblnc  24911  itggt0  24913  itgcn  24914  limciun  24963  perfdvf  24972  dvfre  25020  dvcnvlem  25045  dvexp3  25047  dvferm1lem  25053  dvferm2lem  25055  c1lip2  25067  dvle  25076  dvne0  25080  lhop1lem  25082  dvfsumrlim  25100  ftc1lem5  25109  ftc1cn  25112  ply1nz  25191  ply1nzb  25192  ply1domn  25193  ply1divalg  25207  fta1blem  25238  fta1b  25239  ig1peu  25241  ig1pdvds  25246  ply1lpir  25248  ply1pid  25249  elplyr  25267  plyeq0  25277  coeeu  25291  dgrub  25300  plyreres  25348  plydivalg  25364  fta1lem  25372  elqaalem3  25386  qaa  25388  aareccl  25391  aannenlem1  25393  aalioulem6  25402  taylfvallem1  25421  taylf  25425  tayl0  25426  dvtaylp  25434  ulmss  25461  mtest  25468  radcnvle  25484  psercnlem2  25488  psercn  25490  abelthlem2  25496  abelthlem8  25503  abelth  25505  pilem2  25516  pilem3  25517  efif1olem4  25606  efifo  25608  eff1olem  25609  logdmss  25702  dvloglem  25708  logf1o2  25710  efopnlem2  25717  logtayl  25720  cxpcn2  25804  cxpcn3  25806  loglesqrt  25816  logreclem  25817  relogbcl  25828  relogbreexp  25830  relogbmul  25832  relogbcxp  25840  atanre  25940  asinneg  25941  atandmneg  25961  atandmcj  25964  atandmtan  25975  bndatandm  25984  atansssdm  25988  areaf  26016  rlimcnp  26020  rlimcnp3  26022  xrlimcnp  26023  amgmlem  26044  amgm  26045  emcllem7  26056  dmlogdmgm  26078  rpdmgm  26079  dmgmaddnn0  26081  lgamgulmlem1  26083  lgamgulmlem2  26084  wilthlem2  26123  wilthlem3  26124  wilth  26125  ftalem3  26129  basellem3  26137  basellem4  26138  ppisval  26158  ppisval2  26159  sgmnncl  26201  chtdif  26212  ppidif  26217  ppinncl  26228  ppiltx  26231  sqff1o  26236  muinv  26247  dvdsmulf1o  26248  logexprlim  26278  mersenne  26280  perfectlem2  26283  dchrfi  26308  dchrghm  26309  dchrabs  26313  dchr1re  26316  bcmono  26330  bposlem3  26339  bposlem4  26340  bposlem5  26341  bposlem6  26342  bposlem9  26345  lgsfcl2  26356  lgsval2lem  26360  lgsmod  26376  lgsdirprm  26384  lgsne0  26388  lgsqrlem2  26400  gausslemma2dlem0h  26416  gausslemma2dlem1a  26418  gausslemma2dlem4  26422  lgseisenlem1  26428  lgseisenlem2  26429  lgsquadlem1  26433  lgsquadlem2  26434  lgsquad2lem2  26438  2sqlem8  26479  2sqlem9  26480  2sqlem11  26482  2sqmod  26489  2sqreulem1  26499  2sqreunnlem1  26502  dchrisumlem2  26543  dchrisumlem3  26544  dchrmusum2  26547  dchrvmasumlem2  26551  dchrvmasumiflem1  26554  dchrvmaeq0  26557  dchrisum0flblem2  26562  dchrisum0re  26566  dchrisum0lem1b  26568  dchrisum0lem2  26571  dirith2  26581  2vmadivsumlem  26593  chpdifbndlem1  26606  selberg3lem1  26610  selberg4lem1  26613  pntrlog2bndlem3  26632  pntpbnd1  26639  pntibndlem2  26644  pntlemo  26660  pntlem3  26662  tglngval  26816  hlcgreu  26883  tglinethrueu  26904  ragncol  26974  foot  26987  mideu  27003  opptgdim2  27010  hlpasch  27021  trgcopyeu  27071  cgraswap  27085  cgracom  27087  cgratr  27088  flatcgra  27089  dfcgra2  27095  acopyeu  27099  cgrg3col4  27118  f1otrg  27136  f1otrge  27137  xmstrkgc  27156  axlowdimlem13  27225  axlowdimlem15  27227  axlowdimlem16  27228  axcontlem2  27236  axcontlem3  27237  axcontlem4  27238  axcontlem10  27244  eengtrkg  27257  eengtrkge  27258  structiedg0val  27295  upgr1elem  27385  umgrislfupgrlem  27395  edglnl  27416  ausgrumgri  27440  usgredgreu  27488  uspgredg2vtxeu  27490  uspgredg2v  27494  usgredg2v  27497  usgr1e  27515  subgruhgredgd  27554  subuhgr  27556  subupgr  27557  subumgr  27558  subusgr  27559  upgrreslem  27574  upgrres  27576  umgrres  27577  nbumgrvtx  27616  nbgrssovtx  27631  nbupgrres  27634  nbusgrf1o0  27639  uvtxnbgrb  27671  cusgr0v  27698  cplgr1v  27700  cusgr1v  27701  cusgrexilem2  27712  cusgrexi  27713  structtocusgr  27716  cusgrres  27718  cusgrfilem2  27726  vtxdgfisf  27746  umgr2v2evd2  27797  ewlkprop  27873  lfgriswlk  27958  trlres  27970  upgrwlkdvdelem  28005  uhgrwkspth  28024  usgr2wlkspth  28028  pthdlem1  28035  crctcshwlkn0lem7  28082  crctcshtrl  28089  crctcsh  28090  wwlknbp  28108  wspthnp  28116  wlkswwlksf1o  28145  wwlksnext  28159  wwlksnextinj  28165  wwlksnextsurj  28166  wwlksnextbij0  28167  wwlksnextproplem3  28177  2trld  28204  2spthd  28207  umgr2adedgwlk  28211  umgr2adedgwlkon  28212  umgr2adedgwlkonALT  28213  umgr2adedgspth  28214  elwwlks2ons3  28221  clwwlkbp  28250  clwwlkccatlem  28254  clwlkclwwlklem2a2  28258  clwlkclwwlklem2fv2  28261  clwlkclwwlklem2a4  28262  clwlkclwwlkfolem  28272  clwlkclwwlkfo  28274  clwlkclwwlkf1  28275  clwlkclwwlkf1o  28276  clwwlkinwwlk  28305  clwwlkel  28311  clwwlkf1  28314  clwwlkfo  28315  clwwlkf1o  28316  wwlksext2clwwlk  28322  wwlksubclwwlk  28323  clwwnisshclwwsn  28324  clwwlknccat  28328  s2elclwwlknon2  28369  clwwlknonex2lem2  28373  clwwlknonex2e  28375  lp1cycl  28417  3trld  28437  3spthd  28441  3cycld  28443  eupthp1  28481  eupth2eucrct  28482  frgr1v  28536  nfrgr2v  28537  3vfriswmgrlem  28542  n4cyclfrgr  28556  frgrncvvdeqlem8  28571  frgrncvvdeqlem9  28572  frgrncvvdeqlem10  28573  frgrwopreglem5  28586  clwwnonrepclwwnon  28610  numclwwlk1lem2f1  28622  numclwwlk1lem2fo  28623  numclwwlk1lem2f1o  28624  numclwlk2lem2f1o  28644  nvex  28874  isnv  28875  isblo3i  29064  ipblnfi  29118  ubthlem2  29134  minvecolem7  29146  htthlem  29180  hlimadd  29456  hhsscms  29541  ocsh  29546  occl  29567  pjhthlem2  29655  pjhtheu  29657  pjpreeq  29661  ococin  29671  chscllem2  29901  chscl  29904  unopf1o  30179  cnvunop  30181  unoplin  30183  counop  30184  hmopadj2  30204  hmoplin  30205  bralnfn  30211  lnopmi  30263  unopbd  30278  hmops  30283  hmopm  30284  hmopco  30286  bdophmi  30295  nlelshi  30323  nlelchi  30324  riesz3i  30325  cnlnadjlem2  30331  adjlnop  30349  hmopidmpji  30415  pjclem4  30462  pj3si  30470  h1da  30612  shatomistici  30624  iundisjf  30829  f1o3d  30863  2ndresdju  30887  2ndresdjuf1o  30888  xppreima2  30889  isoun  30936  f1od2  30958  xrge0infss  30985  xrge0addcld  30987  xrofsup  30992  difioo  31005  fzsplit3  31017  iundisjfi  31019  subne0nn  31037  xreceu  31098  s3f1  31123  ccatf1  31125  swrdf1  31130  posrasymb  31145  resspos  31146  resstos  31147  odutos  31148  mgcf1o  31183  abliso  31207  gsumpart  31217  xrge0tsmsd  31219  cntrcrng  31224  pmtrcnel  31260  pmtrcnelor  31262  cycpmfv2  31283  cycpmcl  31285  cycpmco2lem4  31298  tocyccntz  31313  archiabllem1  31349  archiabllem2c  31351  archiabllem2  31353  suborng  31416  subofld  31417  rhmdvdsr  31419  elrhmunit  31421  0nellinds  31468  lindssn  31475  nsgmgc  31499  qsidomlem2  31531  fply1  31569  sradrng  31575  sralvec  31577  rgmoddim  31595  matdim  31600  lmhmlvec2  31604  dimkerim  31610  fedgmul  31614  extdg1id  31640  qtopt1  31687  qtophaus  31688  locfinreflem  31692  cmppcmp  31710  dispcmp  31711  zarmxt1  31732  pstmxmet  31749  xpinpreima2  31759  tpr2rico  31764  ordtrest2NEW  31775  xrmulc1cn  31782  zrhnm  31819  indf1ofs  31894  hashf2  31952  hasheuni  31953  esumcvg  31954  prsiga  31999  pwldsys  32025  ldsysgenld  32028  ldgenpisyslem1  32031  sxsigon  32060  measdivcstALTV  32093  volfiniune  32098  imambfm  32129  dya2iocnrect  32148  omssubaddlem  32166  sibfof  32207  sitgf  32214  oddpwdc  32221  eulerpartlemb  32235  eulerpartlemgvv  32243  sseqmw  32258  sseqf  32259  sseqp1  32262  fibp1  32268  prob01  32280  probfinmeasb  32295  probfinmeasbALTV  32296  probmeasb  32297  dstrvprob  32338  dstfrvel  32340  ballotlemic  32373  ballotlem1c  32374  ballotlemro  32389  ballotlemrc  32397  ballotlemirc  32398  ballotth  32404  plymulx0  32426  signstfvn  32448  signstfvcl  32452  signstfveq0a  32455  signstfveq0  32456  fdvposlt  32479  reprpmtf1o  32506  tgoldbachgnn  32539  bnj951  32655  bnj1379  32710  bnj1422  32717  bnj149  32755  bnj151  32757  bnj908  32811  bnj944  32818  bnj970  32827  bnj1006  32840  bnj1177  32886  bnj1189  32889  bnj1321  32907  bnj1398  32914  bnj1417  32921  bnj1523  32951  srcmpltd  32954  f1resrcmplf1d  32959  pthhashvtx  32989  2cycld  33000  subfacp1lem3  33044  subfacp1lem5  33046  erdszelem8  33060  erdszelem9  33061  cnpconn  33092  txpconn  33094  ptpconn  33095  connpconn  33097  sconnpi1  33101  txsconn  33103  cvxpconn  33104  cvxsconn  33105  iccllysconn  33112  cvmseu  33138  cvmfolem  33141  cvmliftmolem2  33144  cvmliftlem14  33159  cvmlift2lem9a  33165  cvmlift2lem12  33176  cvmlift2lem13  33177  cvmlift3  33190  satfdm  33231  fmla1  33249  fmlaomn0  33252  fmlasucdisj  33261  satff  33272  sategoelfvb  33281  mvrsfpw  33368  mrsubrn  33375  mrsubff1  33376  msubff  33392  msubff1  33418  mvhf1  33421  mclsssvlem  33424  mclsind  33432  mthmpps  33444  lediv2aALT  33535  dfon2  33674  ttrcltr  33702  poxp2  33717  frxp2  33718  poxp3  33723  frxp3  33724  nofnbday  33782  noxp1o  33793  nosepdmlem  33813  nosupno  33833  nosupbday  33835  nosupfv  33836  nosupbnd1  33844  nosupbnd2  33846  noinfno  33848  noinfbday  33850  noinffv  33851  noinfbnd1  33859  noinfbnd2  33861  nocvxmin  33900  conway  33920  scutun12  33931  etasslt  33934  scutbdaybnd2  33937  scutbdaybnd2lim  33938  scutbdaylt  33939  slerec  33940  sltlpss  34014  cofcutr  34019  addsval  34053  dfrdg4  34180  altxpsspw  34206  segconeu  34240  btwnconn1lem13  34328  btwnconn1lem14  34329  outsideofeu  34360  outsidele  34361  linerflx1  34378  linethrueu  34385  fwddifval  34391  fwddifnval  34392  nn0prpwlem  34438  neibastop1  34475  neibastop2lem  34476  topjoin  34481  fnemeet1  34482  fnemeet2  34483  fnejoin1  34484  fnejoin2  34485  filnetlem3  34496  onsuctopon  34550  bj-nnfim  34855  bj-nnfand  34858  bj-nnford  34860  bj-dfnnf3  34866  bj-nnfalt  34875  bj-nnfext  34876  bj-elgab  35054  relowlssretop  35461  elxp8  35469  finorwe  35480  finxp1o  35490  pibt2  35515  finixpnum  35689  fin2solem  35690  fin2so  35691  lindsadd  35697  lindsdom  35698  lindsenlbs  35699  ptrecube  35704  poimirlem4  35708  poimirlem7  35711  poimirlem13  35717  poimirlem15  35719  poimirlem16  35720  poimirlem17  35721  poimirlem18  35722  poimirlem19  35723  poimirlem20  35724  poimirlem21  35725  poimirlem24  35728  poimirlem26  35730  poimirlem27  35731  poimirlem29  35733  poimirlem30  35734  poimirlem31  35735  poimirlem32  35736  opnmbllem0  35740  mblfinlem2  35742  itg2gt0cn  35759  ibladdnclem  35760  itgaddnclem1  35762  iblabsnclem  35767  iblabsnc  35768  iblmulc2nc  35769  itgmulc2nclem1  35770  itggt0cn  35774  ftc1cnnc  35776  ftc1anclem3  35779  ftc1anclem4  35780  ftc1anclem5  35781  ftc1anclem6  35782  ftc1anclem7  35783  ftc1anclem8  35784  ftc1anc  35785  areacirclem2  35793  areacirc  35797  unirep  35798  sdclem1  35828  mettrifi  35842  istotbnd3  35856  sstotbnd2  35859  sstotbnd  35860  sstotbnd3  35861  equivtotbnd  35863  isbndx  35867  isbnd3  35869  blbnd  35872  equivbnd  35875  prdsbnd  35878  prdstotbnd  35879  ismtyhmeo  35890  heibor1  35895  heibor  35906  bfp  35909  rrnmet  35914  rrncmslem  35917  rrnequiv  35920  ismrer1  35923  iccbnd  35925  opidonOLD  35937  grpokerinj  35978  isgrpda  36040  isdrngo2  36043  iscringd  36083  crngohomfo  36091  smprngopr  36137  prnc  36152  isfldidl  36153  prter3  36823  lshpnelb  36925  lsatspn0  36941  lsatssn0  36943  lssats  36953  lsatcv0  36972  lsat0cv  36974  islshpcv  36994  lkr0f  37035  lshpsmreu  37050  lduallvec  37095  lkrlspeqN  37112  cdleme50f1  38484  cdleme50f1o  38487  cdleme  38501  cdlemk56  38912  dvalveclem  38966  dvhlveclem  39049  dvheveccl  39053  cdlemm10N  39059  diaf1oN  39071  dihord4  39199  dihf11lem  39207  dihf11  39208  dihglblem2N  39235  dihglb2  39283  dochvalr  39298  doch2val2  39305  dochocss  39307  dochsat  39324  dochshpncl  39325  dochnel  39334  dvh4dimlem  39384  dochsnkr2cl  39415  dochkr1  39419  lcfl6lem  39439  lcfl9a  39446  lclkrlem1  39447  lclkrlem2l  39459  lclkrlem2o  39462  lclkrlem2q  39464  lclkr  39474  lclkrslem1  39478  lclkrslem2  39479  lcfrlem9  39491  lcfrlem16  39499  lcfrlem17  39500  lcfrlem27  39510  lcfrlem37  39520  lcfrlem38  39521  lcfrlem40  39523  lcdlkreqN  39563  mapdordlem2  39578  mapdrvallem2  39586  mapdn0  39610  mapdpglem20  39632  mapdpglem30  39643  mapdpglem32  39646  mapdpg  39647  mapdindp0  39660  mapdh6aN  39676  mapdh6eN  39681  mapdh6kN  39687  hdmaplem4  39715  hdmap1val  39739  hdmap1l6a  39750  hdmap1l6e  39755  hdmap1l6k  39761  hdmapval3N  39779  hdmap11lem2  39783  hdmapnzcl  39786  hdmaprnlem3eN  39799  hdmap14lem4a  39812  hdmap14lem6  39814  hdmap14lem7  39815  hgmapvvlem2  39865  hgmapvvlem3  39866  hlhilhillem  39905  lcmineqlem15  39979  aks4d1p1  40012  aks4d1p3  40014  xppss12  40130  selvval2lem4  40154  frlmsnic  40188  evlsbagval  40198  mhpind  40206  mhphf  40208  posqsqznn  40264  addinvcom  40334  prjspersym  40367  0prjspnlem  40381  dffltz  40387  flt0  40390  flt4lem5e  40409  isnacs3  40448  mzpindd  40484  eldioph  40496  eldioph3  40504  rencldnfilem  40558  irrapxlem1  40560  irrapxlem4  40563  irrapxlem6  40565  pellexlem5  40571  pellfundlb  40622  rmspecnonsq  40645  rmxnn  40689  rmynn  40694  rmynn0  40695  jm2.22  40733  jm2.23  40734  jm2.20nn  40735  jm2.27a  40743  jm2.27c  40745  rmydioph  40752  jm3.1lem3  40757  dford3lem1  40764  rpnnen3lem  40769  harinf  40772  wepwsolem  40783  dnnumch3  40788  fnwe2lem2  40792  fnwe2  40794  dfac11  40803  lnmlsslnm  40822  lnmepi  40826  lmhmlnmsplit  40828  pwssplit4  40830  filnm  40831  imasgim  40841  harn0  40843  lpirlnr  40858  hbtlem7  40866  hbtlem6  40870  hbt  40871  dgraaub  40889  mpaaeu  40891  aaitgo  40903  rgspnmin  40912  proot1ex  40942  deg1mhm  40948  fiinfi  41069  cotrclrcl  41239  fsovf1od  41513  ntrk2imkb  41536  ntrf  41622  gneispacef2  41635  rr-phpd  41710  expgrowth  41842  binomcxplemdvbinom  41860  binomcxplemnotnn0  41863  ordelordALT  42046  2uasbanh  42070  rfcnnnub  42468  elixpconstg  42528  wessf1ornlem  42611  disjinfi  42620  projf1o  42625  fconst7  42701  fzisoeu  42729  monoordxrv  42912  iccshift  42946  iooshift  42950  fmul01lt1lem2  43016  ellimciota  43045  mullimc  43047  mullimcf  43054  sumnnodd  43061  addlimc  43079  liminfval2  43199  liminflimsupxrre  43248  icccncfext  43318  dvcosre  43343  dvdivbd  43354  dvdivcncf  43358  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  itgsinexplem1  43385  iblcncfioo  43409  itgperiod  43412  stoweidlem7  43438  stoweidlem14  43445  stoweidlem16  43447  stoweidlem26  43457  stoweidlem27  43458  stoweidlem31  43462  stoweidlem34  43465  stoweidlem36  43467  stoweidlem46  43477  stoweidlem47  43478  stoweidlem52  43483  stoweidlem57  43488  stoweidlem59  43490  stoweidlem60  43491  wallispilem3  43498  wallispilem4  43499  dirkertrigeqlem3  43531  dirkeritg  43533  dirkercncf  43538  fourierdlem15  43553  fourierdlem20  43558  fourierdlem25  43563  fourierdlem34  43572  fourierdlem37  43575  fourierdlem41  43579  fourierdlem42  43580  fourierdlem47  43584  fourierdlem48  43585  fourierdlem51  43588  fourierdlem52  43589  fourierdlem57  43594  fourierdlem58  43595  fourierdlem59  43596  fourierdlem63  43600  fourierdlem64  43601  fourierdlem65  43602  fourierdlem68  43605  fourierdlem79  43616  fourierdlem80  43617  fourierdlem81  43618  fourierdlem92  43629  fourierdlem104  43641  fourierdlem111  43648  fouriersw  43662  etransclem3  43668  etransclem7  43672  etransclem10  43675  etransclem15  43680  etransclem19  43684  etransclem20  43685  etransclem21  43686  etransclem22  43687  etransclem24  43689  etransclem25  43690  etransclem27  43692  etransclem28  43693  etransclem35  43700  etransclem44  43709  etransclem48  43713  nnfoctbdjlem  43883  preimagelt  44126  preimalegt  44127  fnresfnco  44422  funressnfv  44424  fsetsnf1  44433  fsetsnfo  44434  fsetsnf1o  44435  cfsetsnfsetf1  44440  cfsetsnfsetfo  44441  cfsetsnfsetf1o  44442  fcoresf1  44450  ffnafv  44550  rlimdmafv  44556  dfatco  44635  rlimdmafv2  44637  zm1nn  44682  eluzge0nn0  44692  2elfz2melfz  44698  subsubelfzo0  44706  smonoord  44711  setsnidel  44717  imasetpreimafvbijlemf1  44744  imasetpreimafvbijlemfo  44745  imasetpreimafvbij  44746  iccpartigtl  44763  iccpartgt  44767  iccpartf  44771  icceuelpart  44776  fargshiftf1  44781  fargshiftfo  44782  sprsymrelfolem2  44833  sprsymrelfo  44837  sprsymrelf1o  44838  prproropf1o  44847  sfprmdvdsmersenne  44943  lighneallem4  44950  evenm1odd  44979  evenp1odd  44980  oddp1eveni  44981  oddm1eveni  44982  m2even  44994  oexpnegALTV  45017  opoeALTV  45023  opeoALTV  45024  oddprmALTV  45027  nnoALTV  45035  nn0oALTV  45036  nnpw2evenALTV  45042  perfectALTVlem2  45062  perfectALTV  45063  sbgoldbalt  45121  wtgoldbnnsum4prm  45142  bgoldbnnsum3prm  45144  isomuspgrlem2c  45170  isomuspgrlem2d  45171  isomuspgrlem2e  45172  1hegrlfgr  45182  uspgrsprfo  45198  uspgrsprf1o  45199  mgmhmf1o  45229  idmgmhm  45230  resmgmhm  45240  resmgmhm2  45241  resmgmhm2b  45242  mgmhmco  45243  mgmhmeql  45245  copissgrp  45250  isrnghm2d  45347  rnghmf1o  45349  rnghmco  45353  idrnghm  45354  c0mgm  45355  c0rhm  45358  c0rnghm  45359  c0snmgmhm  45360  c0snmhm  45361  zrrnghm  45363  lidlmsgrp  45372  zlidlring  45374  2zlidl  45380  2zrngamgm  45385  2zrngagrp  45389  2zrngmmgm  45392  rngcinv  45427  rngcinvALTV  45439  ringcinv  45478  ringcinvALTV  45502  nn0eo  45762  blennnelnn  45810  nnpw2blen  45814  dignn0fr  45835  dignn0ldlem  45836  dig2nn1st  45839  1arymaptf1  45876  1arymaptfo  45877  1arymaptf1o  45878  2arymaptf1  45887  2arymaptfo  45888  2arymaptf1o  45889  inlinecirc02p  46021  toslat  46156  topdlat  46178  isthincd  46206  fullthinc  46215  thincfth  46217  thincciso  46218  0thincg  46219  aacllem  46391