MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylan9ss Structured version   Visualization version   GIF version

Theorem sylan9ss 3995
Description: A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
Hypotheses
Ref Expression
sylan9ss.1 (𝜑𝐴𝐵)
sylan9ss.2 (𝜓𝐵𝐶)
Assertion
Ref Expression
sylan9ss ((𝜑𝜓) → 𝐴𝐶)

Proof of Theorem sylan9ss
StepHypRef Expression
1 sylan9ss.1 . 2 (𝜑𝐴𝐵)
2 sylan9ss.2 . 2 (𝜓𝐵𝐶)
3 sstr 3990 . 2 ((𝐴𝐵𝐵𝐶) → 𝐴𝐶)
41, 2, 3syl2an 596 1 ((𝜑𝜓) → 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wss 3948
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965
This theorem is referenced by:  sylan9ssr  3996  psstr  4104  unss12  4182  ss2in  4236  ssdisj  4459  relrelss  6272  funssxp  6746  axdc3lem  10447  tskuni  10780  rtrclreclem4  15010  tsmsxp  23666  shslubi  30676  chlej12i  30766  insiga  33204  fnetr  35322  pcl0bN  38880  brtrclfv2  42560
  Copyright terms: Public domain W3C validator