Theorem sylan9ss 3936

Description: A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)

Hypotheses

Ref	Expression
sylan9ss.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
sylan9ss.2	⊢ (𝜓 → 𝐵 ⊆ 𝐶)

Assertion

Ref	Expression
sylan9ss	⊢ ((𝜑 ∧ 𝜓) → 𝐴 ⊆ 𝐶)

Proof of Theorem sylan9ss

Step	Hyp	Ref	Expression
1		sylan9ss.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		sylan9ss.2	. 2 ⊢ (𝜓 → 𝐵 ⊆ 𝐶)
3		sstr 3931	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶)
4	1, 2, 3	syl2an 597	1 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ⊆ 𝐶)

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

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

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

This theorem is referenced by:  sylan9ssr  3937  psstr  4048  unss12  4129  ss2in  4186  ssdisj  4401  relrelss  6231  funssxp  6690  axdc3lem  10363  tskuni  10697  rtrclreclem4  15014  tsmsxp  24130  shslubi  31471  chlej12i  31561  insiga  34297  fnetr  36549  pcl0bN  40383  brtrclfv2  44172