Theorem ecase33d

Description: Deduction for elimination by cases. (Contributed by Thierry Arnoux, 5-Jul-2026)

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

Proof

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