Theorem eqsstrrdi 3972

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

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  mptss  5939  ffvresb  6980  tposss  8014  sbthlem5  8827  rankxpl  9564  winafp  10384  wunex2  10425  iooval2  13041  telfsumo  15442  structcnvcnv  16782  ressbasss  16876  tsrdir  18237  idresefmnd  18453  idrespermg  18934  symgsssg  18990  gsumzoppg  19460  dsmmsubg  20860  opsrtoslem2  21173  cnclsi  22331  txss12  22664  txbasval  22665  kqsat  22790  kqcldsat  22792  fmss  23005  cfilucfil  23621  tngtopn  23720  dvaddf  25011  dvmulf  25012  dvcof  25017  dvmptres3  25025  dvmptres2  25031  dvmptcmul  25033  dvmptcj  25037  dvcnvlem  25045  dvcnv  25046  dvcnvrelem1  25086  dvcnvrelem2  25087  plyrem  25370  ulmss  25461  ulmdvlem1  25464  ulmdvlem3  25466  ulmdv  25467  isppw  26168  dchrelbas2  26290  chsupsn  29676  pjss1coi  30426  off2  30879  resspos  31146  resstos  31147  submomnd  31238  suborng  31416  elrspunidl  31508  submatres  31658  madjusmdetlem2  31680  madjusmdetlem3  31681  omsmon  32165  signstfvn  32448  elmsta  33410  mthmpps  33444  dissneqlem  35438  exrecfnlem  35477  hbtlem6  40870  dvmulcncf  43356  dvdivcncf  43358  itgsubsticclem  43406  lidlssbas  45368