Theorem eqsstrrdi 3976

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

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

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 2705

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

This theorem is referenced by:  eqimsscd  3988  mptss  5998  ffvresb  7067  tposss  8166  sbthlem5  9015  rankxpl  9779  winafp  10599  wunex2  10640  iooval2  13285  telfsumo  15716  structcnvcnv  17071  ressbasssg  17155  ressbasssOLD  17158  resspos  18343  resstos  18344  tsrdir  18518  idresefmnd  18815  idrespermg  19331  symgsssg  19387  gsumzoppg  19864  submomnd  20052  suborng  20800  lidlssbas  21159  dsmmsubg  21689  cnclsi  23207  txss12  23540  txbasval  23541  kqsat  23666  kqcldsat  23668  fmss  23881  cfilucfil  24494  tngtopn  24585  dvaddf  25892  dvmulf  25893  dvcof  25899  dvmptres3  25907  dvmptres2  25913  dvmptcmul  25915  dvmptcj  25919  dvcnvlem  25927  dvcnv  25928  dvcnvrelem1  25969  dvcnvrelem2  25970  plyrem  26260  ulmss  26353  ulmdvlem1  26356  ulmdvlem3  26358  ulmdv  26359  isppw  27071  dchrelbas2  27195  chsupsn  31414  pjss1coi  32164  off2  32645  elrgspnsubrunlem2  33258  elrspunidl  33437  evl1deg2  33586  submatres  33891  madjusmdetlem2  33913  madjusmdetlem3  33914  omsmon  34383  signstfvn  34654  elmsta  35664  mthmpps  35698  dissneqlem  37457  exrecfnlem  37496  prjcrv0  42791  hbtlem6  43286  ofoaf  43512  dvmulcncf  46085  dvdivcncf  46087  itgsubsticclem  46135