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

Metamath Proof Explorer

Theorem syl13anc

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012)

Ref Expression
Hypotheses syl3anc.1 ⊢ φ → ψ
syl3anc.2 ⊢ φ → χ
syl3anc.3 ⊢ φ → θ
syl3Xanc.4 ⊢ φ → τ
syl13anc.5 ⊢ ψ ∧ χ ∧ θ ∧ τ → η
Assertion syl13anc ⊢ φ → η

Proof

Step Hyp Ref Expression
1 syl3anc.1 ⊢ φ → ψ
2 syl3anc.2 ⊢ φ → χ
3 syl3anc.3 ⊢ φ → θ
4 syl3Xanc.4 ⊢ φ → τ
5 syl13anc.5 ⊢ ψ ∧ χ ∧ θ ∧ τ → η
6 2 3 4 3jca ⊢ φ → χ ∧ θ ∧ τ
7 1 6 5 syl2anc ⊢ φ → η