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

Theorem syl6sseq 3390
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 3369 . 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 1362    C_ wss 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-in 3323  df-ss 3330
This theorem is referenced by:  syl6sseqr  3391  sofld  5274  relrelss  5349  foimacnv  5646  onfununi  6788  hartogslem1  7744  cantnfp1lem3  7876  cantnfp1lem3OLD  7902  uniwf  8014  rankeq0b  8055  cflecard  8410  fin23lem16  8492  fin23lem41  8509  pwcfsdom  8735  fpwwe2lem13  8796  fpwwe2  8797  canth4  8801  hashbclem  12188  zsum  13178  fsumcvg3  13189  incexclem  13281  ramub1lem1  14069  imasaddfnlem  14448  imasvscafn  14457  mremre  14524  submre  14525  mreexexlem3d  14566  isacs1i  14577  acsmapd  15330  acsmap2d  15331  gsumzoppg  16415  gsumzoppgOLD  16416  lspsntri  17099  lsppratlem4  17152  lbsextlem3  17162  distop  18441  elcls  18518  cnpresti  18733  cnprest  18734  cmpcld  18846  cnconn  18867  iuncon  18873  ptuni2  18990  alexsubALTlem3  19462  ustssco  19630  ust0  19635  ustbas2  19641  ustimasn  19644  utopbas  19651  utop2nei  19666  setsmstopn  19894  metustsymOLD  19977  metustsym  19978  metustOLD  19983  metust  19984  tngtopn  20077  ovoliunlem1  20826  lhop1lem  21326  ig1peu  21527  ig1pdvds  21532  logccv  21992  amgmlem  22267  shsupcl  24563  shsupunss  24571  shslubi  24610  orthin  24671  h1datomi  24806  mdslj2i  25546  mdslmd1lem1  25551  iundifdifd  25735  metideq  26173  hauseqcn  26178  tpr2rico  26195  esumpfinvallem  26376  orvcelval  26698  signsply0  26799  cvmlift2lem11  27049  cvmlift2lem12  27050  zprod  27296  dfon2lem7  27448  onsucsuccmpi  28136  mblfinlem1  28269  ismblfin  28273  comppfsc  28420  filnetlem3  28442  sstotbnd2  28514  ismrcd1  28876  eldioph2lem2  28941  rmxyelqirr  29093  hbt  29328  rngunsnply  29372  iocinico  29429  stoweidlem50  29688  stoweidlem52  29690  stoweidlem53  29691  stoweidlem57  29695  stoweidlem59  29697  zlmodzxzel  30583  lincresunit3  30721  dochexmidlem4  34678  lcfrlem38  34795
  Copyright terms: Public domain W3C validator