Metamath Proof Explorer

Theorem syl3anl1

Description: A syllogism inference. (Contributed by NM, 24-Feb-2005)

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

Proof

Step Hyp Ref Expression
1 syl3anl1.1 ⊢ φ → ψ
2 syl3anl1.2 ⊢ ψ ∧ χ ∧ θ ∧ τ → η
3 1 3anim1i ⊢ φ ∧ χ ∧ θ → ψ ∧ χ ∧ θ
4 3 2 sylan ⊢ φ ∧ χ ∧ θ ∧ τ → η