Theorem sseqtrrd 3232

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 2211	. 2 |- ( ph -> B = C )
4	1, 3	sseqtrd 3231	1 |- ( ph -> A C_ C )

Syntax hints:   -> wi 4   = wceq 1373   C_ wss 3166

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179

This theorem is referenced by:  sseqtrrid  3244  fnfvima  5819  tfrlemiubacc  6416  tfr1onlemubacc  6432  tfrcllemubacc  6445  rdgivallem  6467  nnnninf  7228  nninfwlpoimlemg  7277  ccatass  11064  swrdval2  11104  dfphi2  12542  ctinf  12801  imasaddfnlemg  13146  imasaddvallemg  13147  subsubm  13315  subsubg  13533  subsubrng  13976  subsubrg  14007  lidlss  14238  toponss  14498  ssntr  14594  iscnp3  14675  cnprcl2k  14678  tgcn  14680  tgcnp  14681  ssidcn  14682  cncnp  14702  txcnp  14743  imasnopn  14771  hmeontr  14785  blssec  14910  blssopn  14957  xmettx  14982  metcnp  14984  plyaddlem1  15219  plymullem1  15220  plycoeid3  15229  nnsf  15942  nninfsellemsuc  15949