Theorem eqsstrrid 3973

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 3972	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1559   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ss 3919

This theorem is referenced by:  3sstr3g  3986  relcnvtrg  6249  fimacnvdisj  6737  dffv2  6957  f1ompt  7087  abnexg  7734  fnwelem  8105  tfrlem15  8357  omxpenlem  9044  hartogslem1  9484  ttrcltr  9665  dfttrcl2  9673  infxpidm2  9967  alephgeom  10032  infenaleph  10041  cfflb  10210  pwfseqlem5  10615  imasvscafn  17558  mrieqvlemd  17652  cnvps  18601  dirdm  18623  tsrdir  18627  frmdss2  18888  subdrgint  20840  iinopn  22950  neitr  23228  xkococnlem  23707  tgpconncomp  24161  trcfilu  24341  mbfconstlem  25677  itg2seq  25792  limcdif  25926  dvres2lem  25960  c1lip3  26049  lhop  26066  plyeq0  26259  dchrghm  27308  negbdaylem  28137  precsexlem10  28297  bdaypw2n0bndlem  28544  uspgrupgrushgr  29337  upgrreslem  29462  umgrreslem  29463  umgrres1  29472  umgr2v2e  29683  chssoc  31656  tpssbd  32699  tpsscd  32700  gsumhashmul  33208  pmtrcnelor  33232  tocycfvres1  33251  tocycfvres2  33252  elrgspnsubrunlem2  33390  dimkerim  33885  hauseqcn  34156  carsgclctunlem3  34578  tz9.1regs  35391  cvmliftmolem1  35592  cvmlift2lem9a  35614  cvmlift2lem9  35622  ttcmin  36817  dfttc2g  36827  cnres2  38223  rngunsnply  43707  proot1hash  43733  omabs2  43870  clcnvlem  44160  cnvtrcl0  44163  trrelsuperrel2dg  44208  brtrclfv2  44264  imo72b2lem1  44706  fourierdlem92  46733  vsetrec  50285