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

Theorem syl6sseq 3509
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 3488 . 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 1370    C_ wss 3435
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3442  df-ss 3449
This theorem is referenced by:  syl6sseqr  3510  sofld  5393  relrelss  5468  foimacnv  5765  onfununi  6911  hartogslem1  7866  cantnfp1lem3  7998  cantnfp1lem3OLD  8024  uniwf  8136  rankeq0b  8177  cflecard  8532  fin23lem16  8614  fin23lem41  8631  pwcfsdom  8857  fpwwe2lem13  8919  fpwwe2  8920  canth4  8924  hashbclem  12322  zsum  13312  fsumcvg3  13323  incexclem  13416  ramub1lem1  14204  imasaddfnlem  14584  imasvscafn  14593  mremre  14660  submre  14661  mreexexlem3d  14702  isacs1i  14713  acsmapd  15466  acsmap2d  15467  gsumzoppg  16561  gsumzoppgOLD  16562  lspsntri  17300  lsppratlem4  17353  lbsextlem3  17363  distop  18731  elcls  18808  cnpresti  19023  cnprest  19024  cmpcld  19136  cnconn  19157  iuncon  19163  ptuni2  19280  alexsubALTlem3  19752  ustssco  19920  ust0  19925  ustbas2  19931  ustimasn  19934  utopbas  19941  utop2nei  19956  setsmstopn  20184  metustsymOLD  20267  metustsym  20268  metustOLD  20273  metust  20274  tngtopn  20367  ovoliunlem1  21116  lhop1lem  21617  ig1peu  21775  ig1pdvds  21780  logccv  22240  amgmlem  22515  shsupcl  24892  shsupunss  24900  shslubi  24939  orthin  25000  h1datomi  25135  mdslj2i  25875  mdslmd1lem1  25880  iundifdifd  26062  metideq  26464  hauseqcn  26469  tpr2rico  26486  esumpfinvallem  26667  orvcelval  26994  signsply0  27095  cvmlift2lem11  27345  cvmlift2lem12  27346  zprod  27593  dfon2lem7  27745  onsucsuccmpi  28432  mblfinlem1  28575  ismblfin  28579  comppfsc  28726  filnetlem3  28748  sstotbnd2  28820  ismrcd1  29181  eldioph2lem2  29246  rmxyelqirr  29398  hbt  29633  rngunsnply  29677  iocinico  29734  stoweidlem50  29992  stoweidlem52  29994  stoweidlem53  29995  stoweidlem57  29999  stoweidlem59  30001  zlmodzxzel  30899  lincresunit3  31133  dochexmidlem4  35431  lcfrlem38  35548
  Copyright terms: Public domain W3C validator