Theorem syldanl 608

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  sylanl2  687  oen0  8519  oeordsuc  8527  erth  8695  phplem2  9136  lo1bdd2  15484  grplmulf1o  18987  grplactcnv  19017  trust  24219  efrlim  26958  suppgsumssiun  33160  evlextv  33733  fedgmullem2  33821  submateq  34000  heibor1lem  38183  idlnegcl  38396  igenmin  38438  eqvrelth  39069  sticksstones22  42660  binomcxplemnotnn0  44807  vonioolem1  47130  vonicclem1  47133  smfsuplem1  47261  smflimsuplem4  47273