Theorem eqsstrrid 3989

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ss 3934

This theorem is referenced by:  3sstr3g  4002  relcnvtrg  6242  fimacnvdisj  6741  dffv2  6959  f1ompt  7086  abnexg  7735  fnwelem  8113  tfrlem15  8363  omxpenlem  9047  hartogslem1  9502  ttrcltr  9676  dfttrcl2  9684  infxpidm2  9977  alephgeom  10042  infenaleph  10051  cfflb  10219  pwfseqlem5  10623  imasvscafn  17507  mrieqvlemd  17597  cnvps  18544  dirdm  18566  tsrdir  18570  frmdss2  18797  subdrgint  20719  iinopn  22796  neitr  23074  xkococnlem  23553  tgpconncomp  24007  trcfilu  24188  mbfconstlem  25535  itg2seq  25650  limcdif  25784  dvres2lem  25818  c1lip3  25911  lhop  25928  plyeq0  26123  dchrghm  27174  negsbdaylem  27969  precsexlem10  28125  uspgrupgrushgr  29113  upgrreslem  29238  umgrreslem  29239  umgrres1  29248  umgr2v2e  29460  chssoc  31432  tpssbd  32476  tpsscd  32477  gsumhashmul  33008  pmtrcnelor  33055  tocycfvres1  33074  tocycfvres2  33075  elrgspnsubrunlem2  33206  dimkerim  33630  hauseqcn  33895  carsgclctunlem3  34318  cvmliftmolem1  35275  cvmlift2lem9a  35297  cvmlift2lem9  35305  cnres2  37764  rngunsnply  43165  proot1hash  43191  omabs2  43328  clcnvlem  43619  cnvtrcl0  43622  trrelsuperrel2dg  43667  brtrclfv2  43723  imo72b2lem1  44165  fourierdlem92  46203  vsetrec  49696