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

Theorem syl6sseq 3386
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 3365 . 2  |-  ( A 
C_  B  <->  A  C_  C
)
41, 3sylib 189 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    C_ wss 3312
This theorem is referenced by:  syl6sseqr  3387  sofld  5310  relrelss  5385  foimacnv  5684  onfununi  6595  hartogslem1  7503  cantnfp1lem3  7628  uniwf  7737  rankeq0b  7778  cflecard  8125  fin23lem16  8207  fin23lem41  8224  pwcfsdom  8450  fpwwe2lem13  8509  fpwwe2  8510  canth4  8514  hashbclem  11693  zsum  12504  fsumcvg3  12515  incexclem  12608  ramub1lem1  13386  imasaddfnlem  13745  imasvscafn  13754  mremre  13821  submre  13822  mreexexlem3d  13863  isacs1i  13874  acsmapd  14596  acsmap2d  14597  gsumzoppg  15531  lspsntri  16161  lsppratlem4  16214  lbsextlem3  16224  distop  17052  elcls  17129  cnpresti  17344  cnprest  17345  cmpcld  17457  cnconn  17477  iuncon  17483  ptuni2  17600  alexsubALTlem3  18072  ustssco  18236  ust0  18241  ustbas2  18247  ustimasn  18250  utopbas  18257  utop2nei  18272  setsmstopn  18500  metustsymOLD  18583  metustsym  18584  metustOLD  18589  metust  18590  tngtopn  18683  ovoliunlem1  19390  lhop1lem  19889  ig1peu  20086  ig1pdvds  20091  logccv  20546  amgmlem  20820  shsupcl  22832  shsupunss  22840  shslubi  22879  orthin  22940  h1datomi  23075  mdslj2i  23815  mdslmd1lem1  23820  iundifdifd  24004  metideq  24280  hauseqcn  24285  tpr2rico  24302  esumpfinvallem  24456  orvcelval  24718  cvmlift2lem11  24992  cvmlift2lem12  24993  zprod  25255  dfon2lem7  25408  onsucsuccmpi  26185  mblfinlem  26234  ismblfin  26237  comppfsc  26378  filnetlem3  26400  sstotbnd2  26474  ismrcd1  26743  eldioph2lem2  26810  rmxyelqirr  26964  hbt  27302  rngunsnply  27346  stoweidlem50  27766  stoweidlem52  27768  stoweidlem53  27769  stoweidlem57  27773  stoweidlem59  27775  dochexmidlem4  32198  lcfrlem38  32315
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator