Theorem sylan9ss 3943

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 3938	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶)
4	1, 2, 3	syl2an 596	1 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 ⊆ 𝐶)

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

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

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

This theorem is referenced by:  sylan9ssr  3944  psstr  4052  unss12  4133  ss2in  4190  ssdisj  4405  relrelss  6215  funssxp  6674  axdc3lem  10336  tskuni  10669  rtrclreclem4  14963  tsmsxp  24065  shslubi  31357  chlej12i  31447  insiga  34142  fnetr  36385  pcl0bN  39962  brtrclfv2  43760