Theorem sseqtrd 3235

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 25-Apr-2004.)

Hypotheses

Ref	Expression
sseqtrd.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
sseqtrd.2	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
sseqtrd	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem sseqtrd

Step	Hyp	Ref	Expression
1		sseqtrd.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		sseqtrd.2	. . 3 ⊢ (𝜑 → 𝐵 = 𝐶)
3	2	sseq2d 3227	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐶))
4	1, 3	mpbid 147	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1373   ⊆ wss 3170

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-in 3176  df-ss 3183

This theorem is referenced by:  sseqtrrd  3236  fssdmd  5448  resasplitss  5466  nnaword2  6612  erssxp  6655  phpm  6976  nninfninc  7239  nnnninfeq  7244  ioodisj  10130  subsubm  13385  subsubg  13603  trivsubgd  13606  trivnsgd  13623  subsubrng  14046  subrgugrp  14072  subsubrg  14077  islssmd  14191  lspun  14234  lspssp  14235  lsslsp  14261  tgcl  14606  basgen  14622  bastop1  14625  bastop2  14626  clsss2  14671  topssnei  14704  cnntr  14767  txbasval  14809  neitx  14810  cnmpt1res  14838  cnmpt2res  14839  imasnopn  14841  hmeontr  14855  tgioo  15096  reldvg  15221  dvfvalap  15223  dvbss  15227  dvcnp2cntop  15241  dvaddxxbr  15243  dvmulxxbr  15244  dvcj  15251