This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )