Theorem syldanl 611

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  sylanl2  691  oen0  8551  oeordsuc  8559  erth  8728  phplem2  9169  lo1bdd2  15534  grplmulf1o  19038  grplactcnv  19068  trust  24269  efrlim  27011  suppgsumssiun  33213  evlextv  33800  fedgmullem2  33888  submateq  34067  heibor1lem  38272  idlnegcl  38485  igenmin  38527  eqvrelth  39158  sticksstones22  42749  binomcxplemnotnn0  44896  vonioolem1  47218  vonicclem1  47221  smfsuplem1  47349  smflimsuplem4  47361