Metamath Proof Explorer


Theorem eel0321old

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

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

Proof

Step Hyp Ref Expression
1 eel0321old.1 φ
2 eel0321old.2 ψ χ θ τ
3 eel0321old.3 φ τ η
4 1 2 3 sylancr ψ χ θ η