Theorem eqsstrrdi 3992

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

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

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 2701

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

This theorem is referenced by:  eqimsscd  4004  mptss  6013  ffvresb  7097  tposss  8206  sbthlem5  9055  rankxpl  9828  winafp  10650  wunex2  10691  iooval2  13339  telfsumo  15768  structcnvcnv  17123  ressbasssg  17207  ressbasssOLD  17210  tsrdir  18563  idresefmnd  18826  idrespermg  19341  symgsssg  19397  gsumzoppg  19874  lidlssbas  21123  dsmmsubg  21652  cnclsi  23159  txss12  23492  txbasval  23493  kqsat  23618  kqcldsat  23620  fmss  23833  cfilucfil  24447  tngtopn  24538  dvaddf  25845  dvmulf  25846  dvcof  25852  dvmptres3  25860  dvmptres2  25866  dvmptcmul  25868  dvmptcj  25872  dvcnvlem  25880  dvcnv  25881  dvcnvrelem1  25922  dvcnvrelem2  25923  plyrem  26213  ulmss  26306  ulmdvlem1  26309  ulmdvlem3  26311  ulmdv  26312  isppw  27024  dchrelbas2  27148  chsupsn  31342  pjss1coi  32092  off2  32565  resspos  32892  resstos  32893  submomnd  33024  elrgspnsubrunlem2  33199  suborng  33293  elrspunidl  33399  evl1deg2  33546  submatres  33796  madjusmdetlem2  33818  madjusmdetlem3  33819  omsmon  34289  signstfvn  34560  elmsta  35535  mthmpps  35569  dissneqlem  37328  exrecfnlem  37367  prjcrv0  42621  hbtlem6  43118  ofoaf  43344  dvmulcncf  45923  dvdivcncf  45925  itgsubsticclem  45973