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		ioran	|- ( -. ( ch \/ th ) <-> ( -. ch /\ -. th ) )
5	1 2 4	sylanbrc	|- ( ph -> -. ( ch \/ th ) )
6		3orass	|- ( ( ps \/ ch \/ th ) <-> ( ps \/ ( ch \/ th ) ) )
7	3 6	sylib	|- ( ph -> ( ps \/ ( ch \/ th ) ) )
8	7	ord	|- ( ph -> ( -. ps -> ( ch \/ th ) ) )
9	5 8	mt3d	|- ( ph -> ps )