Metamath Proof Explorer


Theorem sylan2

Description: A syllogism inference. (Contributed by NM, 21-Apr-1994) (Proof shortened by Wolf Lammen, 22-Nov-2012)

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

Proof

Step Hyp Ref Expression
1 sylan2.1 ⊢ φ → χ
2 sylan2.2 ⊢ ψ ∧ χ → θ
3 1 adantl ⊢ ψ ∧ φ → χ
4 3 2 syldan ⊢ ψ ∧ φ → θ