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

Theorem sylan9ss 3900
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 3895 . 2 ((𝐴𝐵𝐵𝐶) → 𝐴𝐶)
41, 2, 3syl2an 599 1 ((𝜑𝜓) → 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wss 3853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-v 3402  df-in 3860  df-ss 3870
This theorem is referenced by:  sylan9ssr  3901  psstr  4005  unss12  4082  ss2in  4137  ssdisj  4359  relrelss  6115  funssxp  6544  axdc3lem  9963  tskuni  10296  rtrclreclem4  14523  tsmsxp  22919  shslubi  29333  chlej12i  29423  insiga  31688  fnetr  34196  pcl0bN  37593  brtrclfv2  40922
  Copyright terms: Public domain W3C validator