Theorem 3sstr3d 3990

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3920

This theorem is referenced by:  cnvtsr  18523  dprdss  19972  dprd2da  19985  dmdprdsplit2lem  19988  mplind  22037  txcmplem1  23597  setsmstopn  24434  tngtopn  24606  bcthlem2  25293  bcthlem4  25295  uniiccvol  25549  dyadmaxlem  25566  dvlip2  25968  dvne0  25984  bdaypw2n0bndlem  28471  shlej2  31448  gsumzresunsn  33155  pmtrcnel2  33183  cyc3co2  33233  ssdifidllem  33548  fedgmullem1  33806  hauseqcn  34075  bnd2lem  38039  heiborlem8  38066  dochord  41743  lclkrlem2p  41895  mapdsn  42014  hbtlem5  43482  oaabsb  43648  omabs2  43686  fvmptiunrelexplb0d  44037  fvmptiunrelexplb1d  44039  ovolval5lem3  47009  isclatd  49339