Theorem sseqtrd 3205

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

Hypotheses

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

Assertion

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

Proof of Theorem sseqtrd

Step	Hyp	Ref	Expression
1		sseqtrd.1	. 2 |- ( ph -> A C_ B )
2		sseqtrd.2	. . 3 |- ( ph -> B = C )
3	2	sseq2d 3197	. 2 |- ( ph -> ( A C_ B <-> A C_ C ) )
4	1, 3	mpbid 147	1 |- ( ph -> A C_ C )

Syntax hints:   -> wi 4   = wceq 1363   C_ wss 3141

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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-11 1516  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-in 3147  df-ss 3154

This theorem is referenced by:  sseqtrrd  3206  fssdmd  5391  resasplitss  5407  nnaword2  6529  erssxp  6572  phpm  6879  nnnninfeq  7140  ioodisj  10007  subsubm  12896  subsubg  13097  trivsubgd  13100  trivnsgd  13117  subsubrng  13491  subrgugrp  13517  subsubrg  13522  islssmd  13605  lspun  13648  lspssp  13649  lsslsp  13675  tgcl  13917  basgen  13933  bastop1  13936  bastop2  13937  clsss2  13982  topssnei  14015  cnntr  14078  txbasval  14120  neitx  14121  cnmpt1res  14149  cnmpt2res  14150  imasnopn  14152  hmeontr  14166  tgioo  14399  reldvg  14501  dvfvalap  14503  dvbss  14507  dvcnp2cntop  14516  dvaddxxbr  14518  dvmulxxbr  14519  dvcj  14526