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  18768  dprdss  20251  dprd2da  20264  dmdprdsplit2lem  20267  ssdifidllem  21646  mplind  22385  txcmplem1  23966  setsmstopn  24803  tngtopn  24975  bcthlem2  25652  bcthlem4  25654  uniiccvol  25907  dyadmaxlem  25924  dvlip2  26321  dvne0  26337  bdaypw2n0bndlem  28855  shlej2  31969  gsumzresunsn  33670  pmtrcnel2  33698  cyc3co2  33748  fedgmullem1  34308  hauseqcn  34577  bnd2lem  38819  heiborlem8  38846  dochord  42521  lclkrlem2p  42673  mapdsn  42792  hbtlem5  44224  oaabsb  44390  omabs2  44428  fvmptiunrelexplb0d  44778  fvmptiunrelexplb1d  44780  ovolval5lem3  47758  isclatd  50191