Metamath Proof Explorer


Theorem syl3an

Description: A triple syllogism inference. (Contributed by NM, 13-May-2004)

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

Proof

Step Hyp Ref Expression
1 syl3an.1 ⊢ φ → ψ
2 syl3an.2 ⊢ χ → θ
3 syl3an.3 ⊢ τ → η
4 syl3an.4 ⊢ ψ ∧ θ ∧ η → ζ
5 1 2 3 3anim123i ⊢ φ ∧ χ ∧ τ → ψ ∧ θ ∧ η
6 5 4 syl ⊢ φ ∧ χ ∧ τ → ζ