Theorem eqsstrrid 3969

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 2740	. 2 ⊢ 𝐴 = 𝐵
3		eqsstrrid.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
4	2, 3	eqsstrid 3968	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ss 3914

This theorem is referenced by:  3sstr3g  3982  relcnvtrg  6209  fimacnvdisj  6696  dffv2  6912  f1ompt  7039  abnexg  7684  fnwelem  8056  tfrlem15  8306  omxpenlem  8986  hartogslem1  9423  ttrcltr  9601  dfttrcl2  9609  infxpidm2  9903  alephgeom  9968  infenaleph  9977  cfflb  10145  pwfseqlem5  10549  imasvscafn  17436  mrieqvlemd  17530  cnvps  18479  dirdm  18501  tsrdir  18505  frmdss2  18766  subdrgint  20713  iinopn  22812  neitr  23090  xkococnlem  23569  tgpconncomp  24023  trcfilu  24203  mbfconstlem  25550  itg2seq  25665  limcdif  25799  dvres2lem  25833  c1lip3  25926  lhop  25943  plyeq0  26138  dchrghm  27189  negsbdaylem  27993  precsexlem10  28149  uspgrupgrushgr  29152  upgrreslem  29277  umgrreslem  29278  umgrres1  29287  umgr2v2e  29499  chssoc  31468  tpssbd  32512  tpsscd  32513  gsumhashmul  33033  pmtrcnelor  33052  tocycfvres1  33071  tocycfvres2  33072  elrgspnsubrunlem2  33207  dimkerim  33632  hauseqcn  33903  carsgclctunlem3  34325  tz9.1regs  35122  cvmliftmolem1  35317  cvmlift2lem9a  35339  cvmlift2lem9  35347  cnres2  37803  rngunsnply  43202  proot1hash  43228  omabs2  43365  clcnvlem  43656  cnvtrcl0  43659  trrelsuperrel2dg  43704  brtrclfv2  43760  imo72b2lem1  44202  fourierdlem92  46236  vsetrec  49735