Theorem eqsstrrdi 3970

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

Syntax hints:   → wi 4   = wceq 1538   ⊆ wss 3881

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  mptss  5877  ffvresb  6865  tposss  7876  sbthlem5  8615  rankxpl  9288  winafp  10108  wunex2  10149  iooval2  12759  telfsumo  15149  structcnvcnv  16489  ressbasss  16548  tsrdir  17840  idresefmnd  18056  idrespermg  18531  symgsssg  18587  gsumzoppg  19057  dsmmsubg  20432  opsrtoslem2  20724  cnclsi  21877  txss12  22210  txbasval  22211  kqsat  22336  kqcldsat  22338  fmss  22551  cfilucfil  23166  tngtopn  23256  dvaddf  24545  dvmulf  24546  dvcof  24551  dvmptres3  24559  dvmptres2  24565  dvmptcmul  24567  dvmptcj  24571  dvcnvlem  24579  dvcnv  24580  dvcnvrelem1  24620  dvcnvrelem2  24621  plyrem  24901  ulmss  24992  ulmdvlem1  24995  ulmdvlem3  24997  ulmdv  24998  isppw  25699  dchrelbas2  25821  chsupsn  29196  pjss1coi  29946  off2  30402  resspos  30672  resstos  30673  submomnd  30761  suborng  30939  elrspunidl  31014  submatres  31159  madjusmdetlem2  31181  madjusmdetlem3  31182  omsmon  31666  signstfvn  31949  elmsta  32908  mthmpps  32942  dissneqlem  34757  exrecfnlem  34796  hbtlem6  40073  dvmulcncf  42567  dvdivcncf  42569  itgsubsticclem  42617  lidlssbas  44546