Theorem eqsstrrdi 3982

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

Syntax hints:   → wi 4   = wceq 1570   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3922

This theorem is referenced by:  eqimsscd  3994  mptss  6044  ffvresb  7121  tposss  8219  sbthlem5  9075  rankxpl  9843  winafp  10677  wunex2  10718  iooval2  13400  telfsumo  15850  structcnvcnv  17208  ressbasssg  17292  ressbasssOLD  17295  resspos  18480  resstos  18481  tsrdir  18655  idresefmnd  18953  idrespermg  19476  symgsssg  19532  gsumzoppg  20009  submomnd  20197  suborng  20979  lidlssbas  21338  dsmmsubg  21893  cnclsi  23429  txss12  23762  txbasval  23763  kqsat  23888  kqcldsat  23890  fmss  24103  cfilucfil  24716  tngtopn  24807  dvaddf  26101  dvmulf  26102  dvcof  26107  dvmptres3  26115  dvmptres2  26121  dvmptcmul  26123  dvmptcj  26127  dvcnvlem  26135  dvcnv  26136  dvcnvrelem1  26176  dvcnvrelem2  26177  plyrem  26466  ulmss  26560  ulmdvlem1  26563  ulmdvlem3  26565  ulmdv  26566  isppw  27278  dchrelbas2  27401  chsupsn  31765  pjss1coi  32515  off2  32986  padct  33063  elrgspnsubrunlem2  33568  elrspunidl  33736  evl1deg2  33867  submatres  34196  madjusmdetlem2  34218  madjusmdetlem3  34219  omsmon  34688  signstfvn  34956  elmsta  36040  mthmpps  36074  dissneqlem  37986  exrecfnlem  38025  prjcrv0  43365  hbtlem6  43856  ofoaf  44082  dvmulcncf  46639  dvdivcncf  46641  itgsubsticclem  46689