Theorem eqsstrrid 3977

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

Hypotheses

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

Assertion

Ref	Expression
eqsstrrid	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem eqsstrrid

Step	Hyp	Ref	Expression
1		eqsstrrid.1	. . 3 ⊢ 𝐵 = 𝐴
2	1	eqcomi 2774	. 2 ⊢ 𝐴 = 𝐵
3		eqsstrrid.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
4	2, 3	eqsstrid 3976	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-ss 3923

This theorem is used by:  3sstr3g  3990  relcnvtrg  6270  relcnvtrgOLD  6271  fimacnvdisj  6760  dffv2  6980  f1ompt  7110  abnexg  7757  fnwelem  8129  tfrlem15  8381  omxpenlem  9069  hartogslem1  9507  ttrcltr  9688  dfttrcl2  9696  infxpidm2  10013  alephgeom  10078  infenaleph  10087  cfflb  10254  pwfseqlem5  10659  imasvscafn  17609  mrieqvlemd  17703  cnvps  18652  dirdm  18674  tsrdir  18678  frmdss2  18946  subdrgint  20936  iinopn  23089  neitr  23367  xkococnlem  23847  tgpconncomp  24301  trcfilu  24481  mbfconstlem  25817  itg2seq  25932  limcdif  26066  dvres2lem  26100  c1lip3  26189  lhop  26206  plyeq0  26399  dchrghm  27451  negbdaylem  28280  precsexlem10  28440  bdaypw2n0bndlem  28687  uspgrupgrushgr  29563  upgrreslem  29688  umgrreslem  29689  umgrres1  29698  umgr2v2e  29909  chssoc  31895  tpssbd  32933  tpsscd  32934  gsumhashmul  33427  pmtrcnelor  33451  tocycfvres1  33470  tocycfvres2  33471  elrgspnsubrunlem2  33608  dimkerim  34057  hauseqcn  34328  carsgclctunlem3  34751  tz9.1regs  35580  cvmliftmolem1  35786  cvmlift2lem9a  35808  cvmlift2lem9  35816  ttcmin  37040  dfttc2g  37050  cnres2  38447  rngunsnply  43929  proot1hash  43955  omabs2  44092  clcnvlem  44382  cnvtrcl0  44385  trrelsuperrel2dg  44430  brtrclfv2  44486  imo72b2lem1  44928  fourierdlem92  46945  vsetrec  50514