Theorem sseq12d 3256

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 3254	. 2 |- ( ph -> ( A C_ C <-> B C_ C ) )
3		sseq12d.2	. . 3 |- ( ph -> C = D )
4	3	sseq2d 3255	. 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 1395   C_ wss 3198

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3204  df-ss 3211

This theorem is referenced by:  3sstr3d  3269  3sstr4d  3270  ssdifeq0  3575  relcnvtr  5254  rdgisucinc  6546  oawordriexmid  6633  nnaword  6674  nnawordi  6678  sbthlem2  7148  isbth  7157  nninff  7312  nninfninc  7313  infnninf  7314  infnninfOLD  7315  nnnninf  7316  nnnninfeq  7318  nnnninfeq2  7319  nninfwlpoimlemg  7365  swrdval  11219  ennnfonelemkh  13023  ennnfonelemrnh  13027  isstruct2im  13082  isstruct2r  13083  basis1  14761  baspartn  14764  eltg  14766  metss  15208  isausgren  16006  wkslem1  16117  wkslem2  16118  iswlk  16120  wlkres  16174  eupthseg  16247  0nninf  16542  nnsf  16543  peano4nninf  16544  nninfalllem1  16546  nninfself  16551