Theorem eqsstrrdi 4022

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

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952

This theorem is referenced by:  mptss  5910  ffvresb  6888  tposss  7893  sbthlem5  8631  rankxpl  9304  winafp  10119  wunex2  10160  iooval2  12772  telfsumo  15157  structcnvcnv  16497  ressbasss  16556  tsrdir  17848  idresefmnd  18064  idrespermg  18539  symgsssg  18595  gsumzoppg  19064  opsrtoslem2  20265  dsmmsubg  20887  cnclsi  21880  txss12  22213  txbasval  22214  kqsat  22339  kqcldsat  22341  fmss  22554  cfilucfil  23169  tngtopn  23259  dvaddf  24539  dvmulf  24540  dvcof  24545  dvmptres3  24553  dvmptres2  24559  dvmptcmul  24561  dvmptcj  24565  dvcnvlem  24573  dvcnv  24574  dvcnvrelem1  24614  dvcnvrelem2  24615  plyrem  24894  ulmss  24985  ulmdvlem1  24988  ulmdvlem3  24990  ulmdv  24991  isppw  25691  dchrelbas2  25813  chsupsn  29190  pjss1coi  29940  off2  30388  resspos  30646  resstos  30647  submomnd  30711  suborng  30888  submatres  31071  madjusmdetlem2  31093  madjusmdetlem3  31094  omsmon  31556  signstfvn  31839  elmsta  32795  mthmpps  32829  dissneqlem  34624  exrecfnlem  34663  hbtlem6  39778  dvmulcncf  42259  dvdivcncf  42261  itgsubsticclem  42309  lidlssbas  44242