Theorem eqsstrrdi 3976

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

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3432  df-in 3894  df-ss 3904

This theorem is referenced by:  mptss  5944  ffvresb  6991  tposss  8031  sbthlem5  8862  rankxpl  9621  winafp  10441  wunex2  10482  iooval2  13100  telfsumo  15502  structcnvcnv  16842  ressbasss  16938  tsrdir  18310  idresefmnd  18526  idrespermg  19007  symgsssg  19063  gsumzoppg  19533  dsmmsubg  20938  opsrtoslem2  21251  cnclsi  22411  txss12  22744  txbasval  22745  kqsat  22870  kqcldsat  22872  fmss  23085  cfilucfil  23703  tngtopn  23802  dvaddf  25094  dvmulf  25095  dvcof  25100  dvmptres3  25108  dvmptres2  25114  dvmptcmul  25116  dvmptcj  25120  dvcnvlem  25128  dvcnv  25129  dvcnvrelem1  25169  dvcnvrelem2  25170  plyrem  25453  ulmss  25544  ulmdvlem1  25547  ulmdvlem3  25549  ulmdv  25550  isppw  26251  dchrelbas2  26373  chsupsn  29761  pjss1coi  30511  off2  30964  resspos  31230  resstos  31231  submomnd  31322  suborng  31500  elrspunidl  31592  submatres  31742  madjusmdetlem2  31764  madjusmdetlem3  31765  omsmon  32251  signstfvn  32534  elmsta  33496  mthmpps  33530  dissneqlem  35497  exrecfnlem  35536  prjcrv0  40456  hbtlem6  40940  dvmulcncf  43425  dvdivcncf  43427  itgsubsticclem  43475  lidlssbas  45436