Theorem eqsstrrid 4058

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

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993

This theorem is referenced by:  relcnvtrg  6297  fimacnvdisj  6799  dffv2  7017  fimacnvOLD  7104  f1ompt  7145  abnexg  7791  fnwelem  8172  tfrlem15  8448  omxpenlem  9139  hartogslem1  9611  ttrcltr  9785  dfttrcl2  9793  infxpidm2  10086  alephgeom  10151  infenaleph  10160  cfflb  10328  pwfseqlem5  10732  imasvscafn  17597  mrieqvlemd  17687  cnvps  18648  dirdm  18670  tsrdir  18674  frmdss2  18898  subdrgint  20826  iinopn  22929  neitr  23209  xkococnlem  23688  tgpconncomp  24142  trcfilu  24324  mbfconstlem  25681  itg2seq  25797  limcdif  25931  dvres2lem  25965  c1lip3  26058  lhop  26075  plyeq0  26270  dchrghm  27318  negsbdaylem  28106  precsexlem10  28258  uspgrupgrushgr  29214  upgrreslem  29339  umgrreslem  29340  umgrres1  29349  umgr2v2e  29561  chssoc  31528  gsumhashmul  33040  pmtrcnelor  33084  tocycfvres1  33103  tocycfvres2  33104  dimkerim  33640  hauseqcn  33844  carsgclctunlem3  34285  cvmliftmolem1  35249  cvmlift2lem9a  35271  cvmlift2lem9  35279  cnres2  37723  rngunsnply  43130  proot1hash  43156  omabs2  43294  clcnvlem  43585  cnvtrcl0  43588  trrelsuperrel2dg  43633  brtrclfv2  43689  imo72b2lem1  44131  fourierdlem92  46119  vsetrec  48795