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  8573  oeordsuc  8581  erth  8750  phplem2  9190  lo1bdd2  15577  grplmulf1o  19080  grplactcnv  19110  trust  24367  efrlim  27112  suppgsumssiun  33370  evlextv  33910  fedgmullem2  33998  submateq  34177  heibor1lem  38438  idlnegcl  38651  igenmin  38693  eqvrelth  39322  sticksstones22  42913  binomcxplemnotnn0  45046  vonioolem1  47374  vonicclem1  47377  smfsuplem1  47505  smflimsuplem4  47517