Theorem eqsstrid 3271

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

Syntax hints:   → wi 4   = wceq 1395   ⊆ wss 3198

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3204  df-ss 3211

This theorem is referenced by:  eqsstrrid  3272  inss  3435  difsnss  3817  tpssi  3840  peano5  4694  opabssxpd  4760  xpsspw  4836  iotanul  5300  iotass  5302  fun  5505  fun11iun  5601  fvss  5649  fmpt  5793  fliftrel  5928  ovssunirng  6048  opabbrex  6060  1stcof  6321  2ndcof  6322  tfrlemibacc  6487  tfrlemibfn  6489  tfr1onlemssrecs  6500  tfr1onlembacc  6503  tfr1onlembfn  6505  tfrcllemssrecs  6513  tfrcllembacc  6516  tfrcllembfn  6518  caucvgprlemladdrl  7888  peano5nnnn  8102  peano5nni  9136  un0addcl  9425  un0mulcl  9426  4sqlemafi  12958  4sqlemffi  12959  4sqleminfi  12960  4sqlem11  12964  4sqlem19  12972  strleund  13176  mgmidsssn0  13457  lsptpcl  14398  cnptopco  14936  cnconst2  14947  xmetresbl  15154  blsscls2  15207  perfectlem2  15714  setsvtx  15892  bj-omtrans  16487