Theorem ecase3ad

Description: Deduction for elimination by cases. (Contributed by NM, 24-May-2013) (Proof shortened by Wolf Lammen, 20-Sep-2024)

	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	1	imp	|- ( ( ph /\ ps ) -> th )
5	2	imp	|- ( ( ph /\ ch ) -> th )
6	3	imp	|- ( ( ph /\ ( -. ps /\ -. ch ) ) -> th )
7	4 5 6	pm2.61ddan	|- ( ph -> th )