Metamath Proof Explorer


Theorem ee022

Description: e022 without virtual deductions. (Contributed by Alan Sare, 13-Jul-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses ee022.1 𝜑
ee022.2 ( 𝜓 → ( 𝜒𝜃 ) )
ee022.3 ( 𝜓 → ( 𝜒𝜏 ) )
ee022.4 ( 𝜑 → ( 𝜃 → ( 𝜏𝜂 ) ) )
Assertion ee022 ( 𝜓 → ( 𝜒𝜂 ) )

Proof

Step Hyp Ref Expression
1 ee022.1 𝜑
2 ee022.2 ( 𝜓 → ( 𝜒𝜃 ) )
3 ee022.3 ( 𝜓 → ( 𝜒𝜏 ) )
4 ee022.4 ( 𝜑 → ( 𝜃 → ( 𝜏𝜂 ) ) )
5 1 a1i ( 𝜒𝜑 )
6 5 a1i ( 𝜓 → ( 𝜒𝜑 ) )
7 6 2 3 4 ee222 ( 𝜓 → ( 𝜒𝜂 ) )