Theorem eqsstrid 3270

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

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

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 3203  df-ss 3210

This theorem is referenced by:  eqsstrrid  3271  inss  3434  difsnss  3813  tpssi  3836  peano5  4689  xpsspw  4830  iotanul  5293  iotass  5295  fun  5496  fun11iun  5592  fvss  5640  fmpt  5784  fliftrel  5915  ovssunirng  6035  opabbrex  6047  1stcof  6307  2ndcof  6308  tfrlemibacc  6470  tfrlemibfn  6472  tfr1onlemssrecs  6483  tfr1onlembacc  6486  tfr1onlembfn  6488  tfrcllemssrecs  6496  tfrcllembacc  6499  tfrcllembfn  6501  caucvgprlemladdrl  7861  peano5nnnn  8075  peano5nni  9109  un0addcl  9398  un0mulcl  9399  4sqlemafi  12913  4sqlemffi  12914  4sqleminfi  12915  4sqlem11  12919  4sqlem19  12927  strleund  13131  mgmidsssn0  13412  lsptpcl  14352  cnptopco  14890  cnconst2  14901  xmetresbl  15108  blsscls2  15161  perfectlem2  15668  setsvtx  15846  bj-omtrans  16277