Theorem 3sstr3d 3993

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

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

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 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930

This theorem is referenced by:  cnvtsr  18491  dprdss  19822  dprd2da  19835  dmdprdsplit2lem  19838  mplind  21515  txcmplem1  23029  setsmstopn  23870  tngtopn  24051  bcthlem2  24726  bcthlem4  24728  uniiccvol  24981  dyadmaxlem  24998  dvlip2  25396  dvne0  25412  shlej2  30366  gsumzresunsn  31966  pmtrcnel2  32011  cyc3co2  32059  fedgmullem1  32411  hauseqcn  32568  bnd2lem  36323  heiborlem8  36350  dochord  39906  lclkrlem2p  40058  mapdsn  40177  hbtlem5  41513  oaabsb  41687  omabs2  41725  fvmptiunrelexplb0d  42078  fvmptiunrelexplb1d  42080  ovolval5lem3  45015  isclatd  47128