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

Theorem syl6eqssr 3797
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 2766 . 2 (𝜑𝐴 = 𝐵)
3 syl6eqssr.2 . 2 𝐵𝐶
42, 3syl6eqss 3796 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  wss 3715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-in 3722  df-ss 3729
This theorem is referenced by:  mptss  5612  ffvresb  6558  tposss  7523  sbthlem5  8241  rankxpl  8913  winafp  9731  wunex2  9772  iooval2  12421  telfsumo  14753  structcnvcnv  16093  ressbasss  16154  tsrdir  17459  idrespermg  18051  symgsssg  18107  gsumzoppg  18564  opsrtoslem2  19707  dsmmsubg  20309  cnclsi  21298  txss12  21630  txbasval  21631  kqsat  21756  kqcldsat  21758  fmss  21971  cfilucfil  22585  tngtopn  22675  dvaddf  23924  dvmulf  23925  dvcof  23930  dvmptres3  23938  dvmptres2  23944  dvmptcmul  23946  dvmptcj  23950  dvcnvlem  23958  dvcnv  23959  dvcnvrelem1  23999  dvcnvrelem2  24000  plyrem  24279  ulmss  24370  ulmdvlem1  24373  ulmdvlem3  24375  ulmdv  24376  isppw  25060  dchrelbas2  25182  chsupsn  28602  pjss1coi  29352  off2  29773  resspos  29989  resstos  29990  submomnd  30040  suborng  30145  submatres  30202  madjusmdetlem2  30224  madjusmdetlem3  30225  omsmon  30690  signstfvn  30976  elmsta  31773  mthmpps  31807  dissneqlem  33516  hbtlem6  38219  dvmulcncf  40661  dvdivcncf  40663  itgsubsticclem  40712  lidlssbas  42450
  Copyright terms: Public domain W3C validator