Theorem syldanl 614

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 418	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	imdistani 579	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜑 ∧ 𝜒))
4		syldanl.2	. 2 ⊢ (((𝜑 ∧ 𝜒) ∧ 𝜃) → 𝜏)
5	3, 4	sylan 592	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜃) → 𝜏)

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  sylanl2  694  oen0  8578  oeordsuc  8586  erth  8755  phplem2  9203  lo1bdd2  15615  grplmulf1o  19142  grplactcnv  19172  trust  24461  efrlim  27214  suppgsumssiun  33520  evlextv  34060  fedgmullem2  34148  submateq  34327  heibor1lem  38567  idlnegcl  38780  igenmin  38822  eqvrelth  39451  sticksstones22  43042  binomcxplemnotnn0  45188  vonioolem1  47516  vonicclem1  47519  smfsuplem1  47647  smflimsuplem4  47659