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

Theorem syl6ss 3077
 Description: Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypotheses
Ref Expression
syl6ss.1 (𝜑𝐴𝐵)
syl6ss.2 𝐵𝐶
Assertion
Ref Expression
syl6ss (𝜑𝐴𝐶)

Proof of Theorem syl6ss
StepHypRef Expression
1 syl6ss.1 . 2 (𝜑𝐴𝐵)
2 syl6ss.2 . . 3 𝐵𝐶
32a1i 9 . 2 (𝜑𝐵𝐶)
41, 3sstrd 3075 1 (𝜑𝐴𝐶)
 Colors of variables: wff set class Syntax hints:   → wi 4   ⊆ wss 3039 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 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097 This theorem depends on definitions:  df-bi 116  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-in 3045  df-ss 3052 This theorem is referenced by:  difss2  3172  sstpr  3652  rintm  3873  eqbrrdva  4677  dmxpss2  4939  rnxpss2  4940  ssxpbm  4942  ssxp1  4943  ssxp2  4944  relfld  5035  funssxp  5260  dff2  5530  fliftf  5666  1stcof  6027  2ndcof  6028  tfrlemibfn  6191  tfr1onlembfn  6207  tfrcllemssrecs  6215  tfrcllembfn  6220  sucinc2  6308  peano5nnnn  7664  peano5nni  8680  suprzclex  9100  ioodisj  9716  fzssnn  9788  fzossnn0  9892  elfzom1elp1fzo  9919  frecuzrdgtcl  10125  frecuzrdgdomlem  10130  frecuzrdgfunlem  10132  zfz1iso  10524  seq3coll  10525  summodclem2a  11090  summodclem2  11091  zsumdc  11093  fsumsersdc  11104  fsum3cvg3  11105  exmidunben  11834  strsetsid  11887  lmss  12310  dvbssntrcntop  12696  dvcjbr  12715  peano5set  12940
 Copyright terms: Public domain W3C validator