Theorem sylan9ssr 4010

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3980

This theorem is referenced by:  intssuni2  4978  marypha1  9472  cardinfima  10135  cfflb  10297  ssfin4  10348  acsfn  17704  mrelatlub  18620  efgval  19750  islbs3  21175  kgentopon  23562  txlly  23660  sigaclci  34113  bnj1014  34954  topjoin  36348  filnetlem3  36363  poimirlem16  37623  mblfinlem3  37646  sspwimpALT  44923  sspwimpALT2  44926  setrecsres  48933