Theorem ecase13d

Description: Deduction for elimination by cases. (Contributed by Jeff Hankins, 18-Aug-2009)

	Ref	Expression
Hypotheses	ecase13d.1	|- ( ph -> -. ch )
	ecase13d.2	|- ( ph -> -. th )
	ecase13d.3	|- ( ph -> ( ch \/ ps \/ th ) )
Assertion	ecase13d	|- ( ph -> ps )

Proof

Step	Hyp	Ref	Expression
1		ecase13d.1	|- ( ph -> -. ch )
2		ecase13d.2	|- ( ph -> -. th )
3		ecase13d.3	|- ( ph -> ( ch \/ ps \/ th ) )
4		3orass	|- ( ( ch \/ ps \/ th ) <-> ( ch \/ ( ps \/ th ) ) )
5		df-or	|- ( ( ch \/ ( ps \/ th ) ) <-> ( -. ch -> ( ps \/ th ) ) )
6	4 5	bitri	|- ( ( ch \/ ps \/ th ) <-> ( -. ch -> ( ps \/ th ) ) )
7	3 6	sylib	|- ( ph -> ( -. ch -> ( ps \/ th ) ) )
8	1 7	mpd	|- ( ph -> ( ps \/ th ) )
9		orcom	|- ( ( ps \/ th ) <-> ( th \/ ps ) )
10		df-or	|- ( ( th \/ ps ) <-> ( -. th -> ps ) )
11	9 10	bitri	|- ( ( ps \/ th ) <-> ( -. th -> ps ) )
12	8 11	sylib	|- ( ph -> ( -. th -> ps ) )
13	2 12	mpd	|- ( ph -> ps )