Theorem syl6eqssr 3619

Description: A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017.)

Hypotheses

Ref	Expression
syl6eqssr.1	⊢ (𝜑 → 𝐵 = 𝐴)
syl6eqssr.2	⊢ 𝐵 ⊆ 𝐶

Assertion

Ref	Expression
syl6eqssr	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem syl6eqssr

Step	Hyp	Ref	Expression
1		syl6eqssr.1	. . 3 ⊢ (𝜑 → 𝐵 = 𝐴)
2	1	eqcomd 2616	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3		syl6eqssr.2	. 2 ⊢ 𝐵 ⊆ 𝐶
4	2, 3	syl6eqss 3618	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1475   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554

This theorem is referenced by:  mptss  5373  ffvresb  6301  tposss  7240  sbthlem5  7959  rankxpl  8621  winafp  9398  wunex2  9439  iooval2  12079  telfsumo  14375  structcnvcnv  15706  ressbasss  15759  tsrdir  17061  idrespermg  17654  symgsssg  17710  gsumzoppg  18167  opsrtoslem2  19306  dsmmsubg  19906  cnclsi  20886  txss12  21218  txbasval  21219  kqsat  21344  kqcldsat  21346  fmss  21560  cfilucfil  22174  tngtopn  22264  dvaddf  23511  dvmulf  23512  dvcof  23517  dvmptres3  23525  dvmptres2  23531  dvmptcmul  23533  dvmptcj  23537  dvcnvlem  23543  dvcnv  23544  dvcnvrelem1  23584  dvcnvrelem2  23585  plyrem  23864  ulmss  23955  ulmdvlem1  23958  ulmdvlem3  23960  ulmdv  23961  isppw  24640  dchrelbas2  24762  chsupsn  27656  pjss1coi  28406  off2  28823  resspos  28990  resstos  28991  submomnd  29041  suborng  29146  submatres  29200  madjusmdetlem2  29222  madjusmdetlem3  29223  omsmon  29687  signstfvn  29972  elmsta  30699  mthmpps  30733  dissneqlem  32363  hbtlem6  36718  dvmulcncf  38815  dvdivcncf  38817  itgsubsticclem  38867  lidlssbas  41712