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

Metamath Proof Explorer

Theorem syl3an2

Description: A syllogism inference. (Contributed by NM, 22-Aug-1995) (Proof shortened by Wolf Lammen, 26-Jun-2022)

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

Proof

Step Hyp Ref Expression
1 syl3an2.1 ⊢ φ → χ
2 syl3an2.2 ⊢ ψ ∧ χ ∧ θ → τ
3 1 3anim2i ⊢ ψ ∧ φ ∧ θ → ψ ∧ χ ∧ θ
4 3 2 syl ⊢ ψ ∧ φ ∧ θ → τ