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

Theorem 3sstr3d 3796
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 3783 . 2 (𝜑 → (𝐴𝐵𝐶𝐷))
51, 4mpbid 222 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1631  wss 3723
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-in 3730  df-ss 3737
This theorem is referenced by:  cnvtsr  17430  dprdss  18636  dprd2da  18649  dmdprdsplit2lem  18652  mplind  19717  txcmplem1  21665  setsmstopn  22503  tngtopn  22674  bcthlem2  23341  bcthlem4  23343  uniiccvol  23568  dyadmaxlem  23585  dvlip2  23978  dvne0  23994  shlej2  28560  hauseqcn  30281  bnd2lem  33922  heiborlem8  33949  dochord  37180  lclkrlem2p  37332  mapdsn  37451  hbtlem5  38224  fvmptiunrelexplb0d  38502  fvmptiunrelexplb1d  38504
  Copyright terms: Public domain W3C validator