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

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

Proof of Theorem syl6sseq
StepHypRef Expression
1 syl6sseq.1 . 2  |-  ( ph  ->  A  C_  B )
2 syl6sseq.2 . . 3  |-  B  =  C
32sseq2i 3216 . 2  |-  ( A 
C_  B  <->  A  C_  C
)
41, 3sylib 188 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:  syl6sseqr  3238  sofld  5137  relrelss  5212  foimacnv  5506  onfununi  6374  hartogslem1  7273  cantnfp1lem3  7398  uniwf  7507  rankeq0b  7548  cflecard  7895  fin23lem16  7977  fin23lem41  7994  pwcfsdom  8221  fpwwe2lem13  8280  fpwwe2  8281  canth4  8285  hashbclem  11406  zsum  12207  fsumcvg3  12218  incexclem  12311  ramub1lem1  13089  imasaddfnlem  13446  imasvscafn  13455  mremre  13522  submre  13523  mreexexlem3d  13564  isacs1i  13575  acsmapd  14297  acsmap2d  14298  gsumzoppg  15232  lspsntri  15866  lsppratlem4  15919  lbsextlem3  15929  distop  16749  elcls  16826  cnpresti  17032  cnprest  17033  cmpcld  17145  cnconn  17164  iuncon  17170  ptuni2  17287  alexsubALTlem3  17759  setsmstopn  18040  tngtopn  18182  ovoliunlem1  18877  lhop1lem  19376  ig1peu  19573  ig1pdvds  19578  logccv  20026  amgmlem  20300  shsupcl  21933  shsupunss  21941  shslubi  21980  orthin  22041  h1datomi  22176  mdslj2i  22916  mdslmd1lem1  22921  tpr2rico  23311  orvcelval  23684  cvmlift2lem11  23859  cvmlift2lem12  23860  zprod  24160  dfon2lem7  24216  onsucsuccmpi  24954  tartarmap  25991  comppfsc  26410  filnetlem3  26432  sstotbnd2  26601  ismrcd1  26876  eldioph2lem2  26943  rmxyelqirr  27098  hbt  27437  rngunsnply  27481  stoweidlem50  27902  stoweidlem52  27904  stoweidlem53  27905  stoweidlem57  27909  stoweidlem59  27911  dochexmidlem4  32275  lcfrlem38  32392
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