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

Theorem 3sstr3d 3610
 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 3597 . 2 (𝜑 → (𝐴𝐵𝐶𝐷))
51, 4mpbid 221 1 (𝜑𝐶𝐷)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1475   ⊆ wss 3540 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554 This theorem is referenced by:  cnvtsr  17045  dprdss  18251  dprd2da  18264  dmdprdsplit2lem  18267  mplind  19323  txcmplem1  21254  setsmstopn  22093  tngtopn  22264  bcthlem2  22930  bcthlem4  22932  uniiccvol  23154  dyadmaxlem  23171  dvlip2  23562  dvne0  23578  shlej2  27604  hauseqcn  29269  bnd2lem  32760  heiborlem8  32787  dochord  35677  lclkrlem2p  35829  mapdsn  35948  hbtlem5  36717  fvmptiunrelexplb0d  36995  fvmptiunrelexplb1d  36997  usgrumgruspgr  40410
 Copyright terms: Public domain W3C validator