Theorem 3sstr3d 3993

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

Syntax hints:   → wi 4   = wceq 1563   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ss 3924

This theorem is referenced by:  cnvtsr  18632  dprdss  20089  dprd2da  20102  dmdprdsplit2lem  20105  ssdifidllem  21441  mplind  22178  txcmplem1  23755  setsmstopn  24592  tngtopn  24764  bcthlem2  25441  bcthlem4  25443  uniiccvol  25696  dyadmaxlem  25713  dvlip2  26111  dvne0  26127  bdaypw2n0bndlem  28610  shlej2  31618  gsumzresunsn  33290  pmtrcnel2  33318  cyc3co2  33368  fedgmullem1  33931  hauseqcn  34200  bnd2lem  38297  heiborlem8  38324  dochord  42001  lclkrlem2p  42153  mapdsn  42272  hbtlem5  43712  oaabsb  43878  omabs2  43916  fvmptiunrelexplb0d  44267  fvmptiunrelexplb1d  44269  ovolval5lem3  47227  isclatd  49613