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