Theorem eqsstrrid 4045

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

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

This theorem is referenced by:  relcnvtrg  6288  fimacnvdisj  6787  dffv2  7004  f1ompt  7131  abnexg  7775  fnwelem  8155  tfrlem15  8431  omxpenlem  9112  hartogslem1  9580  ttrcltr  9754  dfttrcl2  9762  infxpidm2  10055  alephgeom  10120  infenaleph  10129  cfflb  10297  pwfseqlem5  10701  imasvscafn  17584  mrieqvlemd  17674  cnvps  18636  dirdm  18658  tsrdir  18662  frmdss2  18889  subdrgint  20821  iinopn  22924  neitr  23204  xkococnlem  23683  tgpconncomp  24137  trcfilu  24319  mbfconstlem  25676  itg2seq  25792  limcdif  25926  dvres2lem  25960  c1lip3  26053  lhop  26070  plyeq0  26265  dchrghm  27315  negsbdaylem  28103  precsexlem10  28255  uspgrupgrushgr  29211  upgrreslem  29336  umgrreslem  29337  umgrres1  29346  umgr2v2e  29558  chssoc  31525  gsumhashmul  33047  pmtrcnelor  33094  tocycfvres1  33113  tocycfvres2  33114  dimkerim  33655  hauseqcn  33859  carsgclctunlem3  34302  cvmliftmolem1  35266  cvmlift2lem9a  35288  cvmlift2lem9  35296  cnres2  37750  rngunsnply  43158  proot1hash  43184  omabs2  43322  clcnvlem  43613  cnvtrcl0  43616  trrelsuperrel2dg  43661  brtrclfv2  43717  imo72b2lem1  44159  fourierdlem92  46154  vsetrec  48934