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  8579  oeordsuc  8587  erth  8756  phplem2  9204  lo1bdd2  15671  grplmulf1o  19203  grplactcnv  19233  trust  24528  efrlim  27279  suppgsumssiun  33615  evlextv  34156  fedgmullem2  34244  submateq  34423  heibor1lem  38711  idlnegcl  38924  igenmin  38966  eqvrelth  39595  sticksstones22  43186  binomcxplemnotnn0  45299  vonioolem1  47634  vonicclem1  47637  smfsuplem1  47765  smflimsuplem4  47777