Theorem 3sstr3d 4027

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

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3947

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3954  df-ss 3964

This theorem is referenced by:  cnvtsr  18545  dprdss  19940  dprd2da  19953  dmdprdsplit2lem  19956  mplind  21850  txcmplem1  23365  setsmstopn  24206  tngtopn  24387  bcthlem2  25073  bcthlem4  25075  uniiccvol  25329  dyadmaxlem  25346  dvlip2  25747  dvne0  25763  shlej2  30881  gsumzresunsn  32476  pmtrcnel2  32521  cyc3co2  32569  fedgmullem1  33002  hauseqcn  33176  bnd2lem  36962  heiborlem8  36989  dochord  40544  lclkrlem2p  40696  mapdsn  40815  hbtlem5  42172  oaabsb  42346  omabs2  42384  fvmptiunrelexplb0d  42737  fvmptiunrelexplb1d  42739  ovolval5lem3  45668  isclatd  47695