Theorem eqsstrid 3243

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

Hypotheses

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

Assertion

Ref	Expression
eqsstrid	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem eqsstrid

Step	Hyp	Ref	Expression
1		eqsstrid.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
2		eqsstrid.1	. . 3 ⊢ 𝐴 = 𝐵
3	2	sseq1i 3223	. 2 ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)
4	1, 3	sylibr 134	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1373   ⊆ wss 3170

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-in 3176  df-ss 3183

This theorem is referenced by:  eqsstrrid  3244  inss  3407  difsnss  3785  tpssi  3806  peano5  4654  xpsspw  4795  iotanul  5256  iotass  5258  fun  5459  fun11iun  5555  fvss  5603  fmpt  5743  fliftrel  5874  ovssunirng  5992  opabbrex  6002  1stcof  6262  2ndcof  6263  tfrlemibacc  6425  tfrlemibfn  6427  tfr1onlemssrecs  6438  tfr1onlembacc  6441  tfr1onlembfn  6443  tfrcllemssrecs  6451  tfrcllembacc  6454  tfrcllembfn  6456  caucvgprlemladdrl  7811  peano5nnnn  8025  peano5nni  9059  un0addcl  9348  un0mulcl  9349  4sqlemafi  12793  4sqlemffi  12794  4sqleminfi  12795  4sqlem11  12799  4sqlem19  12807  strleund  13010  mgmidsssn0  13291  lsptpcl  14231  cnptopco  14769  cnconst2  14780  xmetresbl  14987  blsscls2  15040  perfectlem2  15547  bj-omtrans  16030