Theorem sylan9ssr 3996

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

Step	Hyp	Ref	Expression
1		sylan9ssr.1	. . 3 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		sylan9ssr.2	. . 3 ⊢ (𝜓 → 𝐵 ⊆ 𝐶)
3	1, 2	sylan9ss 3995	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ⊆ 𝐶)
4	3	ancoms 459	1 ⊢ ((𝜓 ∧ 𝜑) → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   ∧ wa 396   ⊆ wss 3948

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965

This theorem is referenced by:  intssuni2  4977  marypha1  9431  cardinfima  10094  cfflb  10256  ssfin4  10307  acsfn  17605  mrelatlub  18517  efgval  19587  islbs3  20774  kgentopon  23049  txlly  23147  sigaclci  33199  bnj1014  34041  topjoin  35336  filnetlem3  35351  poimirlem16  36590  mblfinlem3  36613  sspwimpALT  43768  sspwimpALT2  43771  setrecsres  47825