Theorem eqsstrrdi 3979

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

Syntax hints:   → wi 4   = wceq 1559   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ss 3919

This theorem is referenced by:  eqimsscd  3991  mptss  6027  ffvresb  7102  tposss  8201  sbthlem5  9057  rankxpl  9827  winafp  10649  wunex2  10690  iooval2  13376  telfsumo  15821  structcnvcnv  17180  ressbasssg  17264  ressbasssOLD  17267  resspos  18452  resstos  18453  tsrdir  18627  idresefmnd  18924  idrespermg  19442  symgsssg  19498  gsumzoppg  19975  submomnd  20163  suborng  20913  lidlssbas  21271  dsmmsubg  21783  cnclsi  23320  txss12  23653  txbasval  23654  kqsat  23779  kqcldsat  23781  fmss  23994  cfilucfil  24607  tngtopn  24698  dvaddf  25992  dvmulf  25993  dvcof  25998  dvmptres3  26006  dvmptres2  26012  dvmptcmul  26014  dvmptcj  26018  dvcnvlem  26026  dvcnv  26027  dvcnvrelem1  26067  dvcnvrelem2  26068  plyrem  26357  ulmss  26448  ulmdvlem1  26451  ulmdvlem3  26453  ulmdv  26454  isppw  27166  dchrelbas2  27289  chsupsn  31573  pjss1coi  32323  off2  32804  padct  32881  elrgspnsubrunlem2  33390  elrspunidl  33575  evl1deg2  33734  submatres  34064  madjusmdetlem2  34086  madjusmdetlem3  34087  omsmon  34556  signstfvn  34824  elmsta  35859  mthmpps  35893  dissneqlem  37795  exrecfnlem  37834  prjcrv0  43176  hbtlem6  43667  ofoaf  43893  dvmulcncf  46460  dvdivcncf  46462  itgsubsticclem  46510