Theorem ecased

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

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

Proof

Step	Hyp	Ref	Expression
1		ecased.1	⊢ ( 𝜑 → ( ¬ 𝜓 → 𝜃 ) )
2		ecased.2	⊢ ( 𝜑 → ( ¬ 𝜒 → 𝜃 ) )
3		ecased.3	⊢ ( 𝜑 → ( ( 𝜓 ∧ 𝜒 ) → 𝜃 ) )
4		pm3.11	⊢ ( ¬ ( ¬ 𝜓 ∨ ¬ 𝜒 ) → ( 𝜓 ∧ 𝜒 ) )
5	4 3	syl5	⊢ ( 𝜑 → ( ¬ ( ¬ 𝜓 ∨ ¬ 𝜒 ) → 𝜃 ) )
6	1 2 5	ecase3d	⊢ ( 𝜑 → 𝜃 )