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

Theorem sylan9ssr 3578
Description: A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004.)
Hypotheses
Ref Expression
sylan9ssr.1 (𝜑𝐴𝐵)
sylan9ssr.2 (𝜓𝐵𝐶)
Assertion
Ref Expression
sylan9ssr ((𝜓𝜑) → 𝐴𝐶)

Proof of Theorem sylan9ssr
StepHypRef Expression
1 sylan9ssr.1 . . 3 (𝜑𝐴𝐵)
2 sylan9ssr.2 . . 3 (𝜓𝐵𝐶)
31, 2sylan9ss 3577 . 2 ((𝜑𝜓) → 𝐴𝐶)
43ancoms 467 1 ((𝜓𝜑) → 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wss 3536
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 2032  ax-13 2229  ax-ext 2586
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 2593  df-cleq 2599  df-clel 2602  df-in 3543  df-ss 3550
This theorem is referenced by:  intssuni2  4428  marypha1  8197  cardinfima  8777  cfflb  8938  ssfin4  8989  acsfn  16086  mrelatlub  16952  efgval  17896  islbs3  18919  kgentopon  21090  txlly  21188  sigaclci  29325  bnj1014  30087  topjoin  31333  filnetlem3  31348  poimirlem16  32395  mblfinlem3  32418  sspwimpALT  37983  sspwimpALT2  37986
  Copyright terms: Public domain W3C validator