Theorem eqsstrrdi 4037

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3955  df-ss 3965

This theorem is referenced by:  eqimsscd  4039  mptss  6042  ffvresb  7126  tposss  8216  sbthlem5  9091  rankxpl  9874  winafp  10696  wunex2  10737  iooval2  13362  telfsumo  15753  structcnvcnv  17091  ressbasssg  17186  ressbasssOLD  17189  tsrdir  18562  idresefmnd  18817  idrespermg  19321  symgsssg  19377  gsumzoppg  19854  lidlssbas  20980  dsmmsubg  21518  opsrtoslem2  21837  cnclsi  22997  txss12  23330  txbasval  23331  kqsat  23456  kqcldsat  23458  fmss  23671  cfilucfil  24289  tngtopn  24388  dvaddf  25694  dvmulf  25695  dvcof  25701  dvmptres3  25709  dvmptres2  25715  dvmptcmul  25717  dvmptcj  25721  dvcnvlem  25729  dvcnv  25730  dvcnvrelem1  25770  dvcnvrelem2  25771  plyrem  26055  ulmss  26146  ulmdvlem1  26149  ulmdvlem3  26151  ulmdv  26152  isppw  26855  dchrelbas2  26977  chsupsn  30934  pjss1coi  31684  off2  32134  resspos  32404  resstos  32405  submomnd  32499  suborng  32704  elrspunidl  32821  submatres  33085  madjusmdetlem2  33107  madjusmdetlem3  33108  omsmon  33596  signstfvn  33879  elmsta  34838  mthmpps  34872  dissneqlem  36525  exrecfnlem  36564  prjcrv0  41678  hbtlem6  42174  ofoaf  42408  dvmulcncf  44940  dvdivcncf  44942  itgsubsticclem  44990