Theorem 3sstr3d 3992

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

Syntax hints:   → wi 4   = wceq 1570   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3923

This theorem is referenced by:  cnvtsr  18645  dprdss  20102  dprd2da  20115  dmdprdsplit2lem  20118  ssdifidllem  21465  mplind  22202  txcmplem1  23779  setsmstopn  24616  tngtopn  24788  bcthlem2  25465  bcthlem4  25467  uniiccvol  25720  dyadmaxlem  25737  dvlip2  26135  dvne0  26151  bdaypw2n0bndlem  28637  shlej2  31694  gsumzresunsn  33363  pmtrcnel2  33391  cyc3co2  33441  fedgmullem1  34000  hauseqcn  34269  bnd2lem  38423  heiborlem8  38450  dochord  42125  lclkrlem2p  42277  mapdsn  42396  hbtlem5  43838  oaabsb  44004  omabs2  44042  fvmptiunrelexplb0d  44393  fvmptiunrelexplb1d  44395  ovolval5lem3  47351  isclatd  49744