Theorem syl5sseq 3077

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

Hypotheses

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

Assertion

Ref	Expression
syl5sseq	⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Proof of Theorem syl5sseq

Step	Hyp	Ref	Expression
1		syl5sseq.2	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
2		syl5sseq.1	. 2 ⊢ 𝐵 ⊆ 𝐴
3		sseq2 3051	. . 3 ⊢ (𝐴 = 𝐶 → (𝐵 ⊆ 𝐴 ↔ 𝐵 ⊆ 𝐶))
4	3	biimpa 291	. 2 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 ⊆ 𝐴) → 𝐵 ⊆ 𝐶)
5	1, 2, 4	sylancl 405	1 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1290   ⊆ wss 3002

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-11 1443  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071

This theorem depends on definitions:  df-bi 116  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-in 3008  df-ss 3015

This theorem is referenced by:  fssdm  5190  fndmdif  5420  fneqeql2  5424  fconst4m  5533  f1opw2  5866  ecss  6349  fopwdom  6608  ssenen  6623  phplem2  6625  fiintim  6695  casefun  6832  caseinj  6836  djufun  6842  djuinj  6844  nn0supp  8788  monoord2  9968  binom1dif  10944