Theorem 3sstr3d 3843

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.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		3sstr3d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐶)
3		3sstr3d.3	. . 3 ⊢ (𝜑 → 𝐵 = 𝐷)
4	2, 3	sseq12d 3830	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ↔ 𝐶 ⊆ 𝐷))
5	1, 4	mpbid 224	1 ⊢ (𝜑 → 𝐶 ⊆ 𝐷)

Syntax hints:   → wi 4   = wceq 1653   ⊆ wss 3769

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-in 3776  df-ss 3783

This theorem is referenced by:  cnvtsr  17537  dprdss  18744  dprd2da  18757  dmdprdsplit2lem  18760  mplind  19824  txcmplem1  21773  setsmstopn  22611  tngtopn  22782  bcthlem2  23451  bcthlem4  23453  uniiccvol  23688  dyadmaxlem  23705  dvlip2  24099  dvne0  24115  shlej2  28745  hauseqcn  30457  bnd2lem  34077  heiborlem8  34104  dochord  37391  lclkrlem2p  37543  mapdsn  37662  hbtlem5  38483  fvmptiunrelexplb0d  38759  fvmptiunrelexplb1d  38761