Metamath Proof Explorer

Theorem syl3anl3

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

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

Proof

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