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

Metamath Proof Explorer

Theorem syl3c

Description: A syllogism inference combined with contraction. (Contributed by Alan Sare, 7-Jul-2011)

Ref Expression
Hypotheses syl3c.1 ⊢ φ → ψ
syl3c.2 ⊢ φ → χ
syl3c.3 ⊢ φ → θ
syl3c.4 ⊢ ψ → χ → θ → τ
Assertion syl3c ⊢ φ → τ

Proof

Step Hyp Ref Expression
1 syl3c.1 ⊢ φ → ψ
2 syl3c.2 ⊢ φ → χ
3 syl3c.3 ⊢ φ → θ
4 syl3c.4 ⊢ ψ → χ → θ → τ
5 1 2 4 sylc ⊢ φ → θ → τ
6 3 5 mpd ⊢ φ → τ