Theorem ecase23d

Description: Deduction for elimination by cases. (Contributed by NM, 22-Apr-1994)

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

Proof

Step	Hyp	Ref	Expression
1		ecase23d.1	|- ( ph -> -. ch )
2		ecase23d.2	|- ( ph -> -. th )
3		ecase23d.3	|- ( ph -> ( ps \/ ch \/ th ) )
4		3orass	|- ( ( ps \/ ch \/ th ) <-> ( ps \/ ( ch \/ th ) ) )
5	3 4	sylib	|- ( ph -> ( ps \/ ( ch \/ th ) ) )
6		ioran	|- ( -. ( ch \/ th ) <-> ( -. ch /\ -. th ) )
7	1 2 6	sylanbrc	|- ( ph -> -. ( ch \/ th ) )
8	5 7	olcnd	|- ( ph -> ps )