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 3434  df-in 3894  df-ss 3904

This theorem is referenced by:  mptss  5950  ffvresb  6998  tposss  8043  sbthlem5  8874  rankxpl  9633  winafp  10453  wunex2  10494  iooval2  13112  telfsumo  15514  structcnvcnv  16854  ressbasss  16950  tsrdir  18322  idresefmnd  18538  idrespermg  19019  symgsssg  19075  gsumzoppg  19545  dsmmsubg  20950  opsrtoslem2  21263  cnclsi  22423  txss12  22756  txbasval  22757  kqsat  22882  kqcldsat  22884  fmss  23097  cfilucfil  23715  tngtopn  23814  dvaddf  25106  dvmulf  25107  dvcof  25112  dvmptres3  25120  dvmptres2  25126  dvmptcmul  25128  dvmptcj  25132  dvcnvlem  25140  dvcnv  25141  dvcnvrelem1  25181  dvcnvrelem2  25182  plyrem  25465  ulmss  25556  ulmdvlem1  25559  ulmdvlem3  25561  ulmdv  25562  isppw  26263  dchrelbas2  26385  chsupsn  29775  pjss1coi  30525  off2  30978  resspos  31244  resstos  31245  submomnd  31336  suborng  31514  elrspunidl  31606  submatres  31756  madjusmdetlem2  31778  madjusmdetlem3  31779  omsmon  32265  signstfvn  32548  elmsta  33510  mthmpps  33544  dissneqlem  35511  exrecfnlem  35550  prjcrv0  40470  hbtlem6  40954  dvmulcncf  43466  dvdivcncf  43468  itgsubsticclem  43516  lidlssbas  45480