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 1542   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ss 3906

This theorem is referenced by:  cnvtsr  18554  dprdss  20006  dprd2da  20019  dmdprdsplit2lem  20022  mplind  22048  txcmplem1  23606  setsmstopn  24443  tngtopn  24615  bcthlem2  25292  bcthlem4  25294  uniiccvol  25547  dyadmaxlem  25564  dvlip2  25962  dvne0  25978  bdaypw2n0bndlem  28455  shlej2  31432  gsumzresunsn  33123  pmtrcnel2  33151  cyc3co2  33201  ssdifidllem  33516  fedgmullem1  33773  hauseqcn  34042  bnd2lem  38112  heiborlem8  38139  dochord  41816  lclkrlem2p  41968  mapdsn  42087  hbtlem5  43556  oaabsb  43722  omabs2  43760  fvmptiunrelexplb0d  44111  fvmptiunrelexplb1d  44113  ovolval5lem3  47082  isclatd  49458