Theorem sylan9ssr 3948

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

Syntax hints:   → wi 4   ∧ wa 399   ⊆ wss 3902

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-ss 3919

This theorem is referenced by:  intssuni2  4928  marypha1  9374  cardinfima  10047  cfflb  10210  ssfin4  10261  acsfn  17682  mrelatlub  18585  efgval  19748  islbs3  21213  kgentopon  23586  txlly  23684  sigaclci  34390  bnj1014  35217  topjoin  36686  filnetlem3  36701  poimirlem16  38096  mblfinlem3  38119  sspwimpALT  45461  sspwimpALT2  45464  setrecsres  50284