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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

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

This theorem is referenced by:  3sstr3g  3986  relcnvtrg  6225  fimacnvdisj  6712  dffv2  6929  f1ompt  7056  abnexg  7701  fnwelem  8073  tfrlem15  8323  omxpenlem  9006  hartogslem1  9447  ttrcltr  9625  dfttrcl2  9633  infxpidm2  9927  alephgeom  9992  infenaleph  10001  cfflb  10169  pwfseqlem5  10574  imasvscafn  17458  mrieqvlemd  17552  cnvps  18501  dirdm  18523  tsrdir  18527  frmdss2  18788  subdrgint  20736  iinopn  22846  neitr  23124  xkococnlem  23603  tgpconncomp  24057  trcfilu  24237  mbfconstlem  25584  itg2seq  25699  limcdif  25833  dvres2lem  25867  c1lip3  25960  lhop  25977  plyeq0  26172  dchrghm  27223  negbdaylem  28052  precsexlem10  28212  bdaypw2n0bndlem  28459  uspgrupgrushgr  29252  upgrreslem  29377  umgrreslem  29378  umgrres1  29387  umgr2v2e  29599  chssoc  31571  tpssbd  32615  tpsscd  32616  gsumhashmul  33150  pmtrcnelor  33173  tocycfvres1  33192  tocycfvres2  33193  elrgspnsubrunlem2  33330  dimkerim  33784  hauseqcn  34055  carsgclctunlem3  34477  tz9.1regs  35290  cvmliftmolem1  35475  cvmlift2lem9a  35497  cvmlift2lem9  35505  cnres2  37964  rngunsnply  43411  proot1hash  43437  omabs2  43574  clcnvlem  43864  cnvtrcl0  43867  trrelsuperrel2dg  43912  brtrclfv2  43968  imo72b2lem1  44410  fourierdlem92  46442  vsetrec  49948