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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-ss 3916

This theorem is used by:  3sstr3g  3983  relcnvtrg  6263  relcnvtrgOLD  6264  fimacnvdisj  6753  dffv2  6973  f1ompt  7104  abnexg  7755  fnwelem  8129  tfrlem15  8381  omxpenlem  9076  hartogslem1  9514  ttrcltr  9695  dfttrcl2  9703  infxpidm2  10020  alephgeom  10085  infenaleph  10094  cfflb  10261  pwfseqlem5  10672  imasvscafn  17623  mrieqvlemd  17717  cnvps  18666  dirdm  18688  tsrdir  18692  frmdss2  18972  subdrgint  20969  iinopn  23127  neitr  23405  xkococnlem  23885  tgpconncomp  24339  trcfilu  24519  mbfconstlem  25855  itg2seq  25970  limcdif  26103  dvres2lem  26137  c1lip3  26226  lhop  26243  plyeq0  26437  dchrghm  27492  negbdaylem  28321  precsexlem10  28481  bdaypw2n0bndlem  28728  uspgrupgrushgr  29639  upgrreslem  29764  umgrreslem  29765  umgrres1  29774  umgr2v2e  29985  chssoc  31977  tpssbd  33015  tpsscd  33016  gsumhashmul  33507  pmtrcnelor  33531  tocycfvres1  33550  tocycfvres2  33551  elrgspnsubrunlem2  33688  dimkerim  34137  hauseqcn  34408  carsgclctunlem3  34831  tz9.1regs  35660  cvmliftmolem1  35860  cvmlift2lem9a  35882  cvmlift2lem9  35890  ttcmin  37115  dfttc2g  37125  cnres2  38513  rngunsnply  44010  proot1hash  44036  omabs2  44173  clcnvlem  44463  cnvtrcl0  44466  trrelsuperrel2dg  44511  brtrclfv2  44567  imo72b2lem1  45009  fourierdlem92  47026  vsetrec  50629