Theorem eqsstrrdi 3967

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3889

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ss 3906

This theorem is referenced by:  eqimsscd  3979  mptss  6007  ffvresb  7078  tposss  8177  sbthlem5  9029  rankxpl  9799  winafp  10620  wunex2  10661  iooval2  13331  telfsumo  15765  structcnvcnv  17123  ressbasssg  17207  ressbasssOLD  17210  resspos  18395  resstos  18396  tsrdir  18570  idresefmnd  18867  idrespermg  19386  symgsssg  19442  gsumzoppg  19919  submomnd  20107  suborng  20853  lidlssbas  21211  dsmmsubg  21723  cnclsi  23237  txss12  23570  txbasval  23571  kqsat  23696  kqcldsat  23698  fmss  23911  cfilucfil  24524  tngtopn  24615  dvaddf  25909  dvmulf  25910  dvcof  25915  dvmptres3  25923  dvmptres2  25929  dvmptcmul  25931  dvmptcj  25935  dvcnvlem  25943  dvcnv  25944  dvcnvrelem1  25984  dvcnvrelem2  25985  plyrem  26271  ulmss  26362  ulmdvlem1  26365  ulmdvlem3  26367  ulmdv  26368  isppw  27077  dchrelbas2  27200  chsupsn  31484  pjss1coi  32234  off2  32714  padct  32791  elrgspnsubrunlem2  33309  elrspunidl  33488  evl1deg2  33637  submatres  33950  madjusmdetlem2  33972  madjusmdetlem3  33973  omsmon  34442  signstfvn  34713  elmsta  35730  mthmpps  35764  dissneqlem  37656  exrecfnlem  37695  prjcrv0  43066  hbtlem6  43557  ofoaf  43783  dvmulcncf  46353  dvdivcncf  46355  itgsubsticclem  46403