Theorem eel2122old 37100

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

Hypotheses

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

Assertion

Ref	Expression
eel2122old	|- ( ( ph /\ ps ) -> et )

Proof of Theorem eel2122old

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

Syntax hints:   -> wi 4   /\ wa 375   /\ w3a 986

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 190  df-an 377  df-3an 988

This theorem is referenced by:  el2122old  37101  suctrALTcf  37316