This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ (φ \land ψ) \to χ$
	4cases.2	$⊢ (φ \land \neg ψ) \to χ$
	4cases.3	$⊢ (\neg φ \land ψ) \to χ$
	4cases.4	$⊢ (\neg φ \land \neg ψ) \to χ$
Assertion	4cases	$⊢ χ$

Proof

Step	Hyp	Ref	Expression
1		4cases.1	$⊢ (φ \land ψ) \to χ$
2		4cases.2	$⊢ (φ \land \neg ψ) \to χ$
3		4cases.3	$⊢ (\neg φ \land ψ) \to χ$
4		4cases.4	$⊢ (\neg φ \land \neg ψ) \to χ$
5	1 3	pm2.61ian	$⊢ ψ \to χ$
6	2 4	pm2.61ian	$⊢ \neg ψ \to χ$
7	5 6	pm2.61i	$⊢ χ$