Theorem ee223 38859

Description: e223 38860 without virtual deductions. (Contributed by Alan Sare, 12-Dec-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

Ref	Expression
ee223.1	|- ( ph -> ( ps -> ch ) )
ee223.2	|- ( ph -> ( ps -> th ) )
ee223.3	|- ( ph -> ( ps -> ( ta -> et ) ) )
ee223.4	|- ( ch -> ( th -> ( et -> ze ) ) )

Assertion

Ref	Expression
ee223	|- ( ph -> ( ps -> ( ta -> ze ) ) )

Proof of Theorem ee223

Step	Hyp	Ref	Expression
1		ee223.2	. 2 |- ( ph -> ( ps -> th ) )
2		ee223.3	. . . . . . . 8 |- ( ph -> ( ps -> ( ta -> et ) ) )
3		ee223.1	. . . . . . . . . . . 12 |- ( ph -> ( ps -> ch ) )
4		ee223.4	. . . . . . . . . . . 12 |- ( ch -> ( th -> ( et -> ze ) ) )
5	3, 4	syl6 35	. . . . . . . . . . 11 |- ( ph -> ( ps -> ( th -> ( et -> ze ) ) ) )
6	5	com34 91	. . . . . . . . . 10 |- ( ph -> ( ps -> ( et -> ( th -> ze ) ) ) )
7	6	com23 86	. . . . . . . . 9 |- ( ph -> ( et -> ( ps -> ( th -> ze ) ) ) )
8	7	com12 32	. . . . . . . 8 |- ( et -> ( ph -> ( ps -> ( th -> ze ) ) ) )
9	2, 8	syl8 76	. . . . . . 7 |- ( ph -> ( ps -> ( ta -> ( ph -> ( ps -> ( th -> ze ) ) ) ) ) )
10	9	com34 91	. . . . . 6 |- ( ph -> ( ps -> ( ph -> ( ta -> ( ps -> ( th -> ze ) ) ) ) ) )
11	10	pm2.43a 54	. . . . 5 |- ( ph -> ( ps -> ( ta -> ( ps -> ( th -> ze ) ) ) ) )
12	11	com34 91	. . . 4 |- ( ph -> ( ps -> ( ps -> ( ta -> ( th -> ze ) ) ) ) )
13	12	pm2.43d 53	. . 3 |- ( ph -> ( ps -> ( ta -> ( th -> ze ) ) ) )
14	13	com34 91	. 2 |- ( ph -> ( ps -> ( th -> ( ta -> ze ) ) ) )
15	1, 14	mpdd 43	1 |- ( ph -> ( ps -> ( ta -> ze ) ) )

Syntax hints:   -> wi 4

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

This theorem is referenced by:  e223  38860