Theorem ecase

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

	Ref	Expression
Hypotheses	ecase.1	$$⊢\neg \phi \to \chi$$
	ecase.2	$$⊢\neg \psi \to \chi$$
	ecase.3	$$⊢\left(\phi \wedge \psi \right)\to \chi$$
Assertion	ecase	$$⊢\chi$$

Proof

Step	Hyp	Ref	Expression
1		ecase.1	$$⊢\neg \phi \to \chi$$
2		ecase.2	$$⊢\neg \psi \to \chi$$
3		ecase.3	$$⊢\left(\phi \wedge \psi \right)\to \chi$$
4	3	ex	$$⊢\phi \to \left(\psi \to \chi \right)$$
5	4 1 2	pm2.61nii	$$⊢\chi$$