Theorem eqsstrrid 3962

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

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

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 3907

This theorem is referenced by:  3sstr3g  3975  relcnvtrg  6225  fimacnvdisj  6712  dffv2  6929  f1ompt  7057  abnexg  7703  fnwelem  8074  tfrlem15  8324  omxpenlem  9009  hartogslem1  9450  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  20771  iinopn  22877  neitr  23155  xkococnlem  23634  tgpconncomp  24088  trcfilu  24268  mbfconstlem  25604  itg2seq  25719  limcdif  25853  dvres2lem  25887  c1lip3  25976  lhop  25993  plyeq0  26186  dchrghm  27233  negbdaylem  28062  precsexlem10  28222  bdaypw2n0bndlem  28469  uspgrupgrushgr  29262  upgrreslem  29387  umgrreslem  29388  umgrres1  29397  umgr2v2e  29609  chssoc  31582  tpssbd  32625  tpsscd  32626  gsumhashmul  33143  pmtrcnelor  33167  tocycfvres1  33186  tocycfvres2  33187  elrgspnsubrunlem2  33324  dimkerim  33787  hauseqcn  34058  carsgclctunlem3  34480  tz9.1regs  35294  cvmliftmolem1  35479  cvmlift2lem9a  35501  cvmlift2lem9  35509  ttcmin  36694  dfttc2g  36704  cnres2  38098  rngunsnply  43615  proot1hash  43641  omabs2  43778  clcnvlem  44068  cnvtrcl0  44071  trrelsuperrel2dg  44116  brtrclfv2  44172  imo72b2lem1  44614  fourierdlem92  46644  vsetrec  50190