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

Theorem syl5eqss 3235
Description: B chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
Hypotheses
Ref Expression
syl5eqss.1  |-  A  =  B
syl5eqss.2  |-  ( ph  ->  B  C_  C )
Assertion
Ref Expression
syl5eqss  |-  ( ph  ->  A  C_  C )

Proof of Theorem syl5eqss
StepHypRef Expression
1 syl5eqss.2 . 2  |-  ( ph  ->  B  C_  C )
2 syl5eqss.1 . . 3  |-  A  =  B
32sseq1i 3215 . 2  |-  ( A 
C_  C  <->  B  C_  C
)
41, 3sylibr 203 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    C_ wss 3165
This theorem is referenced by:  syl5eqssr  3236  inss  3411  fr3nr  4587  suceloni  4620  xpsspw  4813  xpsspwOLD  4814  fun  5421  fun11iun  5509  fmpt  5697  fliftrel  5823  knatar  5873  suppss2  6089  1stcof  6163  2ndcof  6164  fnwelem  6246  oeeui  6616  cantnfp1lem1  7396  cantnfp1lem3  7398  cantnflem1d  7406  cantnflem1  7407  aceq3lem  7763  cflecard  7895  cfslb2n  7910  itunitc1  8062  axdc3lem2  8093  fpwwe2lem12  8279  canthwelem  8288  wuncval2  8385  gruiun  8437  peano5nni  9765  un0addcl  10013  un0mulcl  10014  mertenslem2  12357  4sqlem11  13018  4sqlem19  13026  vdwlem13  13056  imasless  13458  rescfth  13827  oppchofcl  14050  oyoncl  14060  gsumvallem1  14464  efgsfo  15064  efgcpbllemb  15080  frgpuplem  15097  gsumzaddlem  15219  dprdfid  15268  dprd2d2  15295  ablfacrp  15317  ablfac1b  15321  ablfac1eu  15324  pgpfac1lem5  15330  ablfaclem3  15338  lsptpcl  15752  lsppratlem3  15918  lsppratlem4  15919  lbsextlem2  15928  topsn  16689  ordtbaslem  16934  ordtuni  16936  ordtbas2  16937  cnpco  17012  cnconst2  17027  tgcmp  17144  iuncon  17170  ptuni2  17287  xkococnlem  17369  tgqtop  17419  fbasrn  17595  uzrest  17608  fmco  17672  alexsubALT  17761  snclseqg  17814  imasdsf1olem  17953  xmetresbl  17999  blsscls2  18066  tngtopn  18182  reconn  18349  metnrmlem3  18381  cphsubrglem  18629  minveclem1  18804  minveclem3b  18808  ovolficcss  18845  ovolicc2lem4  18895  iundisj2  18922  uniioombllem4  18957  vitalilem5  18983  mbfeqalem  19013  itg1addlem4  19070  limciun  19260  dvlip2  19358  dv11cn  19364  aalioulem3  19730  pserdvlem2  19820  pserdv  19821  abelthlem2  19824  efif1o  19924  efrlim  20280  fsumdvdsmul  20451  perfectlem2  20485  minvecolem1  21469  sh0le  22035  mdslmd3i  22928  suppss2f  23216  iundisj2fi  23379  iundisj2f  23381  blscon  23790  cvmliftlem2  23832  cvmlift2lem12  23860  eupares  23914  ghomfo  24013  relexpdm  24047  relexprn  24048  trpredss  24303  trpredmintr  24305  frrlem5d  24359  areacirclem4  25030  trunitr  25212  cmptdst  25671  limptlimpr2lem1  25677  prismorcsetlemc  26020  neibastop2lem  26412  filnetlem3  26432  sdclem1  26556  istotbnd3  26598  sstotbnd  26602  iccbnd  26667  icccmpALT  26668  f1lindf  27395  hbtlem6  27436  stoweidlem14  27866  opabbrex  28191  bnj849  29273  bnj1136  29343  bnj1311  29370  bnj1413  29381  bnj1452  29398  osumcllem1N  30767  osumcllem2N  30768  osumcllem4N  30770  osumcllem9N  30775  pexmidlem6N  30786  dihglblem3N  32107  dvhdimlem  32256  dochexmidlem6  32277  lcfrlem16  32370  lcfr  32397
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator