Theorem 3sstr3d 3985

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3898

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 2705

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

This theorem is referenced by:  cnvtsr  18498  dprdss  19947  dprd2da  19960  dmdprdsplit2lem  19963  mplind  22008  txcmplem1  23559  setsmstopn  24396  tngtopn  24568  bcthlem2  25255  bcthlem4  25257  uniiccvol  25511  dyadmaxlem  25528  dvlip2  25930  dvne0  25946  shlej2  31345  gsumzresunsn  33045  pmtrcnel2  33068  cyc3co2  33118  ssdifidllem  33430  fedgmullem1  33665  hauseqcn  33934  bnd2lem  37854  heiborlem8  37881  dochord  41492  lclkrlem2p  41644  mapdsn  41763  hbtlem5  43248  oaabsb  43414  omabs2  43452  fvmptiunrelexplb0d  43804  fvmptiunrelexplb1d  43806  ovolval5lem3  46779  isclatd  49110