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

Theorem eqsstrrdi 3998
Description: A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017.)
Hypotheses
Ref Expression
eqsstrrdi.1 (𝜑𝐵 = 𝐴)
eqsstrrdi.2 𝐵𝐶
Assertion
Ref Expression
eqsstrrdi (𝜑𝐴𝐶)

Proof of Theorem eqsstrrdi
StepHypRef Expression
1 eqsstrrdi.1 . . 3 (𝜑𝐵 = 𝐴)
21eqcomd 2827 . 2 (𝜑𝐴 = 𝐵)
3 eqsstrrdi.2 . 2 𝐵𝐶
42, 3eqsstrdi 3997 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wss 3910
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-12 2178  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-v 3473  df-in 3917  df-ss 3927
This theorem is referenced by:  mptss  5883  ffvresb  6861  tposss  7868  sbthlem5  8607  rankxpl  9280  winafp  10096  wunex2  10137  iooval2  12749  telfsumo  15136  structcnvcnv  16475  ressbasss  16534  tsrdir  17826  idresefmnd  18042  idrespermg  18517  symgsssg  18573  gsumzoppg  19042  opsrtoslem2  20240  dsmmsubg  20862  cnclsi  21855  txss12  22188  txbasval  22189  kqsat  22314  kqcldsat  22316  fmss  22529  cfilucfil  23144  tngtopn  23234  dvaddf  24523  dvmulf  24524  dvcof  24529  dvmptres3  24537  dvmptres2  24543  dvmptcmul  24545  dvmptcj  24549  dvcnvlem  24557  dvcnv  24558  dvcnvrelem1  24598  dvcnvrelem2  24599  plyrem  24879  ulmss  24970  ulmdvlem1  24973  ulmdvlem3  24975  ulmdv  24976  isppw  25677  dchrelbas2  25799  chsupsn  29174  pjss1coi  29924  off2  30374  resspos  30632  resstos  30633  submomnd  30718  suborng  30895  submatres  31081  madjusmdetlem2  31103  madjusmdetlem3  31104  omsmon  31563  signstfvn  31846  elmsta  32802  mthmpps  32836  dissneqlem  34639  exrecfnlem  34678  hbtlem6  39870  dvmulcncf  42360  dvdivcncf  42362  itgsubsticclem  42410  lidlssbas  44340
  Copyright terms: Public domain W3C validator