Theorem 3sstr3d 4038

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

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

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 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  cnvtsr  18633  dprdss  20049  dprd2da  20062  dmdprdsplit2lem  20065  mplind  22094  txcmplem1  23649  setsmstopn  24490  tngtopn  24671  bcthlem2  25359  bcthlem4  25361  uniiccvol  25615  dyadmaxlem  25632  dvlip2  26034  dvne0  26050  shlej2  31380  gsumzresunsn  33059  pmtrcnel2  33110  cyc3co2  33160  ssdifidllem  33484  fedgmullem1  33680  hauseqcn  33897  bnd2lem  37798  heiborlem8  37825  dochord  41372  lclkrlem2p  41524  mapdsn  41643  hbtlem5  43140  oaabsb  43307  omabs2  43345  fvmptiunrelexplb0d  43697  fvmptiunrelexplb1d  43699  ovolval5lem3  46669  isclatd  48872