Theorem eqsstrrdi 4037

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

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

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965

This theorem is referenced by:  eqimsscd  4039  mptss  6042  ffvresb  7126  tposss  8214  sbthlem5  9089  rankxpl  9872  winafp  10694  wunex2  10735  iooval2  13359  telfsumo  15750  structcnvcnv  17088  ressbasssg  17183  ressbasssOLD  17186  tsrdir  18559  idresefmnd  18782  idrespermg  19281  symgsssg  19337  gsumzoppg  19814  dsmmsubg  21304  opsrtoslem2  21623  cnclsi  22783  txss12  23116  txbasval  23117  kqsat  23242  kqcldsat  23244  fmss  23457  cfilucfil  24075  tngtopn  24174  dvaddf  25466  dvmulf  25467  dvcof  25472  dvmptres3  25480  dvmptres2  25486  dvmptcmul  25488  dvmptcj  25492  dvcnvlem  25500  dvcnv  25501  dvcnvrelem1  25541  dvcnvrelem2  25542  plyrem  25825  ulmss  25916  ulmdvlem1  25919  ulmdvlem3  25921  ulmdv  25922  isppw  26625  dchrelbas2  26747  chsupsn  30704  pjss1coi  31454  off2  31904  resspos  32174  resstos  32175  submomnd  32269  suborng  32474  elrspunidl  32591  submatres  32855  madjusmdetlem2  32877  madjusmdetlem3  32878  omsmon  33366  signstfvn  33649  elmsta  34608  mthmpps  34642  dissneqlem  36307  exrecfnlem  36346  prjcrv0  41457  hbtlem6  41953  ofoaf  42187  dvmulcncf  44720  dvdivcncf  44722  itgsubsticclem  44770  lidlssbas  46833