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

Theorem sstrd 3165
Description: Subclass transitivity deduction. (Contributed by NM, 2-Jun-2004.)
Hypotheses
Ref Expression
sstrd.1 (𝜑𝐴𝐵)
sstrd.2 (𝜑𝐵𝐶)
Assertion
Ref Expression
sstrd (𝜑𝐴𝐶)

Proof of Theorem sstrd
StepHypRef Expression
1 sstrd.1 . 2 (𝜑𝐴𝐵)
2 sstrd.2 . 2 (𝜑𝐵𝐶)
3 sstr 3163 . 2 ((𝐴𝐵𝐵𝐶) → 𝐴𝐶)
41, 2, 3syl2anc 411 1 (𝜑𝐴𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4  wss 3129
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3135  df-ss 3142
This theorem is referenced by:  sstrid  3166  sstrdi  3167  ssdif2d  3274  tfisi  4586  funss  5235  fssxp  5383  fvmptssdm  5600  suppssfv  6078  suppssov1  6079  tposss  6246  tfrlem1  6308  tfrlemibfn  6328  tfr1onlembfn  6344  tfr1onlemubacc  6346  tfr1onlemres  6349  tfrcllembfn  6357  tfrcllemubacc  6359  tfrcllemres  6362  ecinxp  6609  undifdc  6922  sbthlem1  6955  iseqf1olemnab  10485  fiubm  10803  isumss  11394  prodssdc  11592  ennnfoneleminc  12406  strsetsid  12489  strleund  12556  strext  12558  imasaddvallemg  12718  subsubg  13010  subgintm  13011  subsubrg  13326  ntrss  13512  neiint  13538  neiss  13543  restopnb  13574  iscnp4  13611  blssps  13820  blss  13821  xmettx  13903  tgqioo  13940  rescncf  13961  suplociccreex  13995  suplociccex  13996  dvbss  14047  dvbsssg  14048  dvfgg  14050  dvcnp2cntop  14056  dvcn  14057  dvaddxxbr  14058  dvmulxxbr  14059  dvcoapbr  14064
  Copyright terms: Public domain W3C validator