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 2766	. 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 2732

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

This theorem is used by:  eqimsscd  3988  mptss  6038  ffvresb  7119  tposss  8225  sbthlem5  9089  rankxpl  9857  winafp  10706  wunex2  10747  iooval2  13431  telfsumo  15889  structcnvcnv  17245  ressbasssg  17329  ressbasssOLD  17332  resspos  18517  resstos  18518  tsrdir  18692  idresefmnd  19008  idrespermg  19538  symgsssg  19594  gsumzoppg  20071  submomnd  20259  suborng  21042  lidlssbas  21401  dsmmsubg  21956  cnclsi  23497  txss12  23831  txbasval  23832  kqsat  23957  kqcldsat  23959  fmss  24172  cfilucfil  24785  tngtopn  24876  dvaddf  26169  dvmulf  26170  dvcof  26175  dvmptres3  26183  dvmptres2  26189  dvmptcmul  26191  dvmptcj  26195  dvcnvlem  26203  dvcnv  26204  dvcnvrelem1  26244  dvcnvrelem2  26245  plyrem  26535  ulmss  26633  ulmdvlem1  26636  ulmdvlem3  26638  ulmdv  26639  isppw  27350  dchrelbas2  27473  chsupsn  31894  pjss1coi  32644  off2  33114  padct  33189  elrgspnsubrunlem2  33688  elrspunidl  33856  evl1deg2  33987  submatres  34316  madjusmdetlem2  34338  madjusmdetlem3  34339  omsmon  34809  signstfvn  35077  elmsta  36127  mthmpps  36161  dissneqlem  38094  exrecfnlem  38133  prjcrv0  43479  hbtlem6  43970  ofoaf  44196  dvmulcncf  46753  dvdivcncf  46755  itgsubsticclem  46803