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 1540   ⊆ wss 3905

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 2701

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

This theorem is referenced by:  cnvtsr  18512  dprdss  19928  dprd2da  19941  dmdprdsplit2lem  19944  mplind  21993  txcmplem1  23544  setsmstopn  24382  tngtopn  24554  bcthlem2  25241  bcthlem4  25243  uniiccvol  25497  dyadmaxlem  25514  dvlip2  25916  dvne0  25932  shlej2  31323  gsumzresunsn  33022  pmtrcnel2  33045  cyc3co2  33095  ssdifidllem  33406  fedgmullem1  33604  hauseqcn  33867  bnd2lem  37773  heiborlem8  37800  dochord  41352  lclkrlem2p  41504  mapdsn  41623  hbtlem5  43104  oaabsb  43270  omabs2  43308  fvmptiunrelexplb0d  43660  fvmptiunrelexplb1d  43662  ovolval5lem3  46639  isclatd  48971