Theorem sylan9ssr 3945

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

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

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 3916

This theorem is used by:  intssuni2  4933  marypha1  9419  cardinfima  10169  cfflb  10330  ssfin4  10381  acsfn  17826  mrelatlub  18729  efgval  19924  islbs3  21426  kgentopon  23850  txlly  23948  sigaclci  34757  bnj1014  35584  topjoin  37133  filnetlem3  37148  poimirlem16  38534  mblfinlem3  38557  sspwimpALT  45892  sspwimpALT2  45895  setrecsres  50764