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

Theorem sstri 3076
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 3074 . 2 (𝐴𝐵 → (𝐵𝐶𝐴𝐶))
41, 2, 3mp2 16 1 𝐴𝐶
Colors of variables: wff set class
Syntax hints:  wss 3041
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 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-11 1469  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-in 3047  df-ss 3054
This theorem is referenced by:  difdif2ss  3303  difdifdirss  3417  snsstp1  3640  snsstp2  3641  nnregexmid  4504  dmexg  4773  rnexg  4774  ssrnres  4951  cossxp  5031  cocnvss  5034  funinsn  5142  fabexg  5280  foimacnv  5353  ssimaex  5450  oprabss  5825  tposssxp  6114  mapsspw  6546  sbthlemi5  6817  sbthlem7  6819  caserel  6940  dmaddpi  7101  dmmulpi  7102  ltrelxr  7793  nnsscn  8689  nn0sscn  8940  nn0ssq  9376  nnssq  9377  qsscn  9379  fzval2  9748  fzossnn  9921  fzo0ssnn0  9947  expcl2lemap  10260  rpexpcl  10267  expge0  10284  expge1  10285  seq3coll  10540  summodclem2a  11105  fsum3cvg3  11120  fsumrpcl  11128  fsumge0  11183  infssuzcldc  11556  isprm3  11711  structfn  11889  strleun  11959  toponsspwpwg  12100  dmtopon  12101  lmbrf  12295  lmres  12328  txcnmpt  12353  qtopbas  12602  tgqioo  12627  dvrecap  12757  cosz12  12772
  Copyright terms: Public domain W3C validator