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

Theorem syl6sseq 3510
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 3489 . 2  |-  ( A 
C_  B  <->  A  C_  C
)
41, 3sylib 199 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    C_ wss 3436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-in 3443  df-ss 3450
This theorem is referenced by:  syl6sseqr  3511  sofld  5303  relrelss  5378  foimacnv  5848  onfununi  7071  hartogslem1  8066  cantnfp1lem3  8193  uniwf  8298  rankeq0b  8339  cflecard  8690  fin23lem16  8772  fin23lem41  8789  pwcfsdom  9015  fpwwe2lem13  9074  fpwwe2  9075  canth4  9079  hashbclem  12619  dmtrclfv  13082  zsum  13783  fsumcvg3  13794  incexclem  13893  zprod  13990  ramub1lem1  14983  imasaddfnlem  15433  imasvscafn  15442  mremre  15509  submre  15510  mreexexlem3d  15551  isacs1i  15562  acsmapd  16423  acsmap2d  16424  gsumzoppg  17576  lspsntri  18319  lsppratlem4  18372  lbsextlem3  18382  distop  20009  elcls  20087  cnpresti  20302  cnprest  20303  cmpcld  20415  cnconn  20435  iuncon  20441  comppfsc  20545  ptuni2  20589  alexsubALTlem3  21062  ustssco  21227  ust0  21232  ustbas2  21238  ustimasn  21241  utopbas  21248  utop2nei  21263  setsmstopn  21491  metustsym  21568  metust  21571  tngtopn  21656  ovoliunlem1  22453  lhop1lem  22963  ig1peu  23120  ig1peuOLD  23121  ig1pdvds  23126  ig1pdvdsOLD  23132  logccv  23606  amgmlem  23913  shsupcl  26989  shsupunss  26997  shslubi  27036  orthin  27097  h1datomi  27232  mdslj2i  27971  mdslmd1lem1  27976  pwuniss  28169  iundifdifd  28179  difres  28213  fresf1o  28233  metideq  28704  hauseqcn  28709  tpr2rico  28726  esumrnmpt2  28897  esumpfinvallem  28903  esum2d  28922  omssubadd  29136  omssubaddOLD  29140  carsggect  29158  omsmeas  29163  omsmeasOLD  29164  orvcelval  29309  signsply0  29448  cvmlift2lem11  30044  cvmlift2lem12  30045  dfon2lem7  30442  filnetlem3  31041  onsucsuccmpi  31108  dissneqlem  31706  icoreunrn  31726  mblfinlem1  31941  ismblfin  31945  sstotbnd2  32070  dochexmidlem4  35000  lcfrlem38  35117  ismrcd1  35509  eldioph2lem2  35572  rmxyelqirr  35728  hbt  35959  rngunsnply  36009  iocinico  36066  dmtrcl  36204  rntrcl  36205  trrelsuperrel2dg  36233  limciccioolb  37641  limcrecl  37649  limcicciooub  37657  stoweidlem50  37851  stoweidlem52  37853  stoweidlem53  37854  stoweidlem57  37858  stoweidlem59  37860  fourierdlem50  37960  fourierdlem103  38013  fourierdlem104  38014  pwsal  38097  sge0iun  38169  sge0isum  38177  meadjuni  38203  omessle  38227  umgr1  39014  uspgr1  39099  zlmodzxzel  39757  lincresunit3  39895
  Copyright terms: Public domain W3C validator