Theorem sylan9ss 3900

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-v 3402  df-in 3860  df-ss 3870

This theorem is referenced by:  sylan9ssr  3901  psstr  4005  unss12  4082  ss2in  4137  ssdisj  4359  relrelss  6115  funssxp  6544  axdc3lem  9963  tskuni  10296  rtrclreclem4  14523  tsmsxp  22919  shslubi  29333  chlej12i  29423  insiga  31688  fnetr  34196  pcl0bN  37593  brtrclfv2  40922