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

Metamath Proof Explorer

Theorem eel12131

Description: An elimination deduction. (Contributed by Alan Sare, 17-Oct-2017)

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

Proof

Step Hyp Ref Expression
1 eel12131.1 ⊢ φ → ψ
2 eel12131.2 ⊢ φ ∧ χ → θ
3 eel12131.3 ⊢ φ ∧ τ → η
4 eel12131.4 ⊢ ψ ∧ θ ∧ η → ζ
5 4 3exp ⊢ ψ → θ → η → ζ
6 1 2 5 syl2imc ⊢ φ ∧ χ → φ → η → ζ
7 6 ex ⊢ φ → χ → φ → η → ζ
8 7 pm2.43b ⊢ χ → φ → η → ζ
9 8 com13 ⊢ η → φ → χ → ζ
10 3 9 syl ⊢ φ ∧ τ → φ → χ → ζ
11 10 ex ⊢ φ → τ → φ → χ → ζ
12 11 pm2.43b ⊢ τ → φ → χ → ζ
13 12 3imp231 ⊢ φ ∧ χ ∧ τ → ζ