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

Metamath Proof Explorer

Theorem syli

Description: Syllogism inference with common nested antecedent. (Contributed by NM, 4-Nov-2004)

Ref Expression
Hypotheses syli.1 ⊢ ψ → φ → χ
syli.2 ⊢ χ → φ → θ
Assertion syli ⊢ ψ → φ → θ

Proof

Step Hyp Ref Expression
1 syli.1 ⊢ ψ → φ → χ
2 syli.2 ⊢ χ → φ → θ
3 2 com12 ⊢ φ → χ → θ
4 1 3 sylcom ⊢ ψ → φ → θ