Metamath Proof Explorer


Theorem ee020

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

Ref Expression
Hypotheses ee020.1
|- ph
ee020.2
|- ( ps -> ( ch -> th ) )
ee020.3
|- ta
ee020.4
|- ( ph -> ( th -> ( ta -> et ) ) )
Assertion ee020
|- ( ps -> ( ch -> et ) )

Proof

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