Theorem 3sstr3d 4013

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-ss 3943

This theorem is referenced by:  cnvtsr  18598  dprdss  20012  dprd2da  20025  dmdprdsplit2lem  20028  mplind  22028  txcmplem1  23579  setsmstopn  24417  tngtopn  24589  bcthlem2  25277  bcthlem4  25279  uniiccvol  25533  dyadmaxlem  25550  dvlip2  25952  dvne0  25968  shlej2  31342  gsumzresunsn  33050  pmtrcnel2  33101  cyc3co2  33151  ssdifidllem  33471  fedgmullem1  33669  hauseqcn  33929  bnd2lem  37815  heiborlem8  37842  dochord  41389  lclkrlem2p  41541  mapdsn  41660  hbtlem5  43152  oaabsb  43318  omabs2  43356  fvmptiunrelexplb0d  43708  fvmptiunrelexplb1d  43710  ovolval5lem3  46683  isclatd  48957