Theorem eqsstrrdi 3983

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

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

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 2701

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

This theorem is referenced by:  eqimsscd  3995  mptss  5997  ffvresb  7063  tposss  8167  sbthlem5  9015  rankxpl  9790  winafp  10610  wunex2  10651  iooval2  13300  telfsumo  15728  structcnvcnv  17083  ressbasssg  17167  ressbasssOLD  17170  resspos  18354  resstos  18355  tsrdir  18529  idresefmnd  18792  idrespermg  19309  symgsssg  19365  gsumzoppg  19842  submomnd  20030  suborng  20780  lidlssbas  21139  dsmmsubg  21669  cnclsi  23176  txss12  23509  txbasval  23510  kqsat  23635  kqcldsat  23637  fmss  23850  cfilucfil  24464  tngtopn  24555  dvaddf  25862  dvmulf  25863  dvcof  25869  dvmptres3  25877  dvmptres2  25883  dvmptcmul  25885  dvmptcj  25889  dvcnvlem  25897  dvcnv  25898  dvcnvrelem1  25939  dvcnvrelem2  25940  plyrem  26230  ulmss  26323  ulmdvlem1  26326  ulmdvlem3  26328  ulmdv  26329  isppw  27041  dchrelbas2  27165  chsupsn  31376  pjss1coi  32126  off2  32603  elrgspnsubrunlem2  33207  elrspunidl  33384  evl1deg2  33531  submatres  33792  madjusmdetlem2  33814  madjusmdetlem3  33815  omsmon  34285  signstfvn  34556  elmsta  35540  mthmpps  35574  dissneqlem  37333  exrecfnlem  37372  prjcrv0  42626  hbtlem6  43122  ofoaf  43348  dvmulcncf  45926  dvdivcncf  45928  itgsubsticclem  45976