Theorem 3sstr3d 3961

Description: Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 1-Oct-2000.)

Hypotheses

Ref	Expression
3sstr3d.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
3sstr3d.2	⊢ (𝜑 → 𝐴 = 𝐶)
3sstr3d.3	⊢ (𝜑 → 𝐵 = 𝐷)

Assertion

Ref	Expression
3sstr3d	⊢ (𝜑 → 𝐶 ⊆ 𝐷)

Proof of Theorem 3sstr3d

Step	Hyp	Ref	Expression
1		3sstr3d.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		3sstr3d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐶)
3		3sstr3d.3	. . 3 ⊢ (𝜑 → 𝐵 = 𝐷)
4	2, 3	sseq12d 3948	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ↔ 𝐶 ⊆ 𝐷))
5	1, 4	mpbid 235	1 ⊢ (𝜑 → 𝐶 ⊆ 𝐷)

Syntax hints:   → wi 4   = wceq 1538   ⊆ wss 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  cnvtsr  17824  dprdss  19144  dprd2da  19157  dmdprdsplit2lem  19160  mplind  20741  txcmplem1  22246  setsmstopn  23085  tngtopn  23256  bcthlem2  23929  bcthlem4  23931  uniiccvol  24184  dyadmaxlem  24201  dvlip2  24598  dvne0  24614  shlej2  29144  gsumzresunsn  30739  pmtrcnel2  30784  cyc3co2  30832  fedgmullem1  31113  hauseqcn  31251  bnd2lem  35229  heiborlem8  35256  dochord  38666  lclkrlem2p  38818  mapdsn  38937  hbtlem5  40072  fvmptiunrelexplb0d  40385  fvmptiunrelexplb1d  40387