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 1541   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ss 3918

This theorem is referenced by:  cnvtsr  18511  dprdss  19960  dprd2da  19973  dmdprdsplit2lem  19976  mplind  22025  txcmplem1  23585  setsmstopn  24422  tngtopn  24594  bcthlem2  25281  bcthlem4  25283  uniiccvol  25537  dyadmaxlem  25554  dvlip2  25956  dvne0  25972  bdaypw2n0bndlem  28459  shlej2  31436  gsumzresunsn  33145  pmtrcnel2  33172  cyc3co2  33222  ssdifidllem  33537  fedgmullem1  33786  hauseqcn  34055  bnd2lem  37992  heiborlem8  38019  dochord  41630  lclkrlem2p  41782  mapdsn  41901  hbtlem5  43370  oaabsb  43536  omabs2  43574  fvmptiunrelexplb0d  43925  fvmptiunrelexplb1d  43927  ovolval5lem3  46898  isclatd  49228