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

Metamath Proof Explorer

Theorem eel00000

Description: Elimination rule similar eel0000 , except with five hpothesis steps. (Contributed by Alan Sare, 17-Oct-2017)

Ref Expression
Hypotheses eel00000.1 ⊢ 𝜑
eel00000.2 ⊢ 𝜓
eel00000.3 ⊢ 𝜒
eel00000.4 ⊢ 𝜃
eel00000.5 ⊢ 𝜏
eel00000.6 ⊢ ( ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ∧ 𝜃 ) ∧ 𝜏 ) → 𝜂 )
Assertion eel00000 𝜂

Proof

Step Hyp Ref Expression
1 eel00000.1 ⊢ 𝜑
2 eel00000.2 ⊢ 𝜓
3 eel00000.3 ⊢ 𝜒
4 eel00000.4 ⊢ 𝜃
5 eel00000.5 ⊢ 𝜏
6 eel00000.6 ⊢ ( ( ( ( ( 𝜑 ∧ 𝜓 ) ∧ 𝜒 ) ∧ 𝜃 ) ∧ 𝜏 ) → 𝜂 )
7 6 exp41 ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜒 → ( 𝜃 → ( 𝜏 → 𝜂 ) ) ) )
8 1 7 mpan ⊢ ( 𝜓 → ( 𝜒 → ( 𝜃 → ( 𝜏 → 𝜂 ) ) ) )
9 2 3 8 mp2 ⊢ ( 𝜃 → ( 𝜏 → 𝜂 ) )
10 4 5 9 mp2 ⊢ 𝜂