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

Theorem sstri 2982
Description: Subclass transitivity inference. (Contributed by NM, 5-May-2000.)
Hypotheses
Ref Expression
sstri.1 𝐴𝐵
sstri.2 𝐵𝐶
Assertion
Ref Expression
sstri 𝐴𝐶

Proof of Theorem sstri
StepHypRef Expression
1 sstri.1 . 2 𝐴𝐵
2 sstri.2 . 2 𝐵𝐶
3 sstr2 2980 . 2 (𝐴𝐵 → (𝐵𝐶𝐴𝐶))
41, 2, 3mp2 16 1 𝐴𝐶
Colors of variables: wff set class
Syntax hints:  wss 2945
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-11 1413  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-in 2952  df-ss 2959
This theorem is referenced by:  difdif2ss  3222  difdifdirss  3335  snsstp1  3542  snsstp2  3543  nnregexmid  4370  dmexg  4624  rnexg  4625  ssrnres  4791  cossxp  4871  fabexg  5105  foimacnv  5172  ssimaex  5262  oprabss  5618  tposssxp  5895  dmaddpi  6481  dmmulpi  6482  ltrelxr  7139  nnsscn  7995  nn0sscn  8244  nn0ssq  8660  nnssq  8661  qsscn  8663  fzval2  8979  fzossnn  9147  fzo0ssnn0  9173  serige0  9417  expcl2lemap  9432  rpexpcl  9439  expge0  9456  expge1  9457
  Copyright terms: Public domain W3C validator