Theorem eqsstrrdi 3981

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3920

This theorem is referenced by:  eqimsscd  3993  mptss  6009  ffvresb  7080  tposss  8179  sbthlem5  9031  rankxpl  9799  winafp  10620  wunex2  10661  iooval2  13306  telfsumo  15737  structcnvcnv  17092  ressbasssg  17176  ressbasssOLD  17179  resspos  18364  resstos  18365  tsrdir  18539  idresefmnd  18836  idrespermg  19352  symgsssg  19408  gsumzoppg  19885  submomnd  20073  suborng  20821  lidlssbas  21180  dsmmsubg  21710  cnclsi  23228  txss12  23561  txbasval  23562  kqsat  23687  kqcldsat  23689  fmss  23902  cfilucfil  24515  tngtopn  24606  dvaddf  25913  dvmulf  25914  dvcof  25920  dvmptres3  25928  dvmptres2  25934  dvmptcmul  25936  dvmptcj  25940  dvcnvlem  25948  dvcnv  25949  dvcnvrelem1  25990  dvcnvrelem2  25991  plyrem  26281  ulmss  26374  ulmdvlem1  26377  ulmdvlem3  26379  ulmdv  26380  isppw  27092  dchrelbas2  27216  chsupsn  31501  pjss1coi  32251  off2  32731  elrgspnsubrunlem2  33342  elrspunidl  33521  evl1deg2  33670  submatres  33984  madjusmdetlem2  34006  madjusmdetlem3  34007  omsmon  34476  signstfvn  34747  elmsta  35764  mthmpps  35798  dissneqlem  37595  exrecfnlem  37634  prjcrv0  42991  hbtlem6  43486  ofoaf  43712  dvmulcncf  46283  dvdivcncf  46285  itgsubsticclem  46333