Theorem 3sstr3d 4001

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3931

This theorem is referenced by:  cnvtsr  18547  dprdss  19961  dprd2da  19974  dmdprdsplit2lem  19977  mplind  21977  txcmplem1  23528  setsmstopn  24366  tngtopn  24538  bcthlem2  25225  bcthlem4  25227  uniiccvol  25481  dyadmaxlem  25498  dvlip2  25900  dvne0  25916  shlej2  31290  gsumzresunsn  32996  pmtrcnel2  33047  cyc3co2  33097  ssdifidllem  33427  fedgmullem1  33625  hauseqcn  33888  bnd2lem  37785  heiborlem8  37812  dochord  41364  lclkrlem2p  41516  mapdsn  41635  hbtlem5  43117  oaabsb  43283  omabs2  43321  fvmptiunrelexplb0d  43673  fvmptiunrelexplb1d  43675  ovolval5lem3  46652  isclatd  48971