Theorem eqsstrrid 3977

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

Syntax hints:   → wi 4   = wceq 1570   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3923

This theorem is referenced by:  3sstr3g  3990  relcnvtrg  6270  fimacnvdisj  6758  dffv2  6978  f1ompt  7108  abnexg  7756  fnwelem  8128  tfrlem15  8380  omxpenlem  9067  hartogslem1  9505  ttrcltr  9686  dfttrcl2  9694  infxpidm2  10002  alephgeom  10067  infenaleph  10076  cfflb  10244  pwfseqlem5  10649  imasvscafn  17592  mrieqvlemd  17686  cnvps  18635  dirdm  18657  tsrdir  18661  frmdss2  18923  subdrgint  20887  iinopn  23040  neitr  23318  xkococnlem  23797  tgpconncomp  24251  trcfilu  24431  mbfconstlem  25767  itg2seq  25882  limcdif  26016  dvres2lem  26050  c1lip3  26139  lhop  26156  plyeq0  26349  dchrghm  27401  negbdaylem  28230  precsexlem10  28390  bdaypw2n0bndlem  28637  uspgrupgrushgr  29510  upgrreslem  29635  umgrreslem  29636  umgrres1  29645  umgr2v2e  29856  chssoc  31829  tpssbd  32867  tpsscd  32868  gsumhashmul  33368  pmtrcnelor  33392  tocycfvres1  33411  tocycfvres2  33412  elrgspnsubrunlem2  33549  dimkerim  33998  hauseqcn  34269  carsgclctunlem3  34691  tz9.1regs  35528  cvmliftmolem1  35754  cvmlift2lem9a  35776  cvmlift2lem9  35784  ttcmin  36988  dfttc2g  36998  cnres2  38395  rngunsnply  43879  proot1hash  43905  omabs2  44042  clcnvlem  44332  cnvtrcl0  44335  trrelsuperrel2dg  44380  brtrclfv2  44436  imo72b2lem1  44878  fourierdlem92  46895  vsetrec  50464