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

Theorem 3sstr4d 3169
 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 3155 . 2 (𝜑 → (𝐶𝐷𝐴𝐵))
51, 4mpbird 166 1 (𝜑𝐶𝐷)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1332   ⊆ wss 3098 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-11 1483  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-ext 2136 This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1740  df-clab 2141  df-cleq 2147  df-clel 2150  df-in 3104  df-ss 3111 This theorem is referenced by:  rdgss  6320  sucinc2  6382  oawordi  6405  nnnninf  7054  fzoss1  10048  fzoss2  10049  clsss  12457  ntrss  12458  sslm  12586  txss12  12605  metss2lem  12836  xmettxlem  12848  xmettx  12849  nnsf  13517  nninfself  13526
 Copyright terms: Public domain W3C validator