Metamath Proof Explorer


Theorem eel2122old

Description: el2122old without virtual deductions. (Contributed by Alan Sare, 13-Jun-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses eel2122old.1 φ ψ χ
eel2122old.2 ψ θ
eel2122old.3 ψ τ
eel2122old.4 χ θ τ η
Assertion eel2122old φ ψ η

Proof

Step Hyp Ref Expression
1 eel2122old.1 φ ψ χ
2 eel2122old.2 ψ θ
3 eel2122old.3 ψ τ
4 eel2122old.4 χ θ τ η
5 4 3exp χ θ τ η
6 1 5 syl φ ψ θ τ η
7 2 6 syl5 φ ψ ψ τ η
8 3 7 syl7 φ ψ ψ ψ η
9 8 ex φ ψ ψ ψ η
10 9 pm2.43d φ ψ ψ η
11 10 pm2.43d φ ψ η
12 11 imp φ ψ η