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

Theorem sylan9ss 3908
 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 3903 . 2 ((𝐴𝐵𝐵𝐶) → 𝐴𝐶)
41, 2, 3syl2an 595 1 ((𝜑𝜓) → 𝐴𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 396   ⊆ wss 3865 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-in 3872  df-ss 3880 This theorem is referenced by:  sylan9ssr  3909  psstr  4008  unss12  4085  ss2in  4139  ssdisj  4329  relrelss  6006  funssxp  6410  axdc3lem  9725  tskuni  10058  rtrclreclem4  14258  tsmsxp  22450  shslubi  28849  chlej12i  28939  insiga  31009  fnetr  33310  pcl0bN  36611  brtrclfv2  39578
 Copyright terms: Public domain W3C validator