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

Theorem 3sstr3d 4038
Description: Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 1-Oct-2000.)
Hypotheses
Ref Expression
3sstr3d.1 (𝜑𝐴𝐵)
3sstr3d.2 (𝜑𝐴 = 𝐶)
3sstr3d.3 (𝜑𝐵 = 𝐷)
Assertion
Ref Expression
3sstr3d (𝜑𝐶𝐷)

Proof of Theorem 3sstr3d
StepHypRef Expression
1 3sstr3d.2 . . 3 (𝜑𝐴 = 𝐶)
2 3sstr3d.1 . . 3 (𝜑𝐴𝐵)
31, 2eqsstrrd 4019 . 2 (𝜑𝐶𝐵)
4 3sstr3d.3 . 2 (𝜑𝐵 = 𝐷)
53, 4sseqtrd 4020 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1540  wss 3951
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ss 3968
This theorem is referenced by:  cnvtsr  18633  dprdss  20049  dprd2da  20062  dmdprdsplit2lem  20065  mplind  22094  txcmplem1  23649  setsmstopn  24490  tngtopn  24671  bcthlem2  25359  bcthlem4  25361  uniiccvol  25615  dyadmaxlem  25632  dvlip2  26034  dvne0  26050  shlej2  31380  gsumzresunsn  33059  pmtrcnel2  33110  cyc3co2  33160  ssdifidllem  33484  fedgmullem1  33680  hauseqcn  33897  bnd2lem  37798  heiborlem8  37825  dochord  41372  lclkrlem2p  41524  mapdsn  41643  hbtlem5  43140  oaabsb  43307  omabs2  43345  fvmptiunrelexplb0d  43697  fvmptiunrelexplb1d  43699  ovolval5lem3  46669  isclatd  48872
  Copyright terms: Public domain W3C validator