Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl6eqssr Structured version   Visualization version   GIF version

Theorem syl6eqssr 3852
 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
StepHypRef Expression
1 syl6eqssr.1 . . 3 (𝜑𝐵 = 𝐴)
21eqcomd 2805 . 2 (𝜑𝐴 = 𝐵)
3 syl6eqssr.2 . 2 𝐵𝐶
42, 3syl6eqss 3851 1 (𝜑𝐴𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1653   ⊆ wss 3769 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777 This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-in 3776  df-ss 3783 This theorem is referenced by:  mptss  5666  ffvresb  6620  tposss  7591  sbthlem5  8316  rankxpl  8988  winafp  9807  wunex2  9848  iooval2  12457  telfsumo  14872  structcnvcnv  16198  ressbasss  16257  tsrdir  17553  idrespermg  18143  symgsssg  18199  gsumzoppg  18659  opsrtoslem2  19807  dsmmsubg  20412  cnclsi  21405  txss12  21737  txbasval  21738  kqsat  21863  kqcldsat  21865  fmss  22078  cfilucfil  22692  tngtopn  22782  dvaddf  24046  dvmulf  24047  dvcof  24052  dvmptres3  24060  dvmptres2  24066  dvmptcmul  24068  dvmptcj  24072  dvcnvlem  24080  dvcnv  24081  dvcnvrelem1  24121  dvcnvrelem2  24122  plyrem  24401  ulmss  24492  ulmdvlem1  24495  ulmdvlem3  24497  ulmdv  24498  isppw  25192  dchrelbas2  25314  chsupsn  28797  pjss1coi  29547  off2  29962  resspos  30175  resstos  30176  submomnd  30226  suborng  30331  submatres  30388  madjusmdetlem2  30410  madjusmdetlem3  30411  omsmon  30876  signstfvn  31164  elmsta  31962  mthmpps  31996  dissneqlem  33686  hbtlem6  38484  dvmulcncf  40884  dvdivcncf  40886  itgsubsticclem  40934  lidlssbas  42721
 Copyright terms: Public domain W3C validator