Theorem eqsstrrid 3975

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3920

This theorem is referenced by:  3sstr3g  3988  relcnvtrg  6235  fimacnvdisj  6722  dffv2  6939  f1ompt  7067  abnexg  7713  fnwelem  8085  tfrlem15  8335  omxpenlem  9020  hartogslem1  9461  ttrcltr  9639  dfttrcl2  9647  infxpidm2  9941  alephgeom  10006  infenaleph  10015  cfflb  10183  pwfseqlem5  10588  imasvscafn  17472  mrieqvlemd  17566  cnvps  18515  dirdm  18537  tsrdir  18541  frmdss2  18802  subdrgint  20753  iinopn  22863  neitr  23141  xkococnlem  23620  tgpconncomp  24074  trcfilu  24254  mbfconstlem  25601  itg2seq  25716  limcdif  25850  dvres2lem  25884  c1lip3  25977  lhop  25994  plyeq0  26189  dchrghm  27240  negbdaylem  28069  precsexlem10  28229  bdaypw2n0bndlem  28476  uspgrupgrushgr  29270  upgrreslem  29395  umgrreslem  29396  umgrres1  29405  umgr2v2e  29617  chssoc  31590  tpssbd  32633  tpsscd  32634  gsumhashmul  33167  pmtrcnelor  33191  tocycfvres1  33210  tocycfvres2  33211  elrgspnsubrunlem2  33348  dimkerim  33811  hauseqcn  34082  carsgclctunlem3  34504  tz9.1regs  35318  cvmliftmolem1  35503  cvmlift2lem9a  35525  cvmlift2lem9  35533  cnres2  38043  rngunsnply  43555  proot1hash  43581  omabs2  43718  clcnvlem  44008  cnvtrcl0  44011  trrelsuperrel2dg  44056  brtrclfv2  44112  imo72b2lem1  44554  fourierdlem92  46585  vsetrec  50091