Theorem eqsstrrid 4032

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3956  df-ss 3966

This theorem is referenced by:  relcnvtrg  6266  fimacnvdisj  6770  dffv2  6987  fimacnvOLD  7073  f1ompt  7113  abnexg  7746  fnwelem  8120  tfrlem15  8395  omxpenlem  9076  hartogslem1  9540  ttrcltr  9714  dfttrcl2  9722  infxpidm2  10015  alephgeom  10080  infenaleph  10089  cfflb  10257  pwfseqlem5  10661  imasvscafn  17488  mrieqvlemd  17578  cnvps  18536  dirdm  18558  tsrdir  18562  frmdss2  18781  subdrgint  20563  iinopn  22625  neitr  22905  xkococnlem  23384  tgpconncomp  23838  trcfilu  24020  mbfconstlem  25377  itg2seq  25493  limcdif  25626  dvres2lem  25660  c1lip3  25749  lhop  25766  plyeq0  25958  dchrghm  26992  negsbdaylem  27766  precsexlem10  27898  uspgrupgrushgr  28701  upgrreslem  28825  umgrreslem  28826  umgrres1  28835  umgr2v2e  29046  chssoc  31013  gsumhashmul  32475  pmtrcnelor  32519  tocycfvres1  32536  tocycfvres2  32537  dimkerim  32997  hauseqcn  33173  carsgclctunlem3  33614  cvmliftmolem1  34567  cvmlift2lem9a  34589  cvmlift2lem9  34597  cnres2  36935  rngunsnply  42218  proot1hash  42245  omabs2  42385  clcnvlem  42677  cnvtrcl0  42680  trrelsuperrel2dg  42725  brtrclfv2  42781  imo72b2lem1  43224  fourierdlem92  45214  vsetrec  47837