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

Theorem syl6ss 3026
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 3024 1 (𝜑𝐴𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4  wss 2988
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-11 1440  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-in 2994  df-ss 3001
This theorem is referenced by:  difss2  3117  sstpr  3586  rintm  3802  eqbrrdva  4576  dmxpss2  4831  rnxpss2  4832  ssxpbm  4834  ssxp1  4835  ssxp2  4836  relfld  4927  funssxp  5146  dff2  5408  fliftf  5541  1stcof  5893  2ndcof  5894  tfrlemibfn  6049  tfr1onlembfn  6065  tfrcllemssrecs  6073  tfrcllembfn  6078  sucinc2  6163  peano5nnnn  7374  peano5nni  8363  suprzclex  8780  ioodisj  9345  fzossnn0  9517  elfzom1elp1fzo  9544  frecuzrdgtcl  9750  frecuzrdgdomlem  9755  frecuzrdgfunlem  9757  zfz1iso  10164  iseqcoll  10165  isummolem2a  10684  isummolem2  10685  zisum  10687  fisumsers  10697  fisumcvg3  10698  peano5set  11323
  Copyright terms: Public domain W3C validator