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

Theorem 3sstr3d 3551
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 3538 . 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 1379    C_ wss 3481
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3488  df-ss 3495
This theorem is referenced by:  cnvtsr  15725  dprdss  16946  dprd2da  16961  dmdprdsplit2lem  16964  mplind  18035  txcmplem1  20008  setsmstopn  20847  tngtopn  21030  bcthlem2  21630  bcthlem4  21632  uniiccvol  21855  dyadmaxlem  21872  dvlip2  22262  dvne0  22278  shlej2  26110  hauseqcn  27709  bnd2lem  30221  heiborlem8  30248  hbtlem5  31011  dochord  36573  lclkrlem2p  36725  mapdsn  36844
  Copyright terms: Public domain W3C validator