Theorem eqsstrrid 3952

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3900

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ss 3901

This theorem is used by:  3sstr3g  3965  relcnvtrg  6292  relcnvtrgOLD  6293  fimacnvdisj  6790  dffv2  7011  f1ompt  7143  abnexg  7802  fnwelem  8180  tfrlem15  8438  omxpenlem  9135  hartogslem1  9573  ttrcltr  9754  dfttrcl2  9762  infxpidm2  10135  alephgeom  10200  infenaleph  10209  cfflb  10376  pwfseqlem5  10787  imasvscafn  17759  mrieqvlemd  17853  cnvps  18802  dirdm  18824  tsrdir  18828  frmdss2  19109  subdrgint  21111  iinopn  23275  neitr  23553  xkococnlem  24033  tgpconncomp  24487  trcfilu  24667  mbfconstlem  26003  itg2seq  26118  limcdif  26251  dvres2lem  26285  c1lip3  26374  lhop  26391  plyeq0  26585  rngunsnply  26693  dchrghm  27640  negbdaylem  28499  precsexlem10  28659  bdaypw2n0bndlem  28906  uspgrupgrushgr  29817  upgrreslem  29942  umgrreslem  29943  umgrres1  29952  umgr2v2e  30163  chssoc  32155  tpssbd  33234  tpsscd  33235  gsumhashmul  33727  pmtrcnelor  33751  tocycfvres1  33770  tocycfvres2  33771  elrgspnsubrunlem2  33908  edompidlem  33960  dimkerim  34370  hauseqcn  34641  carsgclctunlem3  35063  tz9.1regs  35943  cvmliftmolem1  36254  cvmlift2lem9a  36276  cvmlift2lem9  36284  ttcmin  37499  dfttc2g  37509  coindi  38219  cossidres1  38220  cossidres2  38221  cossidcnvss2  38222  cossidcnvss  38223  nvo3  38230  cnres2  38963  proot1hash  44458  omabs2  44595  clcnvlem  44884  cnvtrcl0  44887  trrelsuperrel2dg  44932  brtrclfv2  44988  imo72b2lem1  45430  fourierdlem92  47481  vsetrec  51202