Theorem eqsstrrid 3984

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

Syntax hints:   → wi 4   = wceq 1567   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ss 3930

This theorem is referenced by:  3sstr3g  3997  relcnvtrg  6265  fimacnvdisj  6754  dffv2  6974  f1ompt  7104  abnexg  7751  fnwelem  8123  tfrlem15  8375  omxpenlem  9062  hartogslem1  9500  ttrcltr  9681  dfttrcl2  9689  infxpidm2  9997  alephgeom  10062  infenaleph  10071  cfflb  10239  pwfseqlem5  10644  imasvscafn  17587  mrieqvlemd  17681  cnvps  18630  dirdm  18652  tsrdir  18656  frmdss2  18918  subdrgint  20880  iinopn  23024  neitr  23302  xkococnlem  23781  tgpconncomp  24235  trcfilu  24415  mbfconstlem  25751  itg2seq  25866  limcdif  26000  dvres2lem  26034  c1lip3  26123  lhop  26140  plyeq0  26333  dchrghm  27382  negbdaylem  28211  precsexlem10  28371  bdaypw2n0bndlem  28618  uspgrupgrushgr  29466  upgrreslem  29591  umgrreslem  29592  umgrres1  29601  umgr2v2e  29812  chssoc  31785  tpssbd  32823  tpsscd  32824  gsumhashmul  33324  pmtrcnelor  33348  tocycfvres1  33367  tocycfvres2  33368  elrgspnsubrunlem2  33505  dimkerim  33958  hauseqcn  34229  carsgclctunlem3  34651  tz9.1regs  35466  cvmliftmolem1  35668  cvmlift2lem9a  35690  cvmlift2lem9  35698  ttcmin  36892  dfttc2g  36902  cnres2  38297  rngunsnply  43781  proot1hash  43807  omabs2  43944  clcnvlem  44234  cnvtrcl0  44237  trrelsuperrel2dg  44282  brtrclfv2  44338  imo72b2lem1  44780  fourierdlem92  46797  vsetrec  50359