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

Theorem syl6sseq 3224
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 3203 . 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 1623    C_ wss 3152
This theorem is referenced by:  syl6sseqr  3225  sofld  5121  relrelss  5196  foimacnv  5490  onfununi  6358  hartogslem1  7257  cantnfp1lem3  7382  uniwf  7491  rankeq0b  7532  cflecard  7879  fin23lem16  7961  fin23lem41  7978  pwcfsdom  8205  fpwwe2lem13  8264  fpwwe2  8265  canth4  8269  hashbclem  11390  zsum  12191  fsumcvg3  12202  incexclem  12295  ramub1lem1  13073  imasaddfnlem  13430  imasvscafn  13439  mremre  13506  submre  13507  mreexexlem3d  13548  isacs1i  13559  acsmapd  14281  acsmap2d  14282  gsumzoppg  15216  lspsntri  15850  lsppratlem4  15903  lbsextlem3  15913  distop  16733  elcls  16810  cnpresti  17016  cnprest  17017  cmpcld  17129  cnconn  17148  iuncon  17154  ptuni2  17271  alexsubALTlem3  17743  setsmstopn  18024  tngtopn  18166  ovoliunlem1  18861  lhop1lem  19360  ig1peu  19557  ig1pdvds  19562  logccv  20010  amgmlem  20284  shsupcl  21917  shsupunss  21925  shslubi  21964  orthin  22025  h1datomi  22160  mdslj2i  22900  mdslmd1lem1  22905  tpr2rico  23296  orvcelval  23669  cvmlift2lem11  23844  cvmlift2lem12  23845  dfon2lem7  24145  onsucsuccmpi  24882  tartarmap  25888  comppfsc  26307  filnetlem3  26329  sstotbnd2  26498  ismrcd1  26773  eldioph2lem2  26840  rmxyelqirr  26995  hbt  27334  rngunsnply  27378  stoweidlem50  27799  stoweidlem52  27801  stoweidlem53  27802  stoweidlem57  27806  stoweidlem59  27808  dochexmidlem4  31653  lcfrlem38  31770
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator