Theorem eqsstrrdi 4064

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

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993

This theorem is referenced by:  eqimsscd  4066  mptss  6071  ffvresb  7159  tposss  8268  sbthlem5  9153  rankxpl  9944  winafp  10766  wunex2  10807  iooval2  13440  telfsumo  15850  structcnvcnv  17200  ressbasssg  17295  ressbasssOLD  17298  tsrdir  18674  idresefmnd  18934  idrespermg  19453  symgsssg  19509  gsumzoppg  19986  lidlssbas  21246  dsmmsubg  21786  cnclsi  23301  txss12  23634  txbasval  23635  kqsat  23760  kqcldsat  23762  fmss  23975  cfilucfil  24593  tngtopn  24692  dvaddf  25999  dvmulf  26000  dvcof  26006  dvmptres3  26014  dvmptres2  26020  dvmptcmul  26022  dvmptcj  26026  dvcnvlem  26034  dvcnv  26035  dvcnvrelem1  26076  dvcnvrelem2  26077  plyrem  26365  ulmss  26458  ulmdvlem1  26461  ulmdvlem3  26463  ulmdv  26464  isppw  27175  dchrelbas2  27299  pw2bday  28436  chsupsn  31445  pjss1coi  32195  off2  32660  resspos  32939  resstos  32940  submomnd  33060  suborng  33310  elrspunidl  33421  evl1deg2  33567  submatres  33752  madjusmdetlem2  33774  madjusmdetlem3  33775  omsmon  34263  signstfvn  34546  elmsta  35516  mthmpps  35550  dissneqlem  37306  exrecfnlem  37345  prjcrv0  42588  hbtlem6  43086  ofoaf  43317  dvmulcncf  45846  dvdivcncf  45848  itgsubsticclem  45896