Theorem 3sstr3d 3977

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3890

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 2709

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

This theorem is referenced by:  cnvtsr  18545  dprdss  19997  dprd2da  20010  dmdprdsplit2lem  20013  mplind  22058  txcmplem1  23616  setsmstopn  24453  tngtopn  24625  bcthlem2  25302  bcthlem4  25304  uniiccvol  25557  dyadmaxlem  25574  dvlip2  25972  dvne0  25988  bdaypw2n0bndlem  28469  shlej2  31447  gsumzresunsn  33138  pmtrcnel2  33166  cyc3co2  33216  ssdifidllem  33531  fedgmullem1  33789  hauseqcn  34058  bnd2lem  38126  heiborlem8  38153  dochord  41830  lclkrlem2p  41982  mapdsn  42101  hbtlem5  43574  oaabsb  43740  omabs2  43778  fvmptiunrelexplb0d  44129  fvmptiunrelexplb1d  44131  ovolval5lem3  47100  isclatd  49470