Theorem eqsstrrid 3947

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3896

This theorem is used by:  3sstr3g  3960  relcnvtrg  6268  relcnvtrgOLD  6269  fimacnvdisj  6761  dffv2  6981  f1ompt  7112  abnexg  7771  fnwelem  8146  tfrlem15  8404  omxpenlem  9101  hartogslem1  9540  ttrcltr  9721  dfttrcl2  9729  infxpidm2  10100  alephgeom  10165  infenaleph  10174  cfflb  10341  pwfseqlem5  10752  imasvscafn  17715  mrieqvlemd  17809  cnvps  18758  dirdm  18780  tsrdir  18784  frmdss2  19065  subdrgint  21066  iinopn  23226  neitr  23504  xkococnlem  23984  tgpconncomp  24438  trcfilu  24618  mbfconstlem  25954  itg2seq  26069  limcdif  26202  dvres2lem  26236  c1lip3  26325  lhop  26342  plyeq0  26536  dchrghm  27589  negbdaylem  28448  precsexlem10  28608  bdaypw2n0bndlem  28855  uspgrupgrushgr  29766  upgrreslem  29891  umgrreslem  29892  umgrres1  29901  umgr2v2e  30112  chssoc  32104  tpssbd  33184  tpsscd  33185  gsumhashmul  33675  pmtrcnelor  33699  tocycfvres1  33718  tocycfvres2  33719  elrgspnsubrunlem2  33856  dimkerim  34306  hauseqcn  34577  carsgclctunlem3  34999  tz9.1regs  35859  cvmliftmolem1  36133  cvmlift2lem9a  36155  cvmlift2lem9  36163  ttcmin  37377  dfttc2g  37387  cnres2  38791  rngunsnply  44265  proot1hash  44291  omabs2  44428  clcnvlem  44717  cnvtrcl0  44720  trrelsuperrel2dg  44765  brtrclfv2  44821  imo72b2lem1  45263  fourierdlem92  47302  vsetrec  50965