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

Metamath Proof Explorer

Theorem syld3an2

Description: A syllogism inference. (Contributed by NM, 20-May-2007)

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

Proof

Step Hyp Ref Expression
1 syld3an2.1 ⊢ φ ∧ χ ∧ θ → ψ
2 syld3an2.2 ⊢ φ ∧ ψ ∧ θ → τ
3 simp1 ⊢ φ ∧ χ ∧ θ → φ
4 simp3 ⊢ φ ∧ χ ∧ θ → θ
5 3 1 4 2 syl3anc ⊢ φ ∧ χ ∧ θ → τ