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 ( ( 𝜓𝜒 ) → 𝜏 )