Theorem eqsstrrid 3975

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

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

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 2709

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

This theorem is referenced by:  3sstr3g  3988  relcnvtrg  6233  fimacnvdisj  6720  dffv2  6937  f1ompt  7065  abnexg  7711  fnwelem  8083  tfrlem15  8333  omxpenlem  9018  hartogslem1  9459  ttrcltr  9637  dfttrcl2  9645  infxpidm2  9939  alephgeom  10004  infenaleph  10013  cfflb  10181  pwfseqlem5  10586  imasvscafn  17470  mrieqvlemd  17564  cnvps  18513  dirdm  18535  tsrdir  18539  frmdss2  18800  subdrgint  20748  iinopn  22858  neitr  23136  xkococnlem  23615  tgpconncomp  24069  trcfilu  24249  mbfconstlem  25596  itg2seq  25711  limcdif  25845  dvres2lem  25879  c1lip3  25972  lhop  25989  plyeq0  26184  dchrghm  27235  negbdaylem  28064  precsexlem10  28224  bdaypw2n0bndlem  28471  uspgrupgrushgr  29264  upgrreslem  29389  umgrreslem  29390  umgrres1  29399  umgr2v2e  29611  chssoc  31583  tpssbd  32626  tpsscd  32627  gsumhashmul  33160  pmtrcnelor  33184  tocycfvres1  33203  tocycfvres2  33204  elrgspnsubrunlem2  33341  dimkerim  33804  hauseqcn  34075  carsgclctunlem3  34497  tz9.1regs  35309  cvmliftmolem1  35494  cvmlift2lem9a  35516  cvmlift2lem9  35524  cnres2  38011  rngunsnply  43523  proot1hash  43549  omabs2  43686  clcnvlem  43976  cnvtrcl0  43979  trrelsuperrel2dg  44024  brtrclfv2  44080  imo72b2lem1  44522  fourierdlem92  46553  vsetrec  50059