Theorem syl5eqss 3073

Description: B chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)

Hypotheses

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

Assertion

Ref	Expression
syl5eqss	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem syl5eqss

Step	Hyp	Ref	Expression
1		syl5eqss.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
2		syl5eqss.1	. . 3 ⊢ 𝐴 = 𝐵
3	2	sseq1i 3053	. 2 ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)
4	1, 3	sylibr 133	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:  syl5eqssr  3074  inss  3232  difsnss  3591  tpssi  3611  peano5  4428  xpsspw  4565  iotanul  5010  iotass  5012  fun  5198  fun11iun  5289  fvss  5334  fmpt  5465  fliftrel  5587  opabbrex  5709  1stcof  5950  2ndcof  5951  tfrlemibacc  6107  tfrlemibfn  6109  tfr1onlemssrecs  6120  tfr1onlembacc  6123  tfr1onlembfn  6125  tfrcllemssrecs  6133  tfrcllembacc  6136  tfrcllembfn  6138  caucvgprlemladdrl  7300  peano5nnnn  7490  peano5nni  8488  un0addcl  8769  un0mulcl  8770  strleund  11645  bj-omtrans  12155