Theorem eqsstrrid 3986

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3931

This theorem is referenced by:  3sstr3g  3999  relcnvtrg  6239  fimacnvdisj  6738  dffv2  6956  f1ompt  7083  abnexg  7732  fnwelem  8110  tfrlem15  8360  omxpenlem  9042  hartogslem1  9495  ttrcltr  9669  dfttrcl2  9677  infxpidm2  9970  alephgeom  10035  infenaleph  10044  cfflb  10212  pwfseqlem5  10616  imasvscafn  17500  mrieqvlemd  17590  cnvps  18537  dirdm  18559  tsrdir  18563  frmdss2  18790  subdrgint  20712  iinopn  22789  neitr  23067  xkococnlem  23546  tgpconncomp  24000  trcfilu  24181  mbfconstlem  25528  itg2seq  25643  limcdif  25777  dvres2lem  25811  c1lip3  25904  lhop  25921  plyeq0  26116  dchrghm  27167  negsbdaylem  27962  precsexlem10  28118  uspgrupgrushgr  29106  upgrreslem  29231  umgrreslem  29232  umgrres1  29241  umgr2v2e  29453  chssoc  31425  tpssbd  32469  tpsscd  32470  gsumhashmul  33001  pmtrcnelor  33048  tocycfvres1  33067  tocycfvres2  33068  elrgspnsubrunlem2  33199  dimkerim  33623  hauseqcn  33888  carsgclctunlem3  34311  cvmliftmolem1  35268  cvmlift2lem9a  35290  cvmlift2lem9  35298  cnres2  37757  rngunsnply  43158  proot1hash  43184  omabs2  43321  clcnvlem  43612  cnvtrcl0  43615  trrelsuperrel2dg  43660  brtrclfv2  43716  imo72b2lem1  44158  fourierdlem92  46196  vsetrec  49692