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

Theorem 3sstr3d 3410
Description: Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 1-Oct-2000.)
Hypotheses
Ref Expression
3sstr3d.1  |-  ( ph  ->  A  C_  B )
3sstr3d.2  |-  ( ph  ->  A  =  C )
3sstr3d.3  |-  ( ph  ->  B  =  D )
Assertion
Ref Expression
3sstr3d  |-  ( ph  ->  C  C_  D )

Proof of Theorem 3sstr3d
StepHypRef Expression
1 3sstr3d.1 . 2  |-  ( ph  ->  A  C_  B )
2 3sstr3d.2 . . 3  |-  ( ph  ->  A  =  C )
3 3sstr3d.3 . . 3  |-  ( ph  ->  B  =  D )
42, 3sseq12d 3397 . 2  |-  ( ph  ->  ( A  C_  B  <->  C 
C_  D ) )
51, 4mpbid 210 1  |-  ( ph  ->  C  C_  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    C_ wss 3340
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3347  df-ss 3354
This theorem is referenced by:  cnvtsr  15404  dprdss  16538  dprd2da  16553  dmdprdsplit2lem  16556  mplind  17596  txcmplem1  19226  setsmstopn  20065  tngtopn  20248  bcthlem2  20848  bcthlem4  20850  uniiccvol  21072  dyadmaxlem  21089  dvlip2  21479  dvne0  21495  shlej2  24776  hauseqcn  26337  bnd2lem  28702  heiborlem8  28729  hbtlem5  29496  dochord  35027  lclkrlem2p  35179  mapdsn  35298
  Copyright terms: Public domain W3C validator