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

Metamath Proof Explorer

Theorem sylan

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

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

Proof

Step Hyp Ref Expression
1 sylan.1 ⊢ φ → ψ
2 sylan.2 ⊢ ψ ∧ χ → θ
3 2 expcom ⊢ χ → ψ → θ
4 1 3 mpan9 ⊢ φ ∧ χ → θ