Theorem sseq12d 3178

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 3176	. 2 |- ( ph -> ( A C_ C <-> B C_ C ) )
3		sseq12d.2	. . 3 |- ( ph -> C = D )
4	3	sseq2d 3177	. 2 |- ( ph -> ( B C_ C <-> B C_ D ) )
5	2, 4	bitrd 187	1 |- ( ph -> ( A C_ C <-> B C_ D ) )

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1348   C_ wss 3121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134

This theorem is referenced by:  3sstr3d  3191  3sstr4d  3192  ssdifeq0  3497  relcnvtr  5130  rdgisucinc  6364  oawordriexmid  6449  nnaword  6490  nnawordi  6494  sbthlem2  6935  isbth  6944  nninff  7099  infnninf  7100  infnninfOLD  7101  nnnninf  7102  nnnninfeq  7104  nnnninfeq2  7105  nninfwlpoimlemg  7151  ennnfonelemkh  12367  ennnfonelemrnh  12371  isstruct2im  12426  isstruct2r  12427  ressid2  12477  ressval2  12478  basis1  12839  baspartn  12842  eltg  12846  metss  13288  0nninf  14037  nnsf  14038  peano4nninf  14039  nninfalllem1  14041  nninfself  14046