Metamath Proof Explorer

Theorem 4casesdan

Description: Deduction eliminating two antecedents from the four possible cases that result from their true/false combinations. (Contributed by NM, 19-Mar-2013)

		Ref	Expression
	Hypotheses	4casesdan.1	$⊢ (φ \land (ψ \land χ)) \to θ$
		4casesdan.2	$⊢ (φ \land (ψ \land \neg χ)) \to θ$
		4casesdan.3	$⊢ (φ \land (\neg ψ \land χ)) \to θ$
		4casesdan.4	$⊢ (φ \land (\neg ψ \land \neg χ)) \to θ$
	Assertion	4casesdan	$⊢ φ \to θ$

Proof

Step	Hyp	Ref	Expression
1		4casesdan.1	$⊢ (φ \land (ψ \land χ)) \to θ$
2		4casesdan.2	$⊢ (φ \land (ψ \land \neg χ)) \to θ$
3		4casesdan.3	$⊢ (φ \land (\neg ψ \land χ)) \to θ$
4		4casesdan.4	$⊢ (φ \land (\neg ψ \land \neg χ)) \to θ$
5	1	expcom	$⊢ (ψ \land χ) \to (φ \to θ)$
6	2	expcom	$⊢ (ψ \land \neg χ) \to (φ \to θ)$
7	3	expcom	$⊢ (\neg ψ \land χ) \to (φ \to θ)$
8	4	expcom	$⊢ (\neg ψ \land \neg χ) \to (φ \to θ)$
9	5 6 7 8	4cases	$⊢ φ \to θ$