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

Theorem syl6sseq 3397
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 3376 . 2  |-  ( A 
C_  B  <->  A  C_  C
)
41, 3sylib 196 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    C_ wss 3323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3330  df-ss 3337
This theorem is referenced by:  syl6sseqr  3398  sofld  5281  relrelss  5356  foimacnv  5653  onfununi  6794  hartogslem1  7748  cantnfp1lem3  7880  cantnfp1lem3OLD  7906  uniwf  8018  rankeq0b  8059  cflecard  8414  fin23lem16  8496  fin23lem41  8513  pwcfsdom  8739  fpwwe2lem13  8801  fpwwe2  8802  canth4  8806  hashbclem  12197  zsum  13187  fsumcvg3  13198  incexclem  13291  ramub1lem1  14079  imasaddfnlem  14458  imasvscafn  14467  mremre  14534  submre  14535  mreexexlem3d  14576  isacs1i  14587  acsmapd  15340  acsmap2d  15341  gsumzoppg  16430  gsumzoppgOLD  16431  lspsntri  17158  lsppratlem4  17211  lbsextlem3  17221  distop  18580  elcls  18657  cnpresti  18872  cnprest  18873  cmpcld  18985  cnconn  19006  iuncon  19012  ptuni2  19129  alexsubALTlem3  19601  ustssco  19769  ust0  19774  ustbas2  19780  ustimasn  19783  utopbas  19790  utop2nei  19805  setsmstopn  20033  metustsymOLD  20116  metustsym  20117  metustOLD  20122  metust  20123  tngtopn  20216  ovoliunlem1  20965  lhop1lem  21465  ig1peu  21623  ig1pdvds  21628  logccv  22088  amgmlem  22363  shsupcl  24709  shsupunss  24717  shslubi  24756  orthin  24817  h1datomi  24952  mdslj2i  25692  mdslmd1lem1  25697  iundifdifd  25880  metideq  26289  hauseqcn  26294  tpr2rico  26311  esumpfinvallem  26492  orvcelval  26820  signsply0  26921  cvmlift2lem11  27171  cvmlift2lem12  27172  zprod  27419  dfon2lem7  27571  onsucsuccmpi  28259  mblfinlem1  28399  ismblfin  28403  comppfsc  28550  filnetlem3  28572  sstotbnd2  28644  ismrcd1  29005  eldioph2lem2  29070  rmxyelqirr  29222  hbt  29457  rngunsnply  29501  iocinico  29558  stoweidlem50  29816  stoweidlem52  29818  stoweidlem53  29819  stoweidlem57  29823  stoweidlem59  29825  zlmodzxzel  30721  lincresunit3  30946  dochexmidlem4  35001  lcfrlem38  35118
  Copyright terms: Public domain W3C validator