Metamath Proof Explorer


Theorem ee30

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

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

Proof

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