Theorem sseqtrd 3280

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

Syntax hints:   → wi 4   = wceq 1398   ⊆ wss 3214

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227

This theorem is referenced by:  sseqtrrd  3281  fssdmd  5528  resasplitss  5549  nnaword2  6760  erssxp  6803  phpm  7133  nninfninc  7427  nnnninfeq  7432  ioodisj  10345  subsubm  13738  subsubg  13950  trivsubgd  13953  trivnsgd  13970  subsubrng  14460  subrgugrp  14486  subsubrg  14491  islssmd  14633  lspun  14676  lspssp  14677  lsslsp  14703  tgcl  15055  basgen  15071  bastop1  15074  bastop2  15075  clsss2  15120  topssnei  15153  cnntr  15216  txbasval  15258  neitx  15259  cnmpt1res  15287  cnmpt2res  15288  imasnopn  15290  hmeontr  15304  tgioo  15545  reldvg  15670  dvfvalap  15672  dvbss  15676  dvcnp2cntop  15690  dvaddxxbr  15692  dvmulxxbr  15693  dvcj  15700  vtxdumgrfival  16419