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

Metamath Proof Explorer

Theorem syl22anc

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

Ref Expression
Hypotheses syl12anc.1 ⊢ φ → ψ
syl12anc.2 ⊢ φ → χ
syl12anc.3 ⊢ φ → θ
syl22anc.4 ⊢ φ → τ
syl22anc.5 ⊢ ψ ∧ χ ∧ θ ∧ τ → η
Assertion syl22anc ⊢ φ → η

Proof

Step Hyp Ref Expression
1 syl12anc.1 ⊢ φ → ψ
2 syl12anc.2 ⊢ φ → χ
3 syl12anc.3 ⊢ φ → θ
4 syl22anc.4 ⊢ φ → τ
5 syl22anc.5 ⊢ ψ ∧ χ ∧ θ ∧ τ → η
6 1 2 jca ⊢ φ → ψ ∧ χ
7 6 3 4 5 syl12anc ⊢ φ → η