Theorem sylan9ssr 3927

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 3926	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ⊆ 𝐶)
4	3	ancoms 464	1 ⊢ ((𝜓 ∧ 𝜑) → 𝐴 ⊆ 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ⊆ wss 3900

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ss 3901

This theorem is used by:  intssuni2  4938  marypha1  9463  cardinfima  10215  cfflb  10376  ssfin4  10427  acsfn  17883  mrelatlub  18786  efgval  19982  islbs3  21484  kgentopon  23912  txlly  24010  sigaclci  34875  bnj1014  35702  topjoin  37368  filnetlem3  37383  cossidmid  38226  poimirlem16  38822  mblfinlem3  38845  sspwimpALT  46167  sspwimpALT2  46170  setrecsres  51201