Theorem eqsstrrdi 3968

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

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

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 2709

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

This theorem is referenced by:  eqimsscd  3980  mptss  6001  ffvresb  7072  tposss  8170  sbthlem5  9022  rankxpl  9790  winafp  10611  wunex2  10652  iooval2  13322  telfsumo  15756  structcnvcnv  17114  ressbasssg  17198  ressbasssOLD  17201  resspos  18386  resstos  18387  tsrdir  18561  idresefmnd  18858  idrespermg  19377  symgsssg  19433  gsumzoppg  19910  submomnd  20098  suborng  20844  lidlssbas  21203  dsmmsubg  21733  cnclsi  23247  txss12  23580  txbasval  23581  kqsat  23706  kqcldsat  23708  fmss  23921  cfilucfil  24534  tngtopn  24625  dvaddf  25919  dvmulf  25920  dvcof  25925  dvmptres3  25933  dvmptres2  25939  dvmptcmul  25941  dvmptcj  25945  dvcnvlem  25953  dvcnv  25954  dvcnvrelem1  25994  dvcnvrelem2  25995  plyrem  26282  ulmss  26375  ulmdvlem1  26378  ulmdvlem3  26380  ulmdv  26381  isppw  27091  dchrelbas2  27214  chsupsn  31499  pjss1coi  32249  off2  32729  padct  32806  elrgspnsubrunlem2  33324  elrspunidl  33503  evl1deg2  33652  submatres  33966  madjusmdetlem2  33988  madjusmdetlem3  33989  omsmon  34458  signstfvn  34729  elmsta  35746  mthmpps  35780  dissneqlem  37670  exrecfnlem  37709  prjcrv0  43080  hbtlem6  43575  ofoaf  43801  dvmulcncf  46371  dvdivcncf  46373  itgsubsticclem  46421