Theorem eqsstrrdi 3958

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 2769	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3		eqsstrrdi.2	. 2 ⊢ 𝐵 ⊆ 𝐶
4	2, 3	eqsstrdi 3957	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  eqimsscd  3970  mptss  6052  ffvresb  7158  tposss  8282  sbthlem5  9148  rankxpl  9929  winafp  10821  wunex2  10862  iooval2  13549  telfsumo  16013  structcnvcnv  17375  ressbasssg  17459  ressbasssOLD  17462  resspos  18653  resstos  18654  tsrdir  18828  idresefmnd  19145  idrespermg  19676  symgsssg  19732  gsumzoppg  20209  submomnd  20397  suborng  21184  lidlssbas  21543  dsmmsubg  22104  cnclsi  23645  txss12  23979  txbasval  23980  kqsat  24105  kqcldsat  24107  fmss  24320  cfilucfil  24933  tngtopn  25024  dvaddf  26317  dvmulf  26318  dvcof  26323  dvmptres3  26331  dvmptres2  26337  dvmptcmul  26339  dvmptcj  26343  dvcnvlem  26351  dvcnv  26352  dvcnvrelem1  26392  dvcnvrelem2  26393  plyrem  26681  ulmss  26781  ulmdvlem1  26784  ulmdvlem3  26786  ulmdv  26787  isppw  27498  dchrelbas2  27621  chsupsn  32072  pjss1coi  32822  off2  33333  padct  33407  elrgspnsubrunlem2  33908  elrspunidl  34082  evl1deg2  34212  submatres  34549  madjusmdetlem2  34571  madjusmdetlem3  34572  omsmon  35041  signstfvn  35309  elmsta  36521  mthmpps  36555  dissneqlem  38531  exrecfnlem  38570  prjcrv0  43935  hbtlem6  44396  ofoaf  44618  dvmulcncf  47208  dvdivcncf  47210  itgsubsticclem  47258