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

Metamath Proof Explorer

Theorem syland

Description: A syllogism deduction. (Contributed by NM, 15-Dec-2004)

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

Proof

Step Hyp Ref Expression
1 syland.1 ⊢ φ → ψ → χ
2 syland.2 ⊢ φ → χ ∧ θ → τ
3 2 expd ⊢ φ → χ → θ → τ
4 1 3 syld ⊢ φ → ψ → θ → τ
5 4 impd ⊢ φ → ψ ∧ θ → τ