Theorem 3sstr3d 3967

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  cnvtsr  18812  dprdss  20296  dprd2da  20309  dmdprdsplit2lem  20312  ssdifidllem  21691  mplind  22434  txcmplem1  24015  setsmstopn  24852  tngtopn  25024  bcthlem2  25701  bcthlem4  25703  uniiccvol  25956  dyadmaxlem  25973  dvlip2  26370  dvne0  26386  bdaypw2n0bndlem  28906  shlej2  32020  gsumzresunsn  33722  pmtrcnel2  33750  cyc3co2  33800  fedgmullem1  34372  hauseqcn  34641  bnd2lem  38991  heiborlem8  39018  dochord  42693  lclkrlem2p  42845  mapdsn  42964  hbtlem5  44395  oaabsb  44557  omabs2  44595  fvmptiunrelexplb0d  44945  fvmptiunrelexplb1d  44947  ovolval5lem3  47937  isclatd  50428