Theorem syldanl 613

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  sylanl2  693  oen0  8560  oeordsuc  8568  erth  8737  phplem2  9177  lo1bdd2  15565  grplmulf1o  19070  grplactcnv  19100  trust  24347  efrlim  27092  suppgsumssiun  33305  evlextv  33849  fedgmullem2  33937  submateq  34116  heibor1lem  38320  idlnegcl  38533  igenmin  38575  eqvrelth  39206  sticksstones22  42797  binomcxplemnotnn0  44930  vonioolem1  47252  vonicclem1  47255  smfsuplem1  47383  smflimsuplem4  47395