Theorem sseq12d 3228

Description: An equality deduction for the subclass relationship. (Contributed by NM, 31-May-1999.)

Hypotheses

Ref	Expression
sseq1d.1	|- ( ph -> A = B )
sseq12d.2	|- ( ph -> C = D )

Assertion

Ref	Expression
sseq12d	|- ( ph -> ( A C_ C <-> B C_ D ) )

Proof of Theorem sseq12d

Step	Hyp	Ref	Expression
1		sseq1d.1	. . 3 |- ( ph -> A = B )
2	1	sseq1d 3226	. 2 |- ( ph -> ( A C_ C <-> B C_ C ) )
3		sseq12d.2	. . 3 |- ( ph -> C = D )
4	3	sseq2d 3227	. 2 |- ( ph -> ( B C_ C <-> B C_ D ) )
5	2, 4	bitrd 188	1 |- ( ph -> ( A C_ C <-> B C_ D ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1373   C_ wss 3170

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-in 3176  df-ss 3183

This theorem is referenced by:  3sstr3d  3241  3sstr4d  3242  ssdifeq0  3547  relcnvtr  5211  rdgisucinc  6484  oawordriexmid  6569  nnaword  6610  nnawordi  6614  sbthlem2  7075  isbth  7084  nninff  7239  nninfninc  7240  infnninf  7241  infnninfOLD  7242  nnnninf  7243  nnnninfeq  7245  nnnninfeq2  7246  nninfwlpoimlemg  7292  swrdval  11124  ennnfonelemkh  12858  ennnfonelemrnh  12862  isstruct2im  12917  isstruct2r  12918  basis1  14594  baspartn  14597  eltg  14599  metss  15041  0nninf  16082  nnsf  16083  peano4nninf  16084  nninfalllem1  16086  nninfself  16091