Theorem eqsstrrid 3961

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

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

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 2708

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

This theorem is referenced by:  3sstr3g  3974  relcnvtrg  6231  fimacnvdisj  6718  dffv2  6935  f1ompt  7063  abnexg  7710  fnwelem  8081  tfrlem15  8331  omxpenlem  9016  hartogslem1  9457  ttrcltr  9637  dfttrcl2  9645  infxpidm2  9939  alephgeom  10004  infenaleph  10013  cfflb  10181  pwfseqlem5  10586  imasvscafn  17501  mrieqvlemd  17595  cnvps  18544  dirdm  18566  tsrdir  18570  frmdss2  18831  subdrgint  20780  iinopn  22867  neitr  23145  xkococnlem  23624  tgpconncomp  24078  trcfilu  24258  mbfconstlem  25594  itg2seq  25709  limcdif  25843  dvres2lem  25877  c1lip3  25966  lhop  25983  plyeq0  26176  dchrghm  27219  negbdaylem  28048  precsexlem10  28208  bdaypw2n0bndlem  28455  uspgrupgrushgr  29248  upgrreslem  29373  umgrreslem  29374  umgrres1  29383  umgr2v2e  29594  chssoc  31567  tpssbd  32610  tpsscd  32611  gsumhashmul  33128  pmtrcnelor  33152  tocycfvres1  33171  tocycfvres2  33172  elrgspnsubrunlem2  33309  dimkerim  33771  hauseqcn  34042  carsgclctunlem3  34464  tz9.1regs  35278  cvmliftmolem1  35463  cvmlift2lem9a  35485  cvmlift2lem9  35493  ttcmin  36678  dfttc2g  36688  cnres2  38084  rngunsnply  43597  proot1hash  43623  omabs2  43760  clcnvlem  44050  cnvtrcl0  44053  trrelsuperrel2dg  44098  brtrclfv2  44154  imo72b2lem1  44596  fourierdlem92  46626  vsetrec  50178