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

Metamath Proof Explorer

Theorem sylanr1

Description: A syllogism inference. (Contributed by NM, 9-Apr-2005)

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

Proof

Step Hyp Ref Expression
1 sylanr1.1 ⊢ φ → χ
2 sylanr1.2 ⊢ ψ ∧ χ ∧ θ → τ
3 1 anim1i ⊢ φ ∧ θ → χ ∧ θ
4 3 2 sylan2 ⊢ ψ ∧ φ ∧ θ → τ