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

Theorem sylan9ss 4008
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 4003 . 2 ((𝐴𝐵𝐵𝐶) → 𝐴𝐶)
41, 2, 3syl2an 596 1 ((𝜑𝜓) → 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wss 3962
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805
This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3979
This theorem is referenced by:  sylan9ssr  4009  psstr  4116  unss12  4197  ss2in  4252  ssdisj  4465  relrelss  6294  funssxp  6764  axdc3lem  10487  tskuni  10820  rtrclreclem4  15096  tsmsxp  24178  shslubi  31413  chlej12i  31503  insiga  34117  fnetr  36333  pcl0bN  39905  brtrclfv2  43716
  Copyright terms: Public domain W3C validator