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

Metamath Proof Explorer

Theorem sylanl2

Description: A syllogism inference. (Contributed by NM, 1-Jan-2005)

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

Proof

Step Hyp Ref Expression
1 sylanl2.1 ⊢ φ → χ
2 sylanl2.2 ⊢ ψ ∧ χ ∧ θ → τ
3 1 adantl ⊢ ψ ∧ φ → χ
4 3 2 syldanl ⊢ ψ ∧ φ ∧ θ → τ