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

Theorem 3sstr3d 3995
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.1 . 2 (𝜑𝐴𝐵)
2 3sstr3d.2 . . 3 (𝜑𝐴 = 𝐶)
3 3sstr3d.3 . . 3 (𝜑𝐵 = 𝐷)
42, 3sseq12d 3982 . 2 (𝜑 → (𝐴𝐵𝐶𝐷))
51, 4mpbid 231 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wss 3915
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-in 3922  df-ss 3932
This theorem is referenced by:  cnvtsr  18484  dprdss  19815  dprd2da  19828  dmdprdsplit2lem  19831  mplind  21494  txcmplem1  23008  setsmstopn  23849  tngtopn  24030  bcthlem2  24705  bcthlem4  24707  uniiccvol  24960  dyadmaxlem  24977  dvlip2  25375  dvne0  25391  shlej2  30345  gsumzresunsn  31938  pmtrcnel2  31983  cyc3co2  32031  fedgmullem1  32364  hauseqcn  32519  bnd2lem  36279  heiborlem8  36306  dochord  39862  lclkrlem2p  40014  mapdsn  40133  hbtlem5  41484  oaabsb  41658  omabs2  41696  fvmptiunrelexplb0d  42030  fvmptiunrelexplb1d  42032  ovolval5lem3  44969  isclatd  47082
  Copyright terms: Public domain W3C validator