Theorem eqsstrrid 4016

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

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3936

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952

This theorem is referenced by:  relcnvtrg  6119  fimacnvdisj  6557  dffv2  6756  fimacnv  6839  f1ompt  6875  abnexg  7478  fnwelem  7825  tfrlem15  8028  omxpenlem  8618  hartogslem1  9006  infxpidm2  9443  alephgeom  9508  infenaleph  9517  cfflb  9681  pwfseqlem5  10085  imasvscafn  16810  mrieqvlemd  16900  cnvps  17822  dirdm  17844  tsrdir  17848  frmdss2  18028  subdrgint  19582  iinopn  21510  neitr  21788  xkococnlem  22267  tgpconncomp  22721  trcfilu  22903  mbfconstlem  24228  itg2seq  24343  limcdif  24474  dvres2lem  24508  c1lip3  24596  lhop  24613  plyeq0  24801  dchrghm  25832  uspgrupgrushgr  26962  upgrreslem  27086  umgrreslem  27087  umgrres1  27096  umgr2v2e  27307  chssoc  29273  pmtrcnelor  30735  tocycfvres1  30752  tocycfvres2  30753  dimkerim  31023  hauseqcn  31138  carsgclctunlem3  31578  cvmliftmolem1  32528  cvmlift2lem9a  32550  cvmlift2lem9  32558  cnres2  35056  rngunsnply  39822  proot1hash  39849  clcnvlem  40032  cnvtrcl0  40035  trrelsuperrel2dg  40065  brtrclfv2  40121  imo72b2lem1  40570  fourierdlem92  42532  vsetrec  44854