Theorem eqsstrrdi 3976

Description: A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017.)

Hypotheses

Ref	Expression
eqsstrrdi.1	⊢ (𝜑 → 𝐵 = 𝐴)
eqsstrrdi.2	⊢ 𝐵 ⊆ 𝐶

Assertion

Ref	Expression
eqsstrrdi	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem eqsstrrdi

Step	Hyp	Ref	Expression
1		eqsstrrdi.1	. . 3 ⊢ (𝜑 → 𝐵 = 𝐴)
2	1	eqcomd 2767	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3		eqsstrrdi.2	. 2 ⊢ 𝐵 ⊆ 𝐶
4	2, 3	eqsstrdi 3975	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ss 3916

This theorem is used by:  eqimsscd  3988  mptss  6034  ffvresb  7124  tposss  8237  sbthlem5  9103  rankxpl  9885  winafp  10775  wunex2  10816  iooval2  13502  telfsumo  15962  structcnvcnv  17324  ressbasssg  17408  ressbasssOLD  17411  resspos  18596  resstos  18597  tsrdir  18771  idresefmnd  19088  idrespermg  19618  symgsssg  19674  gsumzoppg  20151  submomnd  20339  suborng  21126  lidlssbas  21485  dsmmsubg  22042  cnclsi  23583  txss12  23917  txbasval  23918  kqsat  24043  kqcldsat  24045  fmss  24258  cfilucfil  24871  tngtopn  24962  dvaddf  26255  dvmulf  26256  dvcof  26261  dvmptres3  26269  dvmptres2  26275  dvmptcmul  26277  dvmptcj  26281  dvcnvlem  26289  dvcnv  26290  dvcnvrelem1  26330  dvcnvrelem2  26331  plyrem  26619  ulmss  26717  ulmdvlem1  26720  ulmdvlem3  26722  ulmdv  26723  isppw  27434  dchrelbas2  27557  chsupsn  32008  pjss1coi  32758  off2  33228  padct  33303  elrgspnsubrunlem2  33802  elrspunidl  33971  evl1deg2  34102  submatres  34431  madjusmdetlem2  34453  madjusmdetlem3  34454  omsmon  34923  signstfvn  35191  elmsta  36292  mthmpps  36326  dissneqlem  38243  exrecfnlem  38282  prjcrv0  43649  hbtlem6  44115  ofoaf  44341  dvmulcncf  46904  dvdivcncf  46906  itgsubsticclem  46954