Theorem syl6eqssr 3656

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 2628	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3		syl6eqssr.2	. 2 ⊢ 𝐵 ⊆ 𝐶
4	2, 3	syl6eqss 3655	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1483   ⊆ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  mptss  5454  ffvresb  6394  tposss  7353  sbthlem5  8074  rankxpl  8738  winafp  9519  wunex2  9560  iooval2  12208  telfsumo  14534  structcnvcnv  15871  ressbasss  15932  tsrdir  17238  idrespermg  17831  symgsssg  17887  gsumzoppg  18344  opsrtoslem2  19485  dsmmsubg  20087  cnclsi  21076  txss12  21408  txbasval  21409  kqsat  21534  kqcldsat  21536  fmss  21750  cfilucfil  22364  tngtopn  22454  dvaddf  23705  dvmulf  23706  dvcof  23711  dvmptres3  23719  dvmptres2  23725  dvmptcmul  23727  dvmptcj  23731  dvcnvlem  23739  dvcnv  23740  dvcnvrelem1  23780  dvcnvrelem2  23781  plyrem  24060  ulmss  24151  ulmdvlem1  24154  ulmdvlem3  24156  ulmdv  24157  isppw  24840  dchrelbas2  24962  chsupsn  28272  pjss1coi  29022  off2  29443  resspos  29659  resstos  29660  submomnd  29710  suborng  29815  submatres  29872  madjusmdetlem2  29894  madjusmdetlem3  29895  omsmon  30360  signstfvn  30646  elmsta  31445  mthmpps  31479  dissneqlem  33187  hbtlem6  37699  dvmulcncf  40140  dvdivcncf  40142  itgsubsticclem  40191  lidlssbas  41922