Theorem eqsstrid 3274

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

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

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 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  eqsstrrid  3275  inss  3439  difsnss  3824  tpssi  3847  peano5  4702  opabssxpd  4768  xpsspw  4844  iotanul  5309  iotass  5311  fun  5516  fun11iun  5613  fvss  5662  fmpt  5805  fliftrel  5943  ovssunirng  6063  opabbrex  6075  1stcof  6335  2ndcof  6336  tfrlemibacc  6535  tfrlemibfn  6537  tfr1onlemssrecs  6548  tfr1onlembacc  6551  tfr1onlembfn  6553  tfrcllemssrecs  6561  tfrcllembacc  6564  tfrcllembfn  6566  caucvgprlemladdrl  7941  peano5nnnn  8155  peano5nni  9188  un0addcl  9477  un0mulcl  9478  4sqlemafi  13031  4sqlemffi  13032  4sqleminfi  13033  4sqlem11  13037  4sqlem19  13045  strleund  13249  mgmidsssn0  13530  lsptpcl  14473  cnptopco  15016  cnconst2  15027  xmetresbl  15234  blsscls2  15287  perfectlem2  15797  setsvtx  15975  1hegrvtxdg1rfi  16234  bj-omtrans  16655