Theorem eqsstrrdi 3990

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ss 3930

This theorem is referenced by:  eqimsscd  4002  mptss  6042  ffvresb  7119  tposss  8219  sbthlem5  9075  rankxpl  9843  winafp  10678  wunex2  10719  iooval2  13401  telfsumo  15850  structcnvcnv  17209  ressbasssg  17293  ressbasssOLD  17296  resspos  18481  resstos  18482  tsrdir  18656  idresefmnd  18954  idrespermg  19477  symgsssg  19533  gsumzoppg  20010  submomnd  20198  suborng  20953  lidlssbas  21312  dsmmsubg  21858  cnclsi  23394  txss12  23727  txbasval  23728  kqsat  23853  kqcldsat  23855  fmss  24068  cfilucfil  24681  tngtopn  24772  dvaddf  26066  dvmulf  26067  dvcof  26072  dvmptres3  26080  dvmptres2  26086  dvmptcmul  26088  dvmptcj  26092  dvcnvlem  26100  dvcnv  26101  dvcnvrelem1  26141  dvcnvrelem2  26142  plyrem  26431  ulmss  26522  ulmdvlem1  26525  ulmdvlem3  26527  ulmdv  26528  isppw  27240  dchrelbas2  27363  chsupsn  31702  pjss1coi  32452  off2  32923  padct  33000  elrgspnsubrunlem2  33505  elrspunidl  33676  evl1deg2  33808  submatres  34137  madjusmdetlem2  34159  madjusmdetlem3  34160  omsmon  34629  signstfvn  34897  elmsta  35935  mthmpps  35969  dissneqlem  37869  exrecfnlem  37908  prjcrv0  43252  hbtlem6  43743  ofoaf  43969  dvmulcncf  46526  dvdivcncf  46528  itgsubsticclem  46576