Theorem eqsstrrdi 3975

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

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

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 2121  ax-ext 2703

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

This theorem is referenced by:  eqimsscd  3987  mptss  5986  ffvresb  7053  tposss  8152  sbthlem5  8999  rankxpl  9763  winafp  10583  wunex2  10624  iooval2  13273  telfsumo  15704  structcnvcnv  17059  ressbasssg  17143  ressbasssOLD  17146  resspos  18330  resstos  18331  tsrdir  18505  idresefmnd  18802  idrespermg  19318  symgsssg  19374  gsumzoppg  19851  submomnd  20039  suborng  20786  lidlssbas  21145  dsmmsubg  21675  cnclsi  23182  txss12  23515  txbasval  23516  kqsat  23641  kqcldsat  23643  fmss  23856  cfilucfil  24469  tngtopn  24560  dvaddf  25867  dvmulf  25868  dvcof  25874  dvmptres3  25882  dvmptres2  25888  dvmptcmul  25890  dvmptcj  25894  dvcnvlem  25902  dvcnv  25903  dvcnvrelem1  25944  dvcnvrelem2  25945  plyrem  26235  ulmss  26328  ulmdvlem1  26331  ulmdvlem3  26333  ulmdv  26334  isppw  27046  dchrelbas2  27170  chsupsn  31385  pjss1coi  32135  off2  32615  elrgspnsubrunlem2  33207  elrspunidl  33385  evl1deg2  33532  submatres  33811  madjusmdetlem2  33833  madjusmdetlem3  33834  omsmon  34303  signstfvn  34574  elmsta  35584  mthmpps  35618  dissneqlem  37374  exrecfnlem  37413  prjcrv0  42666  hbtlem6  43162  ofoaf  43388  dvmulcncf  45963  dvdivcncf  45965  itgsubsticclem  46013