Theorem eqsstrrdi 3983

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-ss 3923

This theorem is used by:  eqimsscd  3995  mptss  6046  ffvresb  7125  tposss  8229  sbthlem5  9086  rankxpl  9854  winafp  10697  wunex2  10738  iooval2  13421  telfsumo  15877  structcnvcnv  17235  ressbasssg  17319  ressbasssOLD  17322  resspos  18507  resstos  18508  tsrdir  18682  idresefmnd  18995  idrespermg  19525  symgsssg  19581  gsumzoppg  20058  submomnd  20246  suborng  21029  lidlssbas  21388  dsmmsubg  21943  cnclsi  23479  txss12  23813  txbasval  23814  kqsat  23939  kqcldsat  23941  fmss  24154  cfilucfil  24767  tngtopn  24858  dvaddf  26152  dvmulf  26153  dvcof  26158  dvmptres3  26166  dvmptres2  26172  dvmptcmul  26174  dvmptcj  26178  dvcnvlem  26186  dvcnv  26187  dvcnvrelem1  26227  dvcnvrelem2  26228  plyrem  26517  ulmss  26611  ulmdvlem1  26614  ulmdvlem3  26616  ulmdv  26617  isppw  27329  dchrelbas2  27452  chsupsn  31836  pjss1coi  32586  off2  33057  padct  33133  elrgspnsubrunlem2  33632  elrspunidl  33800  evl1deg2  33931  submatres  34260  madjusmdetlem2  34282  madjusmdetlem3  34283  omsmon  34753  signstfvn  35021  elmsta  36077  mthmpps  36111  dissneqlem  38043  exrecfnlem  38082  prjcrv0  43423  hbtlem6  43914  ofoaf  44140  dvmulcncf  46697  dvdivcncf  46699  itgsubsticclem  46747