Theorem sseqtrd 3193

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 3185	. 2 |- ( ph -> ( A C_ B <-> A C_ C ) )
4	1, 3	mpbid 147	1 |- ( ph -> A C_ C )

Syntax hints:   -> wi 4   = wceq 1353   C_ wss 3129

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3135  df-ss 3142

This theorem is referenced by:  sseqtrrd  3194  fssdmd  5379  resasplitss  5395  nnaword2  6514  erssxp  6557  phpm  6864  nnnninfeq  7125  ioodisj  9992  subsubg  13055  trivsubgd  13058  trivnsgd  13075  subrgugrp  13359  subsubrg  13364  tgcl  13534  basgen  13550  bastop1  13553  bastop2  13554  clsss2  13599  topssnei  13632  cnntr  13695  txbasval  13737  neitx  13738  cnmpt1res  13766  cnmpt2res  13767  imasnopn  13769  hmeontr  13783  tgioo  14016  reldvg  14118  dvfvalap  14120  dvbss  14124  dvcnp2cntop  14133  dvaddxxbr  14135  dvmulxxbr  14136  dvcj  14143