Theorem eqsstrrid 3998

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-ss 3943

This theorem is referenced by:  3sstr3g  4011  relcnvtrg  6255  fimacnvdisj  6756  dffv2  6974  f1ompt  7101  abnexg  7750  fnwelem  8130  tfrlem15  8406  omxpenlem  9087  hartogslem1  9556  ttrcltr  9730  dfttrcl2  9738  infxpidm2  10031  alephgeom  10096  infenaleph  10105  cfflb  10273  pwfseqlem5  10677  imasvscafn  17551  mrieqvlemd  17641  cnvps  18588  dirdm  18610  tsrdir  18614  frmdss2  18841  subdrgint  20763  iinopn  22840  neitr  23118  xkococnlem  23597  tgpconncomp  24051  trcfilu  24232  mbfconstlem  25580  itg2seq  25695  limcdif  25829  dvres2lem  25863  c1lip3  25956  lhop  25973  plyeq0  26168  dchrghm  27219  negsbdaylem  28014  precsexlem10  28170  uspgrupgrushgr  29158  upgrreslem  29283  umgrreslem  29284  umgrres1  29293  umgr2v2e  29505  chssoc  31477  tpssbd  32521  tpsscd  32522  gsumhashmul  33055  pmtrcnelor  33102  tocycfvres1  33121  tocycfvres2  33122  elrgspnsubrunlem2  33243  dimkerim  33667  hauseqcn  33929  carsgclctunlem3  34352  cvmliftmolem1  35303  cvmlift2lem9a  35325  cvmlift2lem9  35333  cnres2  37787  rngunsnply  43193  proot1hash  43219  omabs2  43356  clcnvlem  43647  cnvtrcl0  43650  trrelsuperrel2dg  43695  brtrclfv2  43751  imo72b2lem1  44193  fourierdlem92  46227  vsetrec  49567