Theorem eqsstrrid 3950

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

Syntax hints:   → wi 4   = wceq 1543   ⊆ wss 3866

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-in 3873  df-ss 3883

This theorem is referenced by:  relcnvtrg  6130  fimacnvdisj  6597  dffv2  6806  fimacnvOLD  6891  f1ompt  6928  abnexg  7541  fnwelem  7898  tfrlem15  8128  omxpenlem  8746  hartogslem1  9158  infxpidm2  9631  alephgeom  9696  infenaleph  9705  cfflb  9873  pwfseqlem5  10277  imasvscafn  17042  mrieqvlemd  17132  cnvps  18084  dirdm  18106  tsrdir  18110  frmdss2  18290  subdrgint  19847  iinopn  21799  neitr  22077  xkococnlem  22556  tgpconncomp  23010  trcfilu  23191  mbfconstlem  24524  itg2seq  24640  limcdif  24773  dvres2lem  24807  c1lip3  24896  lhop  24913  plyeq0  25105  dchrghm  26137  uspgrupgrushgr  27268  upgrreslem  27392  umgrreslem  27393  umgrres1  27402  umgr2v2e  27613  chssoc  29577  gsumhashmul  31035  pmtrcnelor  31079  tocycfvres1  31096  tocycfvres2  31097  dimkerim  31422  hauseqcn  31562  carsgclctunlem3  31999  cvmliftmolem1  32956  cvmlift2lem9a  32978  cvmlift2lem9  32986  ttrcltr  33515  dfttrcl2  33523  cnres2  35658  rngunsnply  40701  proot1hash  40728  clcnvlem  40907  cnvtrcl0  40910  trrelsuperrel2dg  40956  brtrclfv2  41012  imo72b2lem1  41457  fourierdlem92  43414  vsetrec  46079