Theorem 3sstr3d 3988

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.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐶)
2		3sstr3d.1	. . 3 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
3	1, 2	eqsstrrd 3969	. 2 ⊢ (𝜑 → 𝐶 ⊆ 𝐵)
4		3sstr3d.3	. 2 ⊢ (𝜑 → 𝐵 = 𝐷)
5	3, 4	sseqtrd 3970	1 ⊢ (𝜑 → 𝐶 ⊆ 𝐷)

Syntax hints:   → wi 4   = wceq 1559   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ss 3919

This theorem is referenced by:  cnvtsr  18610  dprdss  20061  dprd2da  20074  dmdprdsplit2lem  20077  mplind  22110  txcmplem1  23688  setsmstopn  24525  tngtopn  24697  bcthlem2  25374  bcthlem4  25376  uniiccvol  25629  dyadmaxlem  25646  dvlip2  26044  dvne0  26060  bdaypw2n0bndlem  28543  shlej2  31520  gsumzresunsn  33202  pmtrcnel2  33230  cyc3co2  33280  ssdifidllem  33603  fedgmullem1  33886  hauseqcn  34155  bnd2lem  38250  heiborlem8  38277  dochord  41954  lclkrlem2p  42106  mapdsn  42225  hbtlem5  43665  oaabsb  43831  omabs2  43869  fvmptiunrelexplb0d  44220  fvmptiunrelexplb1d  44222  ovolval5lem3  47188  isclatd  49564