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 ⊢ (𝜑 → 𝐶 ⊆ 𝐷)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-ss 3923

This theorem is used by:  cnvtsr  18661  dprdss  20124  dprd2da  20137  dmdprdsplit2lem  20140  ssdifidllem  21513  mplind  22250  txcmplem1  23827  setsmstopn  24664  tngtopn  24836  bcthlem2  25513  bcthlem4  25515  uniiccvol  25768  dyadmaxlem  25785  dvlip2  26183  dvne0  26199  bdaypw2n0bndlem  28685  shlej2  31742  gsumzresunsn  33405  pmtrcnel2  33433  cyc3co2  33483  fedgmullem1  34042  hauseqcn  34311  bnd2lem  38475  heiborlem8  38502  dochord  42177  lclkrlem2p  42329  mapdsn  42448  hbtlem5  43888  oaabsb  44054  omabs2  44092  fvmptiunrelexplb0d  44443  fvmptiunrelexplb1d  44445  ovolval5lem3  47401  isclatd  49794