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 2770	. 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 2733

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

This theorem is used by:  3sstr3g  3983  relcnvtrg  6267  relcnvtrgOLD  6268  fimacnvdisj  6758  dffv2  6978  f1ompt  7109  abnexg  7768  fnwelem  8141  tfrlem15  8393  omxpenlem  9090  hartogslem1  9529  ttrcltr  9710  dfttrcl2  9718  infxpidm2  10089  alephgeom  10154  infenaleph  10163  cfflb  10330  pwfseqlem5  10741  imasvscafn  17702  mrieqvlemd  17796  cnvps  18745  dirdm  18767  tsrdir  18771  frmdss2  19052  subdrgint  21053  iinopn  23213  neitr  23491  xkococnlem  23971  tgpconncomp  24425  trcfilu  24605  mbfconstlem  25941  itg2seq  26056  limcdif  26189  dvres2lem  26223  c1lip3  26312  lhop  26329  plyeq0  26523  dchrghm  27576  negbdaylem  28435  precsexlem10  28595  bdaypw2n0bndlem  28842  uspgrupgrushgr  29753  upgrreslem  29878  umgrreslem  29879  umgrres1  29888  umgr2v2e  30099  chssoc  32091  tpssbd  33129  tpsscd  33130  gsumhashmul  33621  pmtrcnelor  33645  tocycfvres1  33664  tocycfvres2  33665  elrgspnsubrunlem2  33802  dimkerim  34252  hauseqcn  34523  carsgclctunlem3  34945  tz9.1regs  35785  cvmliftmolem1  36025  cvmlift2lem9a  36047  cvmlift2lem9  36055  ttcmin  37264  dfttc2g  37274  cnres2  38677  rngunsnply  44155  proot1hash  44181  omabs2  44318  clcnvlem  44608  cnvtrcl0  44611  trrelsuperrel2dg  44656  brtrclfv2  44712  imo72b2lem1  45154  fourierdlem92  47177  vsetrec  50765