Theorem sseqtrid 3197

Description: Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypotheses

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

Assertion

Ref	Expression
sseqtrid	⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Proof of Theorem sseqtrid

Step	Hyp	Ref	Expression
1		sseqtrid.2	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
2		sseqtrid.1	. 2 ⊢ 𝐵 ⊆ 𝐴
3		sseq2 3171	. . 3 ⊢ (𝐴 = 𝐶 → (𝐵 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐶))
4	3	biimpa 294	. 2 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ⊆ 𝐶)
5	1, 2, 4	sylancl 411	1 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1348   ⊆ wss 3121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134

This theorem is referenced by:  fssdm  5360  fndmdif  5598  fneqeql2  5602  fconst4m  5713  f1opw2  6052  ecss  6550  fopwdom  6810  ssenen  6825  phplem2  6827  fiintim  6902  casefun  7058  caseinj  7062  djufun  7077  djuinj  7079  nn0supp  9174  monoord2  10420  binom1dif  11437  cnpnei  12934  cnntri  12939  cnntr  12940  cncnp  12945  cndis  12956  txdis1cn  12993  hmeontr  13028  hmeoimaf1o  13029  dvcoapbr  13386