Theorem sseqtrd 3262

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 3254	. 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐶))
4	1, 3	mpbid 147	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1395   ⊆ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  sseqtrrd  3263  fssdmd  5486  resasplitss  5504  nnaword2  6658  erssxp  6701  phpm  7023  nninfninc  7286  nnnninfeq  7291  ioodisj  10185  subsubm  13511  subsubg  13729  trivsubgd  13732  trivnsgd  13749  subsubrng  14172  subrgugrp  14198  subsubrg  14203  islssmd  14317  lspun  14360  lspssp  14361  lsslsp  14387  tgcl  14732  basgen  14748  bastop1  14751  bastop2  14752  clsss2  14797  topssnei  14830  cnntr  14893  txbasval  14935  neitx  14936  cnmpt1res  14964  cnmpt2res  14965  imasnopn  14967  hmeontr  14981  tgioo  15222  reldvg  15347  dvfvalap  15349  dvbss  15353  dvcnp2cntop  15367  dvaddxxbr  15369  dvmulxxbr  15370  dvcj  15377