Theorem eqsstrrid 4023

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  3sstr3g  4036  relcnvtrg  6286  fimacnvdisj  6786  dffv2  7004  f1ompt  7131  abnexg  7776  fnwelem  8156  tfrlem15  8432  omxpenlem  9113  hartogslem1  9582  ttrcltr  9756  dfttrcl2  9764  infxpidm2  10057  alephgeom  10122  infenaleph  10131  cfflb  10299  pwfseqlem5  10703  imasvscafn  17582  mrieqvlemd  17672  cnvps  18623  dirdm  18645  tsrdir  18649  frmdss2  18876  subdrgint  20804  iinopn  22908  neitr  23188  xkococnlem  23667  tgpconncomp  24121  trcfilu  24303  mbfconstlem  25662  itg2seq  25777  limcdif  25911  dvres2lem  25945  c1lip3  26038  lhop  26055  plyeq0  26250  dchrghm  27300  negsbdaylem  28088  precsexlem10  28240  uspgrupgrushgr  29196  upgrreslem  29321  umgrreslem  29322  umgrres1  29331  umgr2v2e  29543  chssoc  31515  gsumhashmul  33064  pmtrcnelor  33111  tocycfvres1  33130  tocycfvres2  33131  elrgspnsubrunlem2  33252  dimkerim  33678  hauseqcn  33897  carsgclctunlem3  34322  cvmliftmolem1  35286  cvmlift2lem9a  35308  cvmlift2lem9  35316  cnres2  37770  rngunsnply  43181  proot1hash  43207  omabs2  43345  clcnvlem  43636  cnvtrcl0  43639  trrelsuperrel2dg  43684  brtrclfv2  43740  imo72b2lem1  44182  fourierdlem92  46213  vsetrec  49222