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

Theorem syl6sseq 3488
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 3467 . 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 1405    C_ wss 3414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-in 3421  df-ss 3428
This theorem is referenced by:  syl6sseqr  3489  sofld  5272  relrelss  5347  foimacnv  5816  onfununi  7045  hartogslem1  8001  cantnfp1lem3  8131  cantnfp1lem3OLD  8157  uniwf  8269  rankeq0b  8310  cflecard  8665  fin23lem16  8747  fin23lem41  8764  pwcfsdom  8990  fpwwe2lem13  9050  fpwwe2  9051  canth4  9055  hashbclem  12550  dmtrclfv  13001  zsum  13689  fsumcvg3  13700  incexclem  13799  zprod  13896  ramub1lem1  14753  imasaddfnlem  15142  imasvscafn  15151  mremre  15218  submre  15219  mreexexlem3d  15260  isacs1i  15271  acsmapd  16132  acsmap2d  16133  gsumzoppg  17290  gsumzoppgOLD  17291  lspsntri  18063  lsppratlem4  18116  lbsextlem3  18126  distop  19789  elcls  19867  cnpresti  20082  cnprest  20083  cmpcld  20195  cnconn  20215  iuncon  20221  comppfsc  20325  ptuni2  20369  alexsubALTlem3  20841  ustssco  21009  ust0  21014  ustbas2  21020  ustimasn  21023  utopbas  21030  utop2nei  21045  setsmstopn  21273  metustsymOLD  21356  metustsym  21357  metustOLD  21362  metust  21363  tngtopn  21456  ovoliunlem1  22205  lhop1lem  22706  ig1peu  22864  ig1pdvds  22869  logccv  23338  amgmlem  23645  shsupcl  26670  shsupunss  26678  shslubi  26717  orthin  26778  h1datomi  26913  mdslj2i  27652  mdslmd1lem1  27657  pwuniss  27849  iundifdifd  27859  difres  27893  fresf1o  27914  metideq  28325  hauseqcn  28330  tpr2rico  28347  esumrnmpt2  28515  esumpfinvallem  28521  esum2d  28540  omssubadd  28748  carsggect  28766  omsmeas  28771  orvcelval  28913  signsply0  29014  cvmlift2lem11  29610  cvmlift2lem12  29611  dfon2lem7  30008  filnetlem3  30608  onsucsuccmpi  30675  dissneqlem  31256  icoreunrn  31276  mblfinlem1  31423  ismblfin  31427  sstotbnd2  31552  dochexmidlem4  34483  lcfrlem38  34600  ismrcd1  34992  eldioph2lem2  35055  rmxyelqirr  35207  hbt  35443  rngunsnply  35486  iocinico  35543  trrelsuperrel2dg  35650  limciccioolb  36995  limcrecl  37003  limcicciooub  37011  stoweidlem50  37200  stoweidlem52  37202  stoweidlem53  37203  stoweidlem57  37207  stoweidlem59  37209  fourierdlem50  37307  fourierdlem103  37360  fourierdlem104  37361  zlmodzxzel  38455  lincresunit3  38593
  Copyright terms: Public domain W3C validator