Metamath Proof Explorer

Theorem syld3an1

Description: A syllogism inference. (Contributed by NM, 7-Jul-2008) (Proof shortened by Wolf Lammen, 26-Jun-2022)

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

Proof

Step Hyp Ref Expression
1 syld3an1.1 ⊢ χ ∧ ψ ∧ θ → φ
2 syld3an1.2 ⊢ φ ∧ ψ ∧ θ → τ
3 simp2 ⊢ χ ∧ ψ ∧ θ → ψ
4 simp3 ⊢ χ ∧ ψ ∧ θ → θ
5 1 3 4 2 syl3anc ⊢ χ ∧ ψ ∧ θ → τ