Theorem eqsstrrid 4030

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 4029	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

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

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 3954  df-ss 3964

This theorem is referenced by:  relcnvtrg  6262  fimacnvdisj  6766  dffv2  6983  fimacnvOLD  7069  f1ompt  7107  abnexg  7739  fnwelem  8113  tfrlem15  8388  omxpenlem  9069  hartogslem1  9533  ttrcltr  9707  dfttrcl2  9715  infxpidm2  10008  alephgeom  10073  infenaleph  10082  cfflb  10250  pwfseqlem5  10654  imasvscafn  17479  mrieqvlemd  17569  cnvps  18527  dirdm  18549  tsrdir  18553  frmdss2  18740  subdrgint  20411  iinopn  22395  neitr  22675  xkococnlem  23154  tgpconncomp  23608  trcfilu  23790  mbfconstlem  25135  itg2seq  25251  limcdif  25384  dvres2lem  25418  c1lip3  25507  lhop  25524  plyeq0  25716  dchrghm  26748  negsbdaylem  27519  precsexlem10  27651  uspgrupgrushgr  28426  upgrreslem  28550  umgrreslem  28551  umgrres1  28560  umgr2v2e  28771  chssoc  30736  gsumhashmul  32195  pmtrcnelor  32239  tocycfvres1  32256  tocycfvres2  32257  dimkerim  32700  hauseqcn  32866  carsgclctunlem3  33307  cvmliftmolem1  34260  cvmlift2lem9a  34282  cvmlift2lem9  34290  cnres2  36619  rngunsnply  41900  proot1hash  41927  omabs2  42067  clcnvlem  42359  cnvtrcl0  42362  trrelsuperrel2dg  42407  brtrclfv2  42463  imo72b2lem1  42906  fourierdlem92  44900  vsetrec  47701