Theorem 3sstr3d 4004

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

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

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 2008  ax-9 2119  ax-ext 2702

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

This theorem is referenced by:  cnvtsr  18554  dprdss  19968  dprd2da  19981  dmdprdsplit2lem  19984  mplind  21984  txcmplem1  23535  setsmstopn  24373  tngtopn  24545  bcthlem2  25232  bcthlem4  25234  uniiccvol  25488  dyadmaxlem  25505  dvlip2  25907  dvne0  25923  shlej2  31297  gsumzresunsn  33003  pmtrcnel2  33054  cyc3co2  33104  ssdifidllem  33434  fedgmullem1  33632  hauseqcn  33895  bnd2lem  37792  heiborlem8  37819  dochord  41371  lclkrlem2p  41523  mapdsn  41642  hbtlem5  43124  oaabsb  43290  omabs2  43328  fvmptiunrelexplb0d  43680  fvmptiunrelexplb1d  43682  ovolval5lem3  46659  isclatd  48975