Theorem sseq12d 3258

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 3256	. 2 |- ( ph -> ( A C_ C <-> B C_ C ) )
3		sseq12d.2	. . 3 |- ( ph -> C = D )
4	3	sseq2d 3257	. 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 1397   C_ wss 3200

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  3sstr3d  3271  3sstr4d  3272  ssdifeq0  3577  relcnvtr  5256  rdgisucinc  6551  oawordriexmid  6638  nnaword  6679  nnawordi  6683  sbthlem2  7157  isbth  7166  nninff  7321  nninfninc  7322  infnninf  7323  infnninfOLD  7324  nnnninf  7325  nnnninfeq  7327  nnnninfeq2  7328  nninfwlpoimlemg  7374  swrdval  11233  ennnfonelemkh  13038  ennnfonelemrnh  13042  isstruct2im  13097  isstruct2r  13098  basis1  14777  baspartn  14780  eltg  14782  metss  15224  isausgren  16024  issubgr  16114  subgrprop3  16119  wkslem1  16177  wkslem2  16178  iswlk  16180  wlkres  16236  eupthseg  16309  0nninf  16632  nnsf  16633  peano4nninf  16634  nninfalllem1  16636  nninfself  16641