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 η