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

Theorem syl6sseq 3550
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 3529 . 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 1379    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490
This theorem is referenced by:  syl6sseqr  3551  sofld  5453  relrelss  5529  foimacnv  5831  onfununi  7009  hartogslem1  7963  cantnfp1lem3  8095  cantnfp1lem3OLD  8121  uniwf  8233  rankeq0b  8274  cflecard  8629  fin23lem16  8711  fin23lem41  8728  pwcfsdom  8954  fpwwe2lem13  9016  fpwwe2  9017  canth4  9021  hashbclem  12461  zsum  13496  fsumcvg3  13507  incexclem  13604  ramub1lem1  14396  imasaddfnlem  14776  imasvscafn  14785  mremre  14852  submre  14853  mreexexlem3d  14894  isacs1i  14905  acsmapd  15658  acsmap2d  15659  gsumzoppg  16755  gsumzoppgOLD  16756  lspsntri  17523  lsppratlem4  17576  lbsextlem3  17586  distop  19260  elcls  19337  cnpresti  19552  cnprest  19553  cmpcld  19665  cnconn  19686  iuncon  19692  ptuni2  19809  alexsubALTlem3  20281  ustssco  20449  ust0  20454  ustbas2  20460  ustimasn  20463  utopbas  20470  utop2nei  20485  setsmstopn  20713  metustsymOLD  20796  metustsym  20797  metustOLD  20802  metust  20803  tngtopn  20896  ovoliunlem1  21645  lhop1lem  22146  ig1peu  22304  ig1pdvds  22309  logccv  22769  amgmlem  23044  shsupcl  25929  shsupunss  25937  shslubi  25976  orthin  26037  h1datomi  26172  mdslj2i  26912  mdslmd1lem1  26917  iundifdifd  27099  difres  27127  metideq  27505  hauseqcn  27510  tpr2rico  27527  esumpfinvallem  27717  orvcelval  28044  signsply0  28145  cvmlift2lem11  28395  cvmlift2lem12  28396  zprod  28643  dfon2lem7  28795  onsucsuccmpi  29482  mblfinlem1  29626  ismblfin  29630  comppfsc  29777  filnetlem3  29799  sstotbnd2  29871  ismrcd1  30232  eldioph2lem2  30296  rmxyelqirr  30448  hbt  30683  rngunsnply  30727  iocinico  30784  limciccioolb  31163  limcrecl  31171  limcicciooub  31179  icccncfext  31226  stoweidlem50  31350  stoweidlem52  31352  stoweidlem53  31353  stoweidlem57  31357  stoweidlem59  31359  fourierdlem50  31457  zlmodzxzel  32008  lincresunit3  32155  dochexmidlem4  36260  lcfrlem38  36377
  Copyright terms: Public domain W3C validator