Theorem 3ecase

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

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

Proof

Step	Hyp	Ref	Expression
1		3ecase.1	$$⊢\neg \phi \to \theta$$
2		3ecase.2	$$⊢\neg \psi \to \theta$$
3		3ecase.3	$$⊢\neg \chi \to \theta$$
4		3ecase.4	$$⊢\left(\phi \wedge \psi \wedge \chi \right)\to \theta$$
5	4	3exp	$$⊢\phi \to \left(\psi \to \left(\chi \to \theta \right)\right)$$
6	1	2a1d	$$⊢\neg \phi \to \left(\psi \to \left(\chi \to \theta \right)\right)$$
7	5 6	pm2.61i	$$⊢\psi \to \left(\chi \to \theta \right)$$
8	7 2 3	pm2.61nii	$$⊢\theta$$