Metamath Proof Explorer


Theorem eel00001

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

Ref Expression
Hypotheses eel00001.1 φ
eel00001.2 ψ
eel00001.3 χ
eel00001.4 θ
eel00001.5 τ η
eel00001.6 φ ψ χ θ η ζ
Assertion eel00001 τ ζ

Proof

Step Hyp Ref Expression
1 eel00001.1 φ
2 eel00001.2 ψ
3 eel00001.3 χ
4 eel00001.4 θ
5 eel00001.5 τ η
6 eel00001.6 φ ψ χ θ η ζ
7 6 exp41 φ ψ χ θ η ζ
8 1 2 7 mp2an χ θ η ζ
9 3 4 8 mp2 η ζ
10 5 9 syl τ ζ