Theorem eqsstrrid 3968

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

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

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 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

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

This theorem is used by:  3sstr3g  3981  relcnvtrg  6269  relcnvtrgOLD  6270  fimacnvdisj  6761  dffv2  6981  f1ompt  7112  abnexg  7771  fnwelem  8144  tfrlem15  8401  omxpenlem  9098  hartogslem1  9537  ttrcltr  9718  dfttrcl2  9726  infxpidm2  10097  alephgeom  10162  infenaleph  10171  cfflb  10338  pwfseqlem5  10749  imasvscafn  17710  mrieqvlemd  17804  cnvps  18753  dirdm  18775  tsrdir  18779  frmdss2  19060  subdrgint  21061  iinopn  23221  neitr  23499  xkococnlem  23979  tgpconncomp  24433  trcfilu  24613  mbfconstlem  25949  itg2seq  26064  limcdif  26197  dvres2lem  26231  c1lip3  26320  lhop  26337  plyeq0  26531  dchrghm  27584  negbdaylem  28443  precsexlem10  28603  bdaypw2n0bndlem  28850  uspgrupgrushgr  29761  upgrreslem  29886  umgrreslem  29887  umgrres1  29896  umgr2v2e  30107  chssoc  32099  tpssbd  33137  tpsscd  33138  gsumhashmul  33629  pmtrcnelor  33653  tocycfvres1  33672  tocycfvres2  33673  elrgspnsubrunlem2  33810  dimkerim  34260  hauseqcn  34531  carsgclctunlem3  34953  tz9.1regs  35803  cvmliftmolem1  36047  cvmlift2lem9a  36069  cvmlift2lem9  36077  ttcmin  37285  dfttc2g  37295  cnres2  38699  rngunsnply  44172  proot1hash  44198  omabs2  44335  clcnvlem  44624  cnvtrcl0  44627  trrelsuperrel2dg  44672  brtrclfv2  44728  imo72b2lem1  45170  fourierdlem92  47209  vsetrec  50797