Theorem eqsstrrdi 3995

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

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

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 2702

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

This theorem is referenced by:  eqimsscd  4007  mptss  6016  ffvresb  7100  tposss  8209  sbthlem5  9061  rankxpl  9835  winafp  10657  wunex2  10698  iooval2  13346  telfsumo  15775  structcnvcnv  17130  ressbasssg  17214  ressbasssOLD  17217  tsrdir  18570  idresefmnd  18833  idrespermg  19348  symgsssg  19404  gsumzoppg  19881  lidlssbas  21130  dsmmsubg  21659  cnclsi  23166  txss12  23499  txbasval  23500  kqsat  23625  kqcldsat  23627  fmss  23840  cfilucfil  24454  tngtopn  24545  dvaddf  25852  dvmulf  25853  dvcof  25859  dvmptres3  25867  dvmptres2  25873  dvmptcmul  25875  dvmptcj  25879  dvcnvlem  25887  dvcnv  25888  dvcnvrelem1  25929  dvcnvrelem2  25930  plyrem  26220  ulmss  26313  ulmdvlem1  26316  ulmdvlem3  26318  ulmdv  26319  isppw  27031  dchrelbas2  27155  chsupsn  31349  pjss1coi  32099  off2  32572  resspos  32899  resstos  32900  submomnd  33031  elrgspnsubrunlem2  33206  suborng  33300  elrspunidl  33406  evl1deg2  33553  submatres  33803  madjusmdetlem2  33825  madjusmdetlem3  33826  omsmon  34296  signstfvn  34567  elmsta  35542  mthmpps  35576  dissneqlem  37335  exrecfnlem  37374  prjcrv0  42628  hbtlem6  43125  ofoaf  43351  dvmulcncf  45930  dvdivcncf  45932  itgsubsticclem  45980