Theorem 3sstr3d 3976

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

Syntax hints:   → wi 4   = wceq 1547   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ss 3907

This theorem is referenced by:  cnvtsr  18552  dprdss  20004  dprd2da  20017  dmdprdsplit2lem  20020  mplind  22053  txcmplem1  23631  setsmstopn  24468  tngtopn  24640  bcthlem2  25317  bcthlem4  25319  uniiccvol  25572  dyadmaxlem  25589  dvlip2  25987  dvne0  26003  bdaypw2n0bndlem  28480  shlej2  31457  gsumzresunsn  33150  pmtrcnel2  33178  cyc3co2  33228  ssdifidllem  33546  fedgmullem1  33820  hauseqcn  34089  bnd2lem  38165  heiborlem8  38192  dochord  41869  lclkrlem2p  42021  mapdsn  42140  hbtlem5  43580  oaabsb  43746  omabs2  43784  fvmptiunrelexplb0d  44135  fvmptiunrelexplb1d  44137  ovolval5lem3  47104  isclatd  49480