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

Theorem 3sstr3d 3680
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 3667 . 2 (𝜑 → (𝐴𝐵𝐶𝐷))
51, 4mpbid 222 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621
This theorem is referenced by:  cnvtsr  17269  dprdss  18474  dprd2da  18487  dmdprdsplit2lem  18490  mplind  19550  txcmplem1  21492  setsmstopn  22330  tngtopn  22501  bcthlem2  23168  bcthlem4  23170  uniiccvol  23394  dyadmaxlem  23411  dvlip2  23803  dvne0  23819  shlej2  28348  hauseqcn  30069  bnd2lem  33720  heiborlem8  33747  dochord  36976  lclkrlem2p  37128  mapdsn  37247  hbtlem5  38015  fvmptiunrelexplb0d  38293  fvmptiunrelexplb1d  38295
  Copyright terms: Public domain W3C validator