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

Theorem sstri 3106
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 3104 . 2 (𝐴𝐵 → (𝐵𝐶𝐴𝐶))
41, 2, 3mp2 16 1 𝐴𝐶
Colors of variables: wff set class
Syntax hints:  wss 3071
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 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-in 3077  df-ss 3084
This theorem is referenced by:  difdif2ss  3333  difdifdirss  3447  snsstp1  3670  snsstp2  3671  nnregexmid  4534  dmexg  4803  rnexg  4804  ssrnres  4981  cossxp  5061  cocnvss  5064  funinsn  5172  fabexg  5310  foimacnv  5385  ssimaex  5482  oprabss  5857  tposssxp  6146  mapsspw  6578  sbthlemi5  6849  sbthlem7  6851  caserel  6972  dmaddpi  7140  dmmulpi  7141  ltrelxr  7832  nnsscn  8732  nn0sscn  8989  nn0ssq  9427  nnssq  9428  qsscn  9430  fzval2  9800  fzossnn  9973  fzo0ssnn0  9999  expcl2lemap  10312  rpexpcl  10319  expge0  10336  expge1  10337  seq3coll  10592  summodclem2a  11157  fsum3cvg3  11172  fsumrpcl  11180  fsumge0  11235  prodmodclem2a  11352  infssuzcldc  11651  isprm3  11806  structfn  11988  strleun  12058  toponsspwpwg  12199  dmtopon  12200  lmbrf  12394  lmres  12427  txcnmpt  12452  qtopbas  12701  tgqioo  12726  dvrecap  12856  cosz12  12874  ioocosf1o  12948
  Copyright terms: Public domain W3C validator