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

Metamath Proof Explorer

Theorem syl2ani

Description: A syllogism inference. (Contributed by NM, 3-Aug-1999)

Ref Expression
Hypotheses syl2ani.1 ⊢ φ → χ
syl2ani.2 ⊢ η → θ
syl2ani.3 ⊢ ψ → χ ∧ θ → τ
Assertion syl2ani ⊢ ψ → φ ∧ η → τ

Proof

Step Hyp Ref Expression
1 syl2ani.1 ⊢ φ → χ
2 syl2ani.2 ⊢ η → θ
3 syl2ani.3 ⊢ ψ → χ ∧ θ → τ
4 2 3 sylan2i ⊢ ψ → χ ∧ η → τ
5 1 4 sylani ⊢ ψ → φ ∧ η → τ