Theorem syldanl 603

Description: A syllogism deduction with conjoined antecedents. (Contributed by Jeff Madsen, 20-Jun-2011.)

Hypotheses

Ref	Expression
syldanl.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)
syldanl.2	⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
syldanl	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜏)

Proof of Theorem syldanl

Step	Hyp	Ref	Expression
1		syldanl.1	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	ex 415	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	imdistani 571	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒))
4		syldanl.2	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏)
5	3, 4	sylan 582	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 398

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

This theorem depends on definitions:  df-bi 209  df-an 399

This theorem is referenced by:  sylanl2  679  oen0  8214  oeordsuc  8222  erth  8340  lo1bdd2  14883  grplmulf1o  18175  grplactcnv  18204  trust  22840  efrlim  25549  fedgmullem2  31028  submateq  31076  heibor1lem  35089  idlnegcl  35302  igenmin  35344  eqvrelth  35848  binomcxplemnotnn0  40695  vonioolem1  42969  vonicclem1  42972  smfsuplem1  43092  smflimsuplem4  43104