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

Theorem sylan9ssr 3906
 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 3905 . 2 ((𝜑𝜓) → 𝐴𝐶)
43ancoms 462 1 ((𝜓𝜑) → 𝐴𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ⊆ wss 3858 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3865  df-ss 3875 This theorem is referenced by:  intssuni2  4863  marypha1  8931  cardinfima  9557  cfflb  9719  ssfin4  9770  acsfn  16988  mrelatlub  17862  efgval  18910  islbs3  19995  kgentopon  22238  txlly  22336  sigaclci  31619  bnj1014  32461  topjoin  34103  filnetlem3  34118  poimirlem16  35353  mblfinlem3  35376  sspwimpALT  42004  sspwimpALT2  42007  setrecsres  45622
 Copyright terms: Public domain W3C validator