Theorem sylan9ss 3951

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

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

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 3923

This theorem is used by:  sylan9ssr  3952  psstr  4063  unss12  4141  ss2in  4197  ssdisj  4420  relrelss  6277  funssxp  6738  axdc3lem  10445  tskuni  10779  rtrclreclem4  15117  tsmsxp  24341  shslubi  31766  chlej12i  31856  insiga  34551  fnetr  36895  pcl0bN  40730  brtrclfv2  44486