Theorem 3sstr3d 3985

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

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

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 2155  ax-ext 2732

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

This theorem is used by:  cnvtsr  18676  dprdss  20158  dprd2da  20171  dmdprdsplit2lem  20174  ssdifidllem  21547  mplind  22286  txcmplem1  23867  setsmstopn  24704  tngtopn  24876  bcthlem2  25553  bcthlem4  25555  uniiccvol  25808  dyadmaxlem  25825  dvlip2  26222  dvne0  26238  bdaypw2n0bndlem  28728  shlej2  31842  gsumzresunsn  33502  pmtrcnel2  33530  cyc3co2  33580  fedgmullem1  34139  hauseqcn  34408  bnd2lem  38541  heiborlem8  38568  dochord  42243  lclkrlem2p  42395  mapdsn  42514  hbtlem5  43969  oaabsb  44135  omabs2  44173  fvmptiunrelexplb0d  44524  fvmptiunrelexplb1d  44526  ovolval5lem3  47482  isclatd  49909