Theorem 3sstr3d 3962

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

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

This theorem is used by:  cnvtsr  18762  dprdss  20245  dprd2da  20258  dmdprdsplit2lem  20261  ssdifidllem  21640  mplind  22379  txcmplem1  23960  setsmstopn  24797  tngtopn  24969  bcthlem2  25646  bcthlem4  25648  uniiccvol  25901  dyadmaxlem  25918  dvlip2  26315  dvne0  26331  bdaypw2n0bndlem  28849  shlej2  31963  gsumzresunsn  33665  pmtrcnel2  33693  cyc3co2  33743  fedgmullem1  34303  hauseqcn  34572  bnd2lem  38768  heiborlem8  38795  dochord  42470  lclkrlem2p  42622  mapdsn  42741  hbtlem5  44173  oaabsb  44339  omabs2  44377  fvmptiunrelexplb0d  44727  fvmptiunrelexplb1d  44729  ovolval5lem3  47707  isclatd  50134