Theorem 3sstr3d 3989

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ss 3919

This theorem is referenced by:  cnvtsr  18494  dprdss  19944  dprd2da  19957  dmdprdsplit2lem  19960  mplind  22006  txcmplem1  23557  setsmstopn  24394  tngtopn  24566  bcthlem2  25253  bcthlem4  25255  uniiccvol  25509  dyadmaxlem  25526  dvlip2  25928  dvne0  25944  shlej2  31339  gsumzresunsn  33034  pmtrcnel2  33057  cyc3co2  33107  ssdifidllem  33419  fedgmullem1  33640  hauseqcn  33909  bnd2lem  37837  heiborlem8  37864  dochord  41415  lclkrlem2p  41567  mapdsn  41686  hbtlem5  43167  oaabsb  43333  omabs2  43371  fvmptiunrelexplb0d  43723  fvmptiunrelexplb1d  43725  ovolval5lem3  46698  isclatd  49020