Theorem eqsstrrdi 3979

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ss 3918

This theorem is referenced by:  eqimsscd  3991  mptss  6001  ffvresb  7070  tposss  8169  sbthlem5  9019  rankxpl  9787  winafp  10608  wunex2  10649  iooval2  13294  telfsumo  15725  structcnvcnv  17080  ressbasssg  17164  ressbasssOLD  17167  resspos  18352  resstos  18353  tsrdir  18527  idresefmnd  18824  idrespermg  19340  symgsssg  19396  gsumzoppg  19873  submomnd  20061  suborng  20809  lidlssbas  21168  dsmmsubg  21698  cnclsi  23216  txss12  23549  txbasval  23550  kqsat  23675  kqcldsat  23677  fmss  23890  cfilucfil  24503  tngtopn  24594  dvaddf  25901  dvmulf  25902  dvcof  25908  dvmptres3  25916  dvmptres2  25922  dvmptcmul  25924  dvmptcj  25928  dvcnvlem  25936  dvcnv  25937  dvcnvrelem1  25978  dvcnvrelem2  25979  plyrem  26269  ulmss  26362  ulmdvlem1  26365  ulmdvlem3  26367  ulmdv  26368  isppw  27080  dchrelbas2  27204  chsupsn  31488  pjss1coi  32238  off2  32719  elrgspnsubrunlem2  33330  elrspunidl  33509  evl1deg2  33658  submatres  33963  madjusmdetlem2  33985  madjusmdetlem3  33986  omsmon  34455  signstfvn  34726  elmsta  35742  mthmpps  35776  dissneqlem  37545  exrecfnlem  37584  prjcrv0  42876  hbtlem6  43371  ofoaf  43597  dvmulcncf  46169  dvdivcncf  46171  itgsubsticclem  46219