Theorem eqsstrrid 3971

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

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905

This theorem is referenced by:  relcnvtrg  6174  fimacnvdisj  6661  dffv2  6872  fimacnvOLD  6957  f1ompt  6994  abnexg  7615  fnwelem  7981  tfrlem15  8232  omxpenlem  8869  hartogslem1  9310  ttrcltr  9483  dfttrcl2  9491  infxpidm2  9782  alephgeom  9847  infenaleph  9856  cfflb  10024  pwfseqlem5  10428  imasvscafn  17257  mrieqvlemd  17347  cnvps  18305  dirdm  18327  tsrdir  18331  frmdss2  18511  subdrgint  20080  iinopn  22060  neitr  22340  xkococnlem  22819  tgpconncomp  23273  trcfilu  23455  mbfconstlem  24800  itg2seq  24916  limcdif  25049  dvres2lem  25083  c1lip3  25172  lhop  25189  plyeq0  25381  dchrghm  26413  uspgrupgrushgr  27556  upgrreslem  27680  umgrreslem  27681  umgrres1  27690  umgr2v2e  27901  chssoc  29867  gsumhashmul  31325  pmtrcnelor  31369  tocycfvres1  31386  tocycfvres2  31387  dimkerim  31717  hauseqcn  31857  carsgclctunlem3  32296  cvmliftmolem1  33252  cvmlift2lem9a  33274  cvmlift2lem9  33282  cnres2  35930  rngunsnply  41005  proot1hash  41032  clcnvlem  41238  cnvtrcl0  41241  trrelsuperrel2dg  41286  brtrclfv2  41342  imo72b2lem1  41787  fourierdlem92  43746  vsetrec  46419