ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3sstr4d GIF version

Theorem 3sstr4d 3108
Description: Substitution of equality into both sides of a subclass relationship. (Contributed by NM, 30-Nov-1995.) (Proof shortened by Eric Schmidt, 26-Jan-2007.)
Hypotheses
Ref Expression
3sstr4d.1 (𝜑𝐴𝐵)
3sstr4d.2 (𝜑𝐶 = 𝐴)
3sstr4d.3 (𝜑𝐷 = 𝐵)
Assertion
Ref Expression
3sstr4d (𝜑𝐶𝐷)

Proof of Theorem 3sstr4d
StepHypRef Expression
1 3sstr4d.1 . 2 (𝜑𝐴𝐵)
2 3sstr4d.2 . . 3 (𝜑𝐶 = 𝐴)
3 3sstr4d.3 . . 3 (𝜑𝐷 = 𝐵)
42, 3sseq12d 3094 . 2 (𝜑 → (𝐶𝐷𝐴𝐵))
51, 4mpbird 166 1 (𝜑𝐶𝐷)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1314  wss 3037
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-in 3043  df-ss 3050
This theorem is referenced by:  rdgss  6234  sucinc2  6296  oawordi  6319  nnnninf  6973  fzoss1  9841  fzoss2  9842  clsss  12130  ntrss  12131  sslm  12258  txss12  12277  metss2lem  12486  xmettxlem  12498  xmettx  12499  nnsf  12891  nninfself  12901
  Copyright terms: Public domain W3C validator