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 ⊢ ( ( 𝜑 ∧ 𝜒 ∧ 𝜏 ) → 𝜁 )