Theorem sseqtrrd 3231

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)

Hypotheses

Ref	Expression
sseqtrrd.1	|- ( ph -> A C_ B )
sseqtrrd.2	|- ( ph -> C = B )

Assertion

Ref	Expression
sseqtrrd	|- ( ph -> A C_ C )

Proof of Theorem sseqtrrd

Step	Hyp	Ref	Expression
1		sseqtrrd.1	. 2 |- ( ph -> A C_ B )
2		sseqtrrd.2	. . 3 |- ( ph -> C = B )
3	2	eqcomd 2210	. 2 |- ( ph -> B = C )
4	1, 3	sseqtrd 3230	1 |- ( ph -> A C_ C )

Syntax hints:   -> wi 4   = wceq 1372   C_ wss 3165

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-in 3171  df-ss 3178

This theorem is referenced by:  sseqtrrid  3243  fnfvima  5818  tfrlemiubacc  6415  tfr1onlemubacc  6431  tfrcllemubacc  6444  rdgivallem  6466  nnnninf  7227  nninfwlpoimlemg  7276  ccatass  11062  dfphi2  12513  ctinf  12772  imasaddfnlemg  13117  imasaddvallemg  13118  subsubm  13286  subsubg  13504  subsubrng  13947  subsubrg  13978  lidlss  14209  toponss  14469  ssntr  14565  iscnp3  14646  cnprcl2k  14649  tgcn  14651  tgcnp  14652  ssidcn  14653  cncnp  14673  txcnp  14714  imasnopn  14742  hmeontr  14756  blssec  14881  blssopn  14928  xmettx  14953  metcnp  14955  plyaddlem1  15190  plymullem1  15191  plycoeid3  15200  nnsf  15904  nninfsellemsuc  15911