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

Metamath Proof Explorer

Theorem syl3anl

Description: A triple syllogism inference. (Contributed by NM, 24-Dec-2006)

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

Proof

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