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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  eqimsscd  3993  mptss  5993  ffvresb  7059  tposss  8160  sbthlem5  9008  rankxpl  9771  winafp  10591  wunex2  10632  iooval2  13281  telfsumo  15709  structcnvcnv  17064  ressbasssg  17148  ressbasssOLD  17151  resspos  18335  resstos  18336  tsrdir  18510  idresefmnd  18773  idrespermg  19290  symgsssg  19346  gsumzoppg  19823  submomnd  20011  suborng  20761  lidlssbas  21120  dsmmsubg  21650  cnclsi  23157  txss12  23490  txbasval  23491  kqsat  23616  kqcldsat  23618  fmss  23831  cfilucfil  24445  tngtopn  24536  dvaddf  25843  dvmulf  25844  dvcof  25850  dvmptres3  25858  dvmptres2  25864  dvmptcmul  25866  dvmptcj  25870  dvcnvlem  25878  dvcnv  25879  dvcnvrelem1  25920  dvcnvrelem2  25921  plyrem  26211  ulmss  26304  ulmdvlem1  26307  ulmdvlem3  26309  ulmdv  26310  isppw  27022  dchrelbas2  27146  chsupsn  31357  pjss1coi  32107  off2  32584  elrgspnsubrunlem2  33188  elrspunidl  33365  evl1deg2  33512  submatres  33773  madjusmdetlem2  33795  madjusmdetlem3  33796  omsmon  34266  signstfvn  34537  elmsta  35521  mthmpps  35555  dissneqlem  37314  exrecfnlem  37353  prjcrv0  42606  hbtlem6  43102  ofoaf  43328  dvmulcncf  45906  dvdivcncf  45908  itgsubsticclem  45956