Theorem eqsstrrdi 4051

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

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-ss 3980

This theorem is referenced by:  eqimsscd  4053  mptss  6062  ffvresb  7145  tposss  8251  sbthlem5  9126  rankxpl  9913  winafp  10735  wunex2  10776  iooval2  13417  telfsumo  15835  structcnvcnv  17187  ressbasssg  17282  ressbasssOLD  17285  tsrdir  18662  idresefmnd  18925  idrespermg  19444  symgsssg  19500  gsumzoppg  19977  lidlssbas  21241  dsmmsubg  21781  cnclsi  23296  txss12  23629  txbasval  23630  kqsat  23755  kqcldsat  23757  fmss  23970  cfilucfil  24588  tngtopn  24687  dvaddf  25994  dvmulf  25995  dvcof  26001  dvmptres3  26009  dvmptres2  26015  dvmptcmul  26017  dvmptcj  26021  dvcnvlem  26029  dvcnv  26030  dvcnvrelem1  26071  dvcnvrelem2  26072  plyrem  26362  ulmss  26455  ulmdvlem1  26458  ulmdvlem3  26460  ulmdv  26461  isppw  27172  dchrelbas2  27296  pw2bday  28433  chsupsn  31442  pjss1coi  32192  off2  32658  resspos  32941  resstos  32942  submomnd  33070  suborng  33325  elrspunidl  33436  evl1deg2  33582  submatres  33767  madjusmdetlem2  33789  madjusmdetlem3  33790  omsmon  34280  signstfvn  34563  elmsta  35533  mthmpps  35567  dissneqlem  37323  exrecfnlem  37362  prjcrv0  42620  hbtlem6  43118  ofoaf  43345  dvmulcncf  45881  dvdivcncf  45883  itgsubsticclem  45931