Theorem eqsstrrid 3954

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

Syntax hints:   → wi 4   = wceq 1547   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-ss 3900

This theorem is referenced by:  3sstr3g  3967  relcnvtrg  6218  fimacnvdisj  6705  dffv2  6922  f1ompt  7052  abnexg  7699  fnwelem  8071  tfrlem15  8321  omxpenlem  9006  hartogslem1  9447  ttrcltr  9628  dfttrcl2  9636  infxpidm2  9930  alephgeom  9995  infenaleph  10004  cfflb  10172  pwfseqlem5  10577  imasvscafn  17492  mrieqvlemd  17586  cnvps  18535  dirdm  18557  tsrdir  18561  frmdss2  18822  subdrgint  20775  iinopn  22885  neitr  23163  xkococnlem  23642  tgpconncomp  24096  trcfilu  24276  mbfconstlem  25612  itg2seq  25727  limcdif  25861  dvres2lem  25895  c1lip3  25984  lhop  26001  plyeq0  26194  dchrghm  27237  negbdaylem  28066  precsexlem10  28226  bdaypw2n0bndlem  28473  uspgrupgrushgr  29266  upgrreslem  29391  umgrreslem  29392  umgrres1  29401  umgr2v2e  29612  chssoc  31585  tpssbd  32628  tpsscd  32629  gsumhashmul  33148  pmtrcnelor  33172  tocycfvres1  33191  tocycfvres2  33192  elrgspnsubrunlem2  33329  dimkerim  33811  hauseqcn  34082  carsgclctunlem3  34504  tz9.1regs  35315  cvmliftmolem1  35509  cvmlift2lem9a  35531  cvmlift2lem9  35539  ttcmin  36724  dfttc2g  36734  cnres2  38130  rngunsnply  43614  proot1hash  43640  omabs2  43777  clcnvlem  44067  cnvtrcl0  44070  trrelsuperrel2dg  44115  brtrclfv2  44171  imo72b2lem1  44613  fourierdlem92  46641  vsetrec  50193