Metamath Proof Explorer


Theorem eel2122old

Description: el2122old without virtual deductions. (Contributed by Alan Sare, 13-Jun-2015) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 eel2122old.1
 |-  ( ( ph /\ ps ) -> ch )
2 eel2122old.2
 |-  ( ps -> th )
3 eel2122old.3
 |-  ( ps -> ta )
4 eel2122old.4
 |-  ( ( ch /\ th /\ ta ) -> et )
5 4 3exp
 |-  ( ch -> ( th -> ( ta -> et ) ) )
6 1 5 syl
 |-  ( ( ph /\ ps ) -> ( th -> ( ta -> et ) ) )
7 2 6 syl5
 |-  ( ( ph /\ ps ) -> ( ps -> ( ta -> et ) ) )
8 3 7 syl7
 |-  ( ( ph /\ ps ) -> ( ps -> ( ps -> et ) ) )
9 8 ex
 |-  ( ph -> ( ps -> ( ps -> ( ps -> et ) ) ) )
10 9 pm2.43d
 |-  ( ph -> ( ps -> ( ps -> et ) ) )
11 10 pm2.43d
 |-  ( ph -> ( ps -> et ) )
12 11 imp
 |-  ( ( ph /\ ps ) -> et )