MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl5eqss Structured version   Visualization version   GIF version

Theorem syl5eqss 3809
Description: A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
Hypotheses
Ref Expression
syl5eqss.1 𝐴 = 𝐵
syl5eqss.2 (𝜑𝐵𝐶)
Assertion
Ref Expression
syl5eqss (𝜑𝐴𝐶)

Proof of Theorem syl5eqss
StepHypRef Expression
1 syl5eqss.2 . 2 (𝜑𝐵𝐶)
2 syl5eqss.1 . . 3 𝐴 = 𝐵
32sseq1i 3789 . 2 (𝐴𝐶𝐵𝐶)
41, 3sylibr 225 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1652  wss 3732
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-in 3739  df-ss 3746
This theorem is referenced by:  syl5eqssr  3810  inss  4002  tpssi  4521  xpsspw  5401  opabssxpd  5506  fun  6248  fmpt  6570  fliftrel  6750  knatar  6799  fr3nr  7177  suceloni  7211  fun11iun  7324  1stcof  7396  2ndcof  7397  fnwelem  7494  oeeui  7887  aceq3lem  9194  cflecard  9328  cfslb2n  9343  itunitc1  9495  axdc3lem2  9526  fpwwe2lem12  9716  canthwelem  9725  wuncval2  9822  peano5nni  11277  un0addcl  11573  un0mulcl  11574  fsuppmapnn0fiublem  12997  fsuppmapnn0fiub  12998  mertenslem2  14900  4sqlem11  15938  4sqlem19  15946  vdwlem13  15976  imasless  16466  rescfth  16862  oppchofcl  17166  oyoncl  17176  mgmidsssn0  17535  efgsfo  18417  efgcpbllemb  18434  frgpuplem  18451  gsummpt1n0  18630  dprdfid  18683  dprd2d2  18710  ablfacrp  18732  ablfac1b  18736  ablfac1eu  18739  pgpfac1lem5  18745  ablfaclem3  18753  lsptpcl  19251  lsppratlem3  19423  lsppratlem4  19424  lbsextlem2  19433  f1lindf  20437  topsn  21015  ordtbaslem  21272  ordtuni  21274  ordtbas2  21275  cnpco  21351  cnconst2  21367  tgcmp  21484  iunconn  21511  ptuni2  21659  xkococnlem  21742  tgqtop  21795  fbasrn  21967  uzrest  21980  fmco  22044  alexsubALT  22134  cnextf  22149  snclseqg  22198  ustund  22304  imasdsf1olem  22457  xmetresbl  22521  blsscls2  22588  metustss  22635  tngtopn  22733  reconn  22910  metnrmlem3  22943  cphsubrglem  23255  minveclem1  23484  minveclem3b  23488  ovolficcss  23527  ovolicc2lem4  23578  iundisj2  23607  uniioombllem4  23644  vitalilem5  23670  mbfeqalem1  23699  itg1addlem4  23757  limciun  23949  dvlip2  24049  dv11cn  24055  aalioulem3  24380  pserdvlem2  24473  pserdv  24474  abelthlem2  24477  efif1o  24584  efrlim  24987  lgamgulmlem1  25046  fsumdvdsmul  25212  perfectlem2  25246  setsvtx  26204  uhgredgn0  26300  upgredgss  26304  umgredgss  26305  usgredgss  26332  umgrres1lem  26481  upgrres1  26484  1hegrvtxdg1r  26695  clwlknf1oclwwlknlem3  27349  clwlknf1oclwwlknlem3OLD  27351  minvecolem1  28186  sh0le  28755  mdslmd3i  29647  iundisj2f  29851  suppss2f  29889  suppss3  29951  iundisj2fi  30005  pstmfval  30386  ordtrest2NEW  30416  ldgenpisyslem1  30673  ldgenpisyslem2  30674  omsmeas  30832  sitgclbn  30852  eulerpartlemt  30880  eulerpartlemmf  30884  eulerpartlemgf  30888  bnj849  31443  bnj1136  31513  bnj1311  31540  bnj1413  31551  bnj1452  31568  blsconn  31674  cvmliftlem2  31716  cvmlift2lem12  31744  mvtss  31898  mthmpps  31927  trpredss  32172  trpredmintr  32174  frrlem5d  32231  noextendseq  32264  nosupno  32293  nosupbnd2lem1  32305  noetalem3  32309  neibastop2lem  32798  filnetlem3  32818  finxpsuclem  33667  poimirlem3  33836  mblfinlem3  33872  areacirclem2  33924  sdclem1  33961  istotbnd3  33992  sstotbnd  33996  iccbnd  34061  icccmpALT  34062  osumcllem1N  35912  osumcllem2N  35913  osumcllem4N  35915  osumcllem9N  35920  pexmidlem6N  35931  dihglblem3N  37251  dvhdimlem  37400  dochexmidlem6  37421  lcfrlem16  37514  lcfr  37541  hbtlem6  38376  iocinico  38473  trclubgNEW  38600  cnvrcl0  38607  relexp0a  38683  brtrclfv2  38694  cotrclrcl  38709  frege77d  38713  unhe1  38753  ntrrn  39094  imo72b2lem0  39139  imo72b2lem2  39141  imo72b2lem1  39145  imo72b2  39149  radcnvrat  39187  iunconnlem2  39823  ssinss2d  39879  limccog  40490  limsupresico  40570  liminfresico  40641  icccncfext  40738  stoweidlem14  40868  fourierdlem20  40981  fourierdlem42  41003  fourierdlem46  41006  fourierdlem50  41010  fourierdlem51  41011  fourierdlem54  41014  fourierdlem64  41024  fourierdlem76  41036  fourierdlem102  41062  fourierdlem103  41063  fourierdlem104  41064  fourierdlem114  41074  meadjiunlem  41319  meaiininclem  41340  ovnsupge0  41411  hoidmvlelem2  41450  hoidmvlelem4  41452  vonvolmbllem  41514  vonvolmbl2  41517  vonvol2  41518  vonioolem1  41534  issmflem  41576  perfectALTVlem2  42307  uspgropssxp  42421  funcrngcsetc  42667  funcringcsetc  42704  srhmsubc  42745  rhmsubclem3  42757  srhmsubcALTV  42763  rhmsubcALTVlem4  42776  setrec2fun  43108  onsetreclem2  43121
  Copyright terms: Public domain W3C validator