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

Theorem sylan9ssr 3998
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 3997 . 2 ((𝜑𝜓) → 𝐴𝐶)
43ancoms 458 1 ((𝜓𝜑) → 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wss 3951
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809
This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3968
This theorem is referenced by:  intssuni2  4973  marypha1  9474  cardinfima  10137  cfflb  10299  ssfin4  10350  acsfn  17702  mrelatlub  18607  efgval  19735  islbs3  21157  kgentopon  23546  txlly  23644  sigaclci  34133  bnj1014  34975  topjoin  36366  filnetlem3  36381  poimirlem16  37643  mblfinlem3  37666  sspwimpALT  44945  sspwimpALT2  44948  setrecsres  49221
  Copyright terms: Public domain W3C validator