Theorem eqsstrrdi 4002

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 4001	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3913

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930

This theorem is referenced by:  eqimsscd  4004  mptss  6001  ffvresb  7077  tposss  8163  sbthlem5  9038  rankxpl  9820  winafp  10642  wunex2  10683  iooval2  13307  telfsumo  15698  structcnvcnv  17036  ressbasssg  17131  ressbasssOLD  17134  tsrdir  18507  idresefmnd  18723  idrespermg  19207  symgsssg  19263  gsumzoppg  19735  dsmmsubg  21186  opsrtoslem2  21500  cnclsi  22660  txss12  22993  txbasval  22994  kqsat  23119  kqcldsat  23121  fmss  23334  cfilucfil  23952  tngtopn  24051  dvaddf  25343  dvmulf  25344  dvcof  25349  dvmptres3  25357  dvmptres2  25363  dvmptcmul  25365  dvmptcj  25369  dvcnvlem  25377  dvcnv  25378  dvcnvrelem1  25418  dvcnvrelem2  25419  plyrem  25702  ulmss  25793  ulmdvlem1  25796  ulmdvlem3  25798  ulmdv  25799  isppw  26500  dchrelbas2  26622  chsupsn  30418  pjss1coi  31168  off2  31624  resspos  31896  resstos  31897  submomnd  31988  suborng  32181  elrspunidl  32279  submatres  32476  madjusmdetlem2  32498  madjusmdetlem3  32499  omsmon  32987  signstfvn  33270  elmsta  34229  mthmpps  34263  dissneqlem  35884  exrecfnlem  35923  prjcrv0  41029  hbtlem6  41514  ofoaf  41748  dvmulcncf  44286  dvdivcncf  44288  itgsubsticclem  44336  lidlssbas  46340