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

Metamath Proof Explorer

Theorem sylanl1

Description: A syllogism inference. (Contributed by NM, 10-Mar-2005)

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

Proof

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