Theorem 3sstr3d 4028

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3948

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965

This theorem is referenced by:  cnvtsr  18543  dprdss  19901  dprd2da  19914  dmdprdsplit2lem  19917  mplind  21637  txcmplem1  23152  setsmstopn  23993  tngtopn  24174  bcthlem2  24849  bcthlem4  24851  uniiccvol  25104  dyadmaxlem  25121  dvlip2  25519  dvne0  25535  shlej2  30652  gsumzresunsn  32247  pmtrcnel2  32292  cyc3co2  32340  fedgmullem1  32773  hauseqcn  32947  bnd2lem  36745  heiborlem8  36772  dochord  40327  lclkrlem2p  40479  mapdsn  40598  hbtlem5  41952  oaabsb  42126  omabs2  42164  fvmptiunrelexplb0d  42517  fvmptiunrelexplb1d  42519  ovolval5lem3  45449  isclatd  47686