Theorem eqsstrrid 4031

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3948

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965

This theorem is referenced by:  relcnvtrg  6265  fimacnvdisj  6769  dffv2  6986  fimacnvOLD  7072  f1ompt  7112  abnexg  7745  fnwelem  8119  tfrlem15  8394  omxpenlem  9075  hartogslem1  9539  ttrcltr  9713  dfttrcl2  9721  infxpidm2  10014  alephgeom  10079  infenaleph  10088  cfflb  10256  pwfseqlem5  10660  imasvscafn  17485  mrieqvlemd  17575  cnvps  18533  dirdm  18555  tsrdir  18559  frmdss2  18746  subdrgint  20423  iinopn  22411  neitr  22691  xkococnlem  23170  tgpconncomp  23624  trcfilu  23806  mbfconstlem  25151  itg2seq  25267  limcdif  25400  dvres2lem  25434  c1lip3  25523  lhop  25540  plyeq0  25732  dchrghm  26766  negsbdaylem  27540  precsexlem10  27672  uspgrupgrushgr  28475  upgrreslem  28599  umgrreslem  28600  umgrres1  28609  umgr2v2e  28820  chssoc  30787  gsumhashmul  32249  pmtrcnelor  32293  tocycfvres1  32310  tocycfvres2  32311  dimkerim  32771  hauseqcn  32947  carsgclctunlem3  33388  cvmliftmolem1  34341  cvmlift2lem9a  34363  cvmlift2lem9  34371  cnres2  36717  rngunsnply  41997  proot1hash  42024  omabs2  42164  clcnvlem  42456  cnvtrcl0  42459  trrelsuperrel2dg  42504  brtrclfv2  42560  imo72b2lem1  43003  fourierdlem92  44993  vsetrec  47826