Metamath Proof Explorer


Theorem eel021old

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

Ref Expression
Hypotheses eel021.1 φ
eel021.2 ψχθ
eel021.3 φθτ
Assertion eel021old ψχτ

Proof

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