Theorem ecase33d

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

	Ref	Expression
Hypotheses	ecase33d.1	⊢ ( 𝜑 → ¬ 𝜓 )
	ecase33d.2	⊢ ( 𝜑 → ¬ 𝜒 )
	ecase33d.3	⊢ ( 𝜑 → ( 𝜓 ∨ 𝜒 ∨ 𝜃 ) )
Assertion	ecase33d	⊢ ( 𝜑 → 𝜃 )

Proof

Step	Hyp	Ref	Expression
1		ecase33d.1	⊢ ( 𝜑 → ¬ 𝜓 )
2		ecase33d.2	⊢ ( 𝜑 → ¬ 𝜒 )
3		ecase33d.3	⊢ ( 𝜑 → ( 𝜓 ∨ 𝜒 ∨ 𝜃 ) )
4		df-3or	⊢ ( ( 𝜓 ∨ 𝜒 ∨ 𝜃 ) ↔ ( ( 𝜓 ∨ 𝜒 ) ∨ 𝜃 ) )
5	3 4	sylib	⊢ ( 𝜑 → ( ( 𝜓 ∨ 𝜒 ) ∨ 𝜃 ) )
6		ioran	⊢ ( ¬ ( 𝜓 ∨ 𝜒 ) ↔ ( ¬ 𝜓 ∧ ¬ 𝜒 ) )
7	1 2 6	sylanbrc	⊢ ( 𝜑 → ¬ ( 𝜓 ∨ 𝜒 ) )
8	5 7	orcnd	⊢ ( 𝜑 → 𝜃 )