Theorem syl6sseq 3651

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

Step	Hyp	Ref	Expression
1		syl6sseq.1	. 2 |- ( ph -> A C_ B )
2		syl6sseq.2	. . 3 |- B = C
3	2	sseq2i 3630	. 2 |- ( A C_ B <-> A C_ C )
4	1, 3	sylib 208	1 |- ( ph -> A C_ C )

Syntax hints:   -> wi 4   = wceq 1483   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  syl6sseqr  3652  sofld  5581  relrelss  5659  foimacnv  6154  onfununi  7438  hartogslem1  8447  cantnfp1lem3  8577  uniwf  8682  rankeq0b  8723  cflecard  9075  fin23lem16  9157  fin23lem41  9174  pwcfsdom  9405  fpwwe2lem13  9464  fpwwe2  9465  canth4  9469  hashbclem  13236  dmtrclfv  13759  zsum  14449  fsumcvg3  14460  incexclem  14568  zprod  14667  ramub1lem1  15730  setsstruct2  15896  imasaddfnlem  16188  imasvscafn  16197  mremre  16264  submre  16265  mreexexlem3d  16306  isacs1i  16318  acsmapd  17178  acsmap2d  17179  gsumzoppg  18344  lspsntri  19097  lsppratlem4  19150  lbsextlem3  19160  distop  20799  elcls  20877  cnpresti  21092  cnprest  21093  cmpcld  21205  cnconn  21225  iunconn  21231  comppfsc  21335  ptuni2  21379  alexsubALTlem3  21853  ustssco  22018  ust0  22023  ustbas2  22029  ustimasn  22032  utopbas  22039  utop2nei  22054  setsmstopn  22283  metustsym  22360  metust  22363  tngtopn  22454  ovoliunlem1  23270  lhop1lem  23776  ig1peu  23931  ig1pdvds  23936  logccv  24409  amgmlem  24716  upgr1e  26008  uspgr1e  26136  shsupcl  28197  shsupunss  28205  shslubi  28244  orthin  28305  h1datomi  28440  mdslj2i  29179  mdslmd1lem1  29184  pwuniss  29370  iundifdifd  29380  difres  29413  fresf1o  29433  metideq  29936  hauseqcn  29941  tpr2rico  29958  esumrnmpt2  30130  esumpfinvallem  30136  esum2d  30155  omssubadd  30362  carsggect  30380  omsmeas  30385  orvcelval  30530  signsply0  30628  cvmlift2lem11  31295  cvmlift2lem12  31296  dfon2lem7  31694  filnetlem3  32375  onsucsuccmpi  32442  dissneqlem  33187  icoreunrn  33207  mblfinlem1  33446  ismblfin  33450  sstotbnd2  33573  dochexmidlem4  36752  lcfrlem38  36869  ismrcd1  37261  eldioph2lem2  37324  rmxyelqirr  37475  hbt  37700  rngunsnply  37743  iocinico  37797  dmtrcl  37934  rntrcl  37935  trrelsuperrel2dg  37963  restuni5  39306  unirnmapsn  39406  limciccioolb  39853  limcrecl  39861  limcicciooub  39869  stoweidlem50  40267  stoweidlem52  40269  stoweidlem53  40270  stoweidlem57  40274  stoweidlem59  40276  fourierdlem50  40373  fourierdlem103  40426  fourierdlem104  40427  pwsal  40535  sge0iun  40636  sge0isum  40644  meadjuni  40674  omessle  40712  zlmodzxzel  42133  lincresunit3  42270  amgmwlem  42548