Theorem eqsstrrid 3983

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

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

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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  3sstr3g  3996  relcnvtrg  6227  fimacnvdisj  6720  dffv2  6938  f1ompt  7065  abnexg  7712  fnwelem  8087  tfrlem15  8337  omxpenlem  9019  hartogslem1  9471  ttrcltr  9645  dfttrcl2  9653  infxpidm2  9946  alephgeom  10011  infenaleph  10020  cfflb  10188  pwfseqlem5  10592  imasvscafn  17476  mrieqvlemd  17566  cnvps  18513  dirdm  18535  tsrdir  18539  frmdss2  18766  subdrgint  20688  iinopn  22765  neitr  23043  xkococnlem  23522  tgpconncomp  23976  trcfilu  24157  mbfconstlem  25504  itg2seq  25619  limcdif  25753  dvres2lem  25787  c1lip3  25880  lhop  25897  plyeq0  26092  dchrghm  27143  negsbdaylem  27938  precsexlem10  28094  uspgrupgrushgr  29082  upgrreslem  29207  umgrreslem  29208  umgrres1  29217  umgr2v2e  29429  chssoc  31398  tpssbd  32442  tpsscd  32443  gsumhashmul  32974  pmtrcnelor  33021  tocycfvres1  33040  tocycfvres2  33041  elrgspnsubrunlem2  33172  dimkerim  33596  hauseqcn  33861  carsgclctunlem3  34284  cvmliftmolem1  35241  cvmlift2lem9a  35263  cvmlift2lem9  35271  cnres2  37730  rngunsnply  43131  proot1hash  43157  omabs2  43294  clcnvlem  43585  cnvtrcl0  43588  trrelsuperrel2dg  43633  brtrclfv2  43689  imo72b2lem1  44131  fourierdlem92  46169  vsetrec  49665