Theorem ecase3ad

Description: Deduction for elimination by cases. (Contributed by NM, 24-May-2013)

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

Proof

Step	Hyp	Ref	Expression
1		ecase3ad.1	|- ( ph -> ( ps -> th ) )
2		ecase3ad.2	|- ( ph -> ( ch -> th ) )
3		ecase3ad.3	|- ( ph -> ( ( -. ps /\ -. ch ) -> th ) )
4		notnotr	|- ( -. -. ps -> ps )
5	4 1	syl5	|- ( ph -> ( -. -. ps -> th ) )
6		notnotr	|- ( -. -. ch -> ch )
7	6 2	syl5	|- ( ph -> ( -. -. ch -> th ) )
8	5 7 3	ecased	|- ( ph -> th )