Theorem 3ecase

Description: Inference for elimination by cases. (Contributed by NM, 13-Jul-2005)

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

Proof

Step	Hyp	Ref	Expression
1		3ecase.1	⊢ ( ¬ 𝜑 → 𝜃 )
2		3ecase.2	⊢ ( ¬ 𝜓 → 𝜃 )
3		3ecase.3	⊢ ( ¬ 𝜒 → 𝜃 )
4		3ecase.4	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → 𝜃 )
5	4	3exp	⊢ ( 𝜑 → ( 𝜓 → ( 𝜒 → 𝜃 ) ) )
6	1	2a1d	⊢ ( ¬ 𝜑 → ( 𝜓 → ( 𝜒 → 𝜃 ) ) )
7	5 6	pm2.61i	⊢ ( 𝜓 → ( 𝜒 → 𝜃 ) )
8	7 2 3	pm2.61nii	⊢ 𝜃