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	⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜒 ) ) → 𝜃 )
	4casesdan.2	⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ ¬ 𝜒 ) ) → 𝜃 )
	4casesdan.3	⊢ ( ( 𝜑 ∧ ( ¬ 𝜓 ∧ 𝜒 ) ) → 𝜃 )
	4casesdan.4	⊢ ( ( 𝜑 ∧ ( ¬ 𝜓 ∧ ¬ 𝜒 ) ) → 𝜃 )
Assertion	4casesdan	⊢ ( 𝜑 → 𝜃 )

Proof

Step	Hyp	Ref	Expression
1		4casesdan.1	⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜒 ) ) → 𝜃 )
2		4casesdan.2	⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ ¬ 𝜒 ) ) → 𝜃 )
3		4casesdan.3	⊢ ( ( 𝜑 ∧ ( ¬ 𝜓 ∧ 𝜒 ) ) → 𝜃 )
4		4casesdan.4	⊢ ( ( 𝜑 ∧ ( ¬ 𝜓 ∧ ¬ 𝜒 ) ) → 𝜃 )
5	1	expcom	⊢ ( ( 𝜓 ∧ 𝜒 ) → ( 𝜑 → 𝜃 ) )
6	2	expcom	⊢ ( ( 𝜓 ∧ ¬ 𝜒 ) → ( 𝜑 → 𝜃 ) )
7	3	expcom	⊢ ( ( ¬ 𝜓 ∧ 𝜒 ) → ( 𝜑 → 𝜃 ) )
8	4	expcom	⊢ ( ( ¬ 𝜓 ∧ ¬ 𝜒 ) → ( 𝜑 → 𝜃 ) )
9	5 6 7 8	4cases	⊢ ( 𝜑 → 𝜃 )