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

Theorem syl6eqssr 3648
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 2626 . 2 (𝜑𝐴 = 𝐵)
3 syl6eqssr.2 . 2 𝐵𝐶
42, 3syl6eqss 3647 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1481  wss 3567
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-in 3574  df-ss 3581
This theorem is referenced by:  mptss  5442  ffvresb  6380  tposss  7338  sbthlem5  8059  rankxpl  8723  winafp  9504  wunex2  9545  iooval2  12193  telfsumo  14515  structcnvcnv  15852  ressbasss  15913  tsrdir  17219  idrespermg  17812  symgsssg  17868  gsumzoppg  18325  opsrtoslem2  19466  dsmmsubg  20068  cnclsi  21057  txss12  21389  txbasval  21390  kqsat  21515  kqcldsat  21517  fmss  21731  cfilucfil  22345  tngtopn  22435  dvaddf  23686  dvmulf  23687  dvcof  23692  dvmptres3  23700  dvmptres2  23706  dvmptcmul  23708  dvmptcj  23712  dvcnvlem  23720  dvcnv  23721  dvcnvrelem1  23761  dvcnvrelem2  23762  plyrem  24041  ulmss  24132  ulmdvlem1  24135  ulmdvlem3  24137  ulmdv  24138  isppw  24821  dchrelbas2  24943  chsupsn  28242  pjss1coi  28992  off2  29416  resspos  29633  resstos  29634  submomnd  29684  suborng  29789  submatres  29846  madjusmdetlem2  29868  madjusmdetlem3  29869  omsmon  30334  signstfvn  30620  elmsta  31419  mthmpps  31453  dissneqlem  33158  hbtlem6  37518  dvmulcncf  39903  dvdivcncf  39905  itgsubsticclem  39954  lidlssbas  41687
  Copyright terms: Public domain W3C validator