Metamath Proof Explorer


Theorem ee002

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

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

Proof

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