Theorem ecased

Description: Deduction for elimination by cases. (Contributed by NM, 8-Oct-2012)

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

Proof

Step	Hyp	Ref	Expression
1		ecased.1	|- ( ph -> ( -. ps -> th ) )
2		ecased.2	|- ( ph -> ( -. ch -> th ) )
3		ecased.3	|- ( ph -> ( ( ps /\ ch ) -> th ) )
4		pm3.11	|- ( -. ( -. ps \/ -. ch ) -> ( ps /\ ch ) )
5	4 3	syl5	|- ( ph -> ( -. ( -. ps \/ -. ch ) -> th ) )
6	1 2 5	ecase3d	|- ( ph -> th )