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  18543  dprdss  19995  dprd2da  20008  dmdprdsplit2lem  20011  mplind  22057  txcmplem1  23615  setsmstopn  24452  tngtopn  24624  bcthlem2  25301  bcthlem4  25303  uniiccvol  25556  dyadmaxlem  25573  dvlip2  25972  dvne0  25988  bdaypw2n0bndlem  28474  shlej2  31452  gsumzresunsn  33143  pmtrcnel2  33171  cyc3co2  33221  ssdifidllem  33536  fedgmullem1  33794  hauseqcn  34063  bnd2lem  38123  heiborlem8  38150  dochord  41827  lclkrlem2p  41979  mapdsn  42098  hbtlem5  43571  oaabsb  43737  omabs2  43775  fvmptiunrelexplb0d  44126  fvmptiunrelexplb1d  44128  ovolval5lem3  47097  isclatd  49455