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  8599  oeordsuc  8607  erth  8776  phplem2  9224  lo1bdd2  15697  grplmulf1o  19229  grplactcnv  19259  trust  24554  efrlim  27303  suppgsumssiun  33680  evlextv  34221  fedgmullem2  34309  submateq  34488  heibor1lem  38837  idlnegcl  39050  igenmin  39092  eqvrelth  39721  sticksstones22  43312  binomcxplemnotnn0  45434  vonioolem1  47784  vonicclem1  47787  smfsuplem1  47915  smflimsuplem4  47927