Theorem eqsstrrid 3970

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

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

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 2123  ax-ext 2705

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

This theorem is referenced by:  3sstr3g  3983  relcnvtrg  6222  fimacnvdisj  6709  dffv2  6926  f1ompt  7053  abnexg  7698  fnwelem  8070  tfrlem15  8320  omxpenlem  9002  hartogslem1  9439  ttrcltr  9617  dfttrcl2  9625  infxpidm2  9919  alephgeom  9984  infenaleph  9993  cfflb  10161  pwfseqlem5  10565  imasvscafn  17449  mrieqvlemd  17543  cnvps  18492  dirdm  18514  tsrdir  18518  frmdss2  18779  subdrgint  20727  iinopn  22837  neitr  23115  xkococnlem  23594  tgpconncomp  24048  trcfilu  24228  mbfconstlem  25575  itg2seq  25690  limcdif  25824  dvres2lem  25858  c1lip3  25951  lhop  25968  plyeq0  26163  dchrghm  27214  negsbdaylem  28018  precsexlem10  28174  uspgrupgrushgr  29178  upgrreslem  29303  umgrreslem  29304  umgrres1  29313  umgr2v2e  29525  chssoc  31497  tpssbd  32541  tpsscd  32542  gsumhashmul  33078  pmtrcnelor  33101  tocycfvres1  33120  tocycfvres2  33121  elrgspnsubrunlem2  33258  dimkerim  33712  hauseqcn  33983  carsgclctunlem3  34405  tz9.1regs  35202  cvmliftmolem1  35397  cvmlift2lem9a  35419  cvmlift2lem9  35427  cnres2  37876  rngunsnply  43326  proot1hash  43352  omabs2  43489  clcnvlem  43780  cnvtrcl0  43783  trrelsuperrel2dg  43828  brtrclfv2  43884  imo72b2lem1  44326  fourierdlem92  46358  vsetrec  49864