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

Theorem 3sstr3d 3962
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 3949 . 2 (𝜑 → (𝐴𝐵𝐶𝐷))
51, 4mpbid 235 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1543  wss 3881
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-ext 2709
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2072  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3423  df-in 3888  df-ss 3898
This theorem is referenced by:  cnvtsr  18119  dprdss  19441  dprd2da  19454  dmdprdsplit2lem  19457  mplind  21052  txcmplem1  22562  setsmstopn  23400  tngtopn  23572  bcthlem2  24246  bcthlem4  24248  uniiccvol  24501  dyadmaxlem  24518  dvlip2  24916  dvne0  24932  shlej2  29466  gsumzresunsn  31057  pmtrcnel2  31102  cyc3co2  31150  fedgmullem1  31448  hauseqcn  31586  bnd2lem  35713  heiborlem8  35740  dochord  39148  lclkrlem2p  39300  mapdsn  39419  hbtlem5  40685  fvmptiunrelexplb0d  40998  fvmptiunrelexplb1d  41000  isclatd  45971
  Copyright terms: Public domain W3C validator