Theorem eqsstrrid 3966

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

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  relcnvtrg  6159  fimacnvdisj  6636  dffv2  6845  fimacnvOLD  6930  f1ompt  6967  abnexg  7584  fnwelem  7943  tfrlem15  8194  omxpenlem  8813  hartogslem1  9231  infxpidm2  9704  alephgeom  9769  infenaleph  9778  cfflb  9946  pwfseqlem5  10350  imasvscafn  17165  mrieqvlemd  17255  cnvps  18211  dirdm  18233  tsrdir  18237  frmdss2  18417  subdrgint  19986  iinopn  21959  neitr  22239  xkococnlem  22718  tgpconncomp  23172  trcfilu  23354  mbfconstlem  24696  itg2seq  24812  limcdif  24945  dvres2lem  24979  c1lip3  25068  lhop  25085  plyeq0  25277  dchrghm  26309  uspgrupgrushgr  27450  upgrreslem  27574  umgrreslem  27575  umgrres1  27584  umgr2v2e  27795  chssoc  29759  gsumhashmul  31218  pmtrcnelor  31262  tocycfvres1  31279  tocycfvres2  31280  dimkerim  31610  hauseqcn  31750  carsgclctunlem3  32187  cvmliftmolem1  33143  cvmlift2lem9a  33165  cvmlift2lem9  33173  ttrcltr  33702  dfttrcl2  33710  cnres2  35848  rngunsnply  40914  proot1hash  40941  clcnvlem  41120  cnvtrcl0  41123  trrelsuperrel2dg  41168  brtrclfv2  41224  imo72b2lem1  41669  fourierdlem92  43629  vsetrec  46294