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
|- ph
ee022.2
|- ( ps -> ( ch -> th ) )
ee022.3
|- ( ps -> ( ch -> ta ) )
ee022.4
|- ( ph -> ( th -> ( ta -> et ) ) )
Assertion ee022
|- ( ps -> ( ch -> et ) )

Proof

Step Hyp Ref Expression
1 ee022.1
 |-  ph
2 ee022.2
 |-  ( ps -> ( ch -> th ) )
3 ee022.3
 |-  ( ps -> ( ch -> ta ) )
4 ee022.4
 |-  ( ph -> ( th -> ( ta -> et ) ) )
5 1 a1i
 |-  ( ch -> ph )
6 5 a1i
 |-  ( ps -> ( ch -> ph ) )
7 6 2 3 4 ee222
 |-  ( ps -> ( ch -> et ) )