Theorem 3sstr3d 4041

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 4028	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ↔ 𝐶 ⊆ 𝐷))
5	1, 4	mpbid 232	1 ⊢ (𝜑 → 𝐶 ⊆ 𝐷)

Syntax hints:   → wi 4   = wceq 1536   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ss 3979

This theorem is referenced by:  cnvtsr  18645  dprdss  20063  dprd2da  20076  dmdprdsplit2lem  20079  mplind  22111  txcmplem1  23664  setsmstopn  24505  tngtopn  24686  bcthlem2  25372  bcthlem4  25374  uniiccvol  25628  dyadmaxlem  25645  dvlip2  26048  dvne0  26064  shlej2  31389  gsumzresunsn  33041  pmtrcnel2  33092  cyc3co2  33142  ssdifidllem  33463  fedgmullem1  33656  hauseqcn  33858  bnd2lem  37777  heiborlem8  37804  dochord  41352  lclkrlem2p  41504  mapdsn  41623  hbtlem5  43116  oaabsb  43283  omabs2  43321  fvmptiunrelexplb0d  43673  fvmptiunrelexplb1d  43675  ovolval5lem3  46609  isclatd  48771