Theorem sseq12d 3256

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

Hypotheses

Ref	Expression
sseq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)
sseq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
sseq12d	⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷))

Proof of Theorem sseq12d

Step	Hyp	Ref	Expression
1		sseq1d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	sseq1d 3254	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
3		sseq12d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
4	3	sseq2d 3255	. 2 ⊢ (𝜑 → (𝐵 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷))
5	2, 4	bitrd 188	1 ⊢ (𝜑 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐷))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1395   ⊆ 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  7151  isbth  7160  nninff  7315  nninfninc  7316  infnninf  7317  infnninfOLD  7318  nnnninf  7319  nnnninfeq  7321  nnnninfeq2  7322  nninfwlpoimlemg  7368  swrdval  11222  ennnfonelemkh  13026  ennnfonelemrnh  13030  isstruct2im  13085  isstruct2r  13086  basis1  14764  baspartn  14767  eltg  14769  metss  15211  isausgren  16011  wkslem1  16131  wkslem2  16132  iswlk  16134  wlkres  16188  eupthseg  16261  0nninf  16556  nnsf  16557  peano4nninf  16558  nninfalllem1  16560  nninfself  16565