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

Theorem sylan9ss 3580
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 3575 . 2 ((𝐴𝐵𝐵𝐶) → 𝐴𝐶)
41, 2, 3syl2an 492 1 ((𝜑𝜓) → 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wss 3539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-in 3546  df-ss 3553
This theorem is referenced by:  sylan9ssr  3581  psstr  3672  unss12  3746  ss2in  3801  ssdisj  3977  relrelss  5562  funssxp  5960  axdc3lem  9132  tskuni  9461  rtrclreclem4  13595  tsmsxp  21710  shslubi  27434  chlej12i  27524  insiga  29333  fnetr  31322  pcl0bN  34023  brtrclfv2  36834
  Copyright terms: Public domain W3C validator