Theorem eqsstrrdi 3954

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ⊆ wss 3896

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3897

This theorem is used by:  eqimsscd  3966  mptss  6036  ffvresb  7131  tposss  8251  sbthlem5  9117  rankxpl  9899  winafp  10789  wunex2  10830  iooval2  13516  telfsumo  15978  structcnvcnv  17340  ressbasssg  17424  ressbasssOLD  17427  resspos  18612  resstos  18613  tsrdir  18787  idresefmnd  19104  idrespermg  19634  symgsssg  19690  gsumzoppg  20167  submomnd  20355  suborng  21142  lidlssbas  21501  dsmmsubg  22058  cnclsi  23599  txss12  23933  txbasval  23934  kqsat  24059  kqcldsat  24061  fmss  24274  cfilucfil  24887  tngtopn  24978  dvaddf  26271  dvmulf  26272  dvcof  26277  dvmptres3  26285  dvmptres2  26291  dvmptcmul  26293  dvmptcj  26297  dvcnvlem  26305  dvcnv  26306  dvcnvrelem1  26346  dvcnvrelem2  26347  plyrem  26635  ulmss  26733  ulmdvlem1  26736  ulmdvlem3  26738  ulmdv  26739  isppw  27450  dchrelbas2  27573  chsupsn  32024  pjss1coi  32774  off2  33286  padct  33361  elrgspnsubrunlem2  33859  elrspunidl  34028  evl1deg2  34159  submatres  34488  madjusmdetlem2  34510  madjusmdetlem3  34511  omsmon  34980  signstfvn  35248  elmsta  36403  mthmpps  36437  dissneqlem  38372  exrecfnlem  38411  prjcrv0  43778  hbtlem6  44240  ofoaf  44466  dvmulcncf  47043  dvdivcncf  47045  itgsubsticclem  47093