Theorem eqsstrrdi 4032

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

Syntax hints:   → wi 4   = wceq 1533   ⊆ wss 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717  df-ss 3961

This theorem is referenced by:  eqimsscd  4034  mptss  6047  ffvresb  7134  tposss  8233  sbthlem5  9112  rankxpl  9900  winafp  10722  wunex2  10763  iooval2  13392  telfsumo  15784  structcnvcnv  17125  ressbasssg  17220  ressbasssOLD  17223  tsrdir  18599  idresefmnd  18859  idrespermg  19378  symgsssg  19434  gsumzoppg  19911  lidlssbas  21121  dsmmsubg  21694  opsrtoslem2  22022  cnclsi  23220  txss12  23553  txbasval  23554  kqsat  23679  kqcldsat  23681  fmss  23894  cfilucfil  24512  tngtopn  24611  dvaddf  25917  dvmulf  25918  dvcof  25924  dvmptres3  25932  dvmptres2  25938  dvmptcmul  25940  dvmptcj  25944  dvcnvlem  25952  dvcnv  25953  dvcnvrelem1  25994  dvcnvrelem2  25995  plyrem  26285  ulmss  26378  ulmdvlem1  26381  ulmdvlem3  26383  ulmdv  26384  isppw  27091  dchrelbas2  27215  chsupsn  31295  pjss1coi  32045  off2  32508  resspos  32782  resstos  32783  submomnd  32880  suborng  33129  elrspunidl  33240  submatres  33538  madjusmdetlem2  33560  madjusmdetlem3  33561  omsmon  34049  signstfvn  34332  elmsta  35289  mthmpps  35323  dissneqlem  36950  exrecfnlem  36989  prjcrv0  42192  hbtlem6  42695  ofoaf  42926  dvmulcncf  45451  dvdivcncf  45453  itgsubsticclem  45501