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 2733

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

This theorem is used by:  cnvtsr  18755  dprdss  20238  dprd2da  20251  dmdprdsplit2lem  20254  ssdifidllem  21633  mplind  22372  txcmplem1  23953  setsmstopn  24790  tngtopn  24962  bcthlem2  25639  bcthlem4  25641  uniiccvol  25894  dyadmaxlem  25911  dvlip2  26308  dvne0  26324  bdaypw2n0bndlem  28842  shlej2  31956  gsumzresunsn  33616  pmtrcnel2  33644  cyc3co2  33694  fedgmullem1  34254  hauseqcn  34523  bnd2lem  38705  heiborlem8  38732  dochord  42407  lclkrlem2p  42559  mapdsn  42678  hbtlem5  44114  oaabsb  44280  omabs2  44318  fvmptiunrelexplb0d  44669  fvmptiunrelexplb1d  44671  ovolval5lem3  47633  isclatd  50060