Theorem ee223

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

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

Proof

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