Theorem eqsstrid 3238

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

Syntax hints:   → wi 4   = wceq 1372   ⊆ wss 3165

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-in 3171  df-ss 3178

This theorem is referenced by:  eqsstrrid  3239  inss  3402  difsnss  3778  tpssi  3799  peano5  4644  xpsspw  4785  iotanul  5244  iotass  5246  fun  5442  fun11iun  5537  fvss  5584  fmpt  5724  fliftrel  5851  ovssunirng  5969  opabbrex  5979  1stcof  6239  2ndcof  6240  tfrlemibacc  6402  tfrlemibfn  6404  tfr1onlemssrecs  6415  tfr1onlembacc  6418  tfr1onlembfn  6420  tfrcllemssrecs  6428  tfrcllembacc  6431  tfrcllembfn  6433  caucvgprlemladdrl  7773  peano5nnnn  7987  peano5nni  9021  un0addcl  9310  un0mulcl  9311  4sqlemafi  12637  4sqlemffi  12638  4sqleminfi  12639  4sqlem11  12643  4sqlem19  12651  strleund  12854  mgmidsssn0  13134  lsptpcl  14074  cnptopco  14612  cnconst2  14623  xmetresbl  14830  blsscls2  14883  perfectlem2  15390  bj-omtrans  15756