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

Theorem 3sstr3d 3631
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 3618 . 2 (𝜑 → (𝐴𝐵𝐶𝐷))
51, 4mpbid 222 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  wss 3560
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-in 3567  df-ss 3574
This theorem is referenced by:  cnvtsr  17138  dprdss  18344  dprd2da  18357  dmdprdsplit2lem  18360  mplind  19416  txcmplem1  21349  setsmstopn  22188  tngtopn  22359  bcthlem2  23025  bcthlem4  23027  uniiccvol  23249  dyadmaxlem  23266  dvlip2  23657  dvne0  23673  usgrumgruspgr  25962  shlej2  28060  hauseqcn  29715  bnd2lem  33189  heiborlem8  33216  dochord  36106  lclkrlem2p  36258  mapdsn  36377  hbtlem5  37146  fvmptiunrelexplb0d  37424  fvmptiunrelexplb1d  37426
  Copyright terms: Public domain W3C validator