Theorem eqsstrrid 3977

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

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

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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  3sstr3g  3990  relcnvtrg  6219  fimacnvdisj  6706  dffv2  6922  f1ompt  7049  abnexg  7696  fnwelem  8071  tfrlem15  8321  omxpenlem  9002  hartogslem1  9453  ttrcltr  9631  dfttrcl2  9639  infxpidm2  9930  alephgeom  9995  infenaleph  10004  cfflb  10172  pwfseqlem5  10576  imasvscafn  17460  mrieqvlemd  17554  cnvps  18503  dirdm  18525  tsrdir  18529  frmdss2  18756  subdrgint  20707  iinopn  22806  neitr  23084  xkococnlem  23563  tgpconncomp  24017  trcfilu  24198  mbfconstlem  25545  itg2seq  25660  limcdif  25794  dvres2lem  25828  c1lip3  25921  lhop  25938  plyeq0  26133  dchrghm  27184  negsbdaylem  27986  precsexlem10  28142  uspgrupgrushgr  29143  upgrreslem  29268  umgrreslem  29269  umgrres1  29278  umgr2v2e  29490  chssoc  31459  tpssbd  32503  tpsscd  32504  gsumhashmul  33033  pmtrcnelor  33052  tocycfvres1  33071  tocycfvres2  33072  elrgspnsubrunlem2  33207  dimkerim  33613  hauseqcn  33884  carsgclctunlem3  34307  tz9.1regs  35086  cvmliftmolem1  35273  cvmlift2lem9a  35295  cvmlift2lem9  35303  cnres2  37762  rngunsnply  43162  proot1hash  43188  omabs2  43325  clcnvlem  43616  cnvtrcl0  43619  trrelsuperrel2dg  43664  brtrclfv2  43720  imo72b2lem1  44162  fourierdlem92  46199  vsetrec  49708