This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem syldanl

Description: A syllogism deduction with conjoined antecedents. (Contributed by Jeff Madsen, 20-Jun-2011)

Ref Expression
Hypotheses syldanl.1 ⊢ φ ∧ ψ → χ
syldanl.2 ⊢ φ ∧ χ ∧ θ → τ
Assertion syldanl ⊢ φ ∧ ψ ∧ θ → τ

Proof

Step Hyp Ref Expression
1 syldanl.1 ⊢ φ ∧ ψ → χ
2 syldanl.2 ⊢ φ ∧ χ ∧ θ → τ
3 1 ex ⊢ φ → ψ → χ
4 3 imdistani ⊢ φ ∧ ψ → φ ∧ χ
5 4 2 sylan ⊢ φ ∧ ψ ∧ θ → τ