Theorem eqsstrrdi 4029

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

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

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 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  eqimsscd  4041  mptss  6060  ffvresb  7145  tposss  8252  sbthlem5  9127  rankxpl  9915  winafp  10737  wunex2  10778  iooval2  13420  telfsumo  15838  structcnvcnv  17190  ressbasssg  17282  ressbasssOLD  17285  tsrdir  18649  idresefmnd  18912  idrespermg  19429  symgsssg  19485  gsumzoppg  19962  lidlssbas  21223  dsmmsubg  21763  cnclsi  23280  txss12  23613  txbasval  23614  kqsat  23739  kqcldsat  23741  fmss  23954  cfilucfil  24572  tngtopn  24671  dvaddf  25979  dvmulf  25980  dvcof  25986  dvmptres3  25994  dvmptres2  26000  dvmptcmul  26002  dvmptcj  26006  dvcnvlem  26014  dvcnv  26015  dvcnvrelem1  26056  dvcnvrelem2  26057  plyrem  26347  ulmss  26440  ulmdvlem1  26443  ulmdvlem3  26445  ulmdv  26446  isppw  27157  dchrelbas2  27281  pw2bday  28418  chsupsn  31432  pjss1coi  32182  off2  32651  resspos  32956  resstos  32957  submomnd  33087  elrgspnsubrunlem2  33252  suborng  33345  elrspunidl  33456  evl1deg2  33602  submatres  33805  madjusmdetlem2  33827  madjusmdetlem3  33828  omsmon  34300  signstfvn  34584  elmsta  35553  mthmpps  35587  dissneqlem  37341  exrecfnlem  37380  prjcrv0  42643  hbtlem6  43141  ofoaf  43368  dvmulcncf  45940  dvdivcncf  45942  itgsubsticclem  45990