Theorem 4cases

Description: Inference eliminating two antecedents from the four possible cases that result from their true/false combinations. (Contributed by NM, 25-Oct-2003)

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

Proof

Step	Hyp	Ref	Expression
1		4cases.1	$$⊢\left(\phi \wedge \psi \right)\to \chi$$
2		4cases.2	$$⊢\left(\phi \wedge \neg \psi \right)\to \chi$$
3		4cases.3	$$⊢\left(\neg \phi \wedge \psi \right)\to \chi$$
4		4cases.4	$$⊢\left(\neg \phi \wedge \neg \psi \right)\to \chi$$
5	1 3	pm2.61ian	$$⊢\psi \to \chi$$
6	2 4	pm2.61ian	$$⊢\neg \psi \to \chi$$
7	5 6	pm2.61i	$$⊢\chi$$