Theorem eqsstrrdi 3960

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

Syntax hints:   → wi 4   = wceq 1547   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-ss 3900

This theorem is referenced by:  eqimsscd  3972  mptss  5994  ffvresb  7067  tposss  8167  sbthlem5  9019  rankxpl  9790  winafp  10611  wunex2  10652  iooval2  13322  telfsumo  15756  structcnvcnv  17114  ressbasssg  17198  ressbasssOLD  17201  resspos  18386  resstos  18387  tsrdir  18561  idresefmnd  18858  idrespermg  19377  symgsssg  19433  gsumzoppg  19910  submomnd  20098  suborng  20848  lidlssbas  21206  dsmmsubg  21718  cnclsi  23255  txss12  23588  txbasval  23589  kqsat  23714  kqcldsat  23716  fmss  23929  cfilucfil  24542  tngtopn  24633  dvaddf  25927  dvmulf  25928  dvcof  25933  dvmptres3  25941  dvmptres2  25947  dvmptcmul  25949  dvmptcj  25953  dvcnvlem  25961  dvcnv  25962  dvcnvrelem1  26002  dvcnvrelem2  26003  plyrem  26289  ulmss  26380  ulmdvlem1  26383  ulmdvlem3  26385  ulmdv  26386  isppw  27095  dchrelbas2  27218  chsupsn  31502  pjss1coi  32252  off2  32733  padct  32810  elrgspnsubrunlem2  33329  elrspunidl  33511  evl1deg2  33660  submatres  33990  madjusmdetlem2  34012  madjusmdetlem3  34013  omsmon  34482  signstfvn  34753  elmsta  35776  mthmpps  35810  dissneqlem  37702  exrecfnlem  37741  prjcrv0  43083  hbtlem6  43574  ofoaf  43800  dvmulcncf  46368  dvdivcncf  46370  itgsubsticclem  46418