Theorem eqsstrrdi 3989

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 3988	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

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

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 3928

This theorem is referenced by:  eqimsscd  4001  mptss  6002  ffvresb  7079  tposss  8183  sbthlem5  9032  rankxpl  9804  winafp  10626  wunex2  10667  iooval2  13315  telfsumo  15744  structcnvcnv  17099  ressbasssg  17183  ressbasssOLD  17186  tsrdir  18539  idresefmnd  18802  idrespermg  19317  symgsssg  19373  gsumzoppg  19850  lidlssbas  21099  dsmmsubg  21628  cnclsi  23135  txss12  23468  txbasval  23469  kqsat  23594  kqcldsat  23596  fmss  23809  cfilucfil  24423  tngtopn  24514  dvaddf  25821  dvmulf  25822  dvcof  25828  dvmptres3  25836  dvmptres2  25842  dvmptcmul  25844  dvmptcj  25848  dvcnvlem  25856  dvcnv  25857  dvcnvrelem1  25898  dvcnvrelem2  25899  plyrem  26189  ulmss  26282  ulmdvlem1  26285  ulmdvlem3  26287  ulmdv  26288  isppw  27000  dchrelbas2  27124  chsupsn  31315  pjss1coi  32065  off2  32538  resspos  32865  resstos  32866  submomnd  32997  elrgspnsubrunlem2  33172  suborng  33266  elrspunidl  33372  evl1deg2  33519  submatres  33769  madjusmdetlem2  33791  madjusmdetlem3  33792  omsmon  34262  signstfvn  34533  elmsta  35508  mthmpps  35542  dissneqlem  37301  exrecfnlem  37340  prjcrv0  42594  hbtlem6  43091  ofoaf  43317  dvmulcncf  45896  dvdivcncf  45898  itgsubsticclem  45946