Theorem eqsstrrdi 4009

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

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

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 2708

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

This theorem is referenced by:  eqimsscd  4021  mptss  6034  ffvresb  7120  tposss  8231  sbthlem5  9106  rankxpl  9894  winafp  10716  wunex2  10757  iooval2  13400  telfsumo  15823  structcnvcnv  17177  ressbasssg  17263  ressbasssOLD  17266  tsrdir  18619  idresefmnd  18882  idrespermg  19397  symgsssg  19453  gsumzoppg  19930  lidlssbas  21179  dsmmsubg  21708  cnclsi  23215  txss12  23548  txbasval  23549  kqsat  23674  kqcldsat  23676  fmss  23889  cfilucfil  24503  tngtopn  24594  dvaddf  25902  dvmulf  25903  dvcof  25909  dvmptres3  25917  dvmptres2  25923  dvmptcmul  25925  dvmptcj  25929  dvcnvlem  25937  dvcnv  25938  dvcnvrelem1  25979  dvcnvrelem2  25980  plyrem  26270  ulmss  26363  ulmdvlem1  26366  ulmdvlem3  26368  ulmdv  26369  isppw  27081  dchrelbas2  27205  chsupsn  31399  pjss1coi  32149  off2  32624  resspos  32951  resstos  32952  submomnd  33083  elrgspnsubrunlem2  33248  suborng  33342  elrspunidl  33448  evl1deg2  33595  submatres  33842  madjusmdetlem2  33864  madjusmdetlem3  33865  omsmon  34335  signstfvn  34606  elmsta  35575  mthmpps  35609  dissneqlem  37363  exrecfnlem  37402  prjcrv0  42623  hbtlem6  43120  ofoaf  43346  dvmulcncf  45921  dvdivcncf  45923  itgsubsticclem  45971