Theorem 3sstr3d 4055

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

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993

This theorem is referenced by:  cnvtsr  18658  dprdss  20073  dprd2da  20086  dmdprdsplit2lem  20089  mplind  22117  txcmplem1  23670  setsmstopn  24511  tngtopn  24692  bcthlem2  25378  bcthlem4  25380  uniiccvol  25634  dyadmaxlem  25651  dvlip2  26054  dvne0  26070  shlej2  31393  gsumzresunsn  33037  pmtrcnel2  33083  cyc3co2  33133  ssdifidllem  33449  fedgmullem1  33642  hauseqcn  33844  bnd2lem  37751  heiborlem8  37778  dochord  41327  lclkrlem2p  41479  mapdsn  41598  hbtlem5  43085  oaabsb  43256  omabs2  43294  fvmptiunrelexplb0d  43646  fvmptiunrelexplb1d  43648  ovolval5lem3  46575  isclatd  48655