Theorem ccased

Description: Deduction for combining cases. (Contributed by NM, 9-May-2004)

	Ref	Expression
Hypotheses	ccased.1	⊢ ( 𝜑 → ( ( 𝜓 ∧ 𝜒 ) → 𝜂 ) )
	ccased.2	⊢ ( 𝜑 → ( ( 𝜃 ∧ 𝜒 ) → 𝜂 ) )
	ccased.3	⊢ ( 𝜑 → ( ( 𝜓 ∧ 𝜏 ) → 𝜂 ) )
	ccased.4	⊢ ( 𝜑 → ( ( 𝜃 ∧ 𝜏 ) → 𝜂 ) )
Assertion	ccased	⊢ ( 𝜑 → ( ( ( 𝜓 ∨ 𝜃 ) ∧ ( 𝜒 ∨ 𝜏 ) ) → 𝜂 ) )

Proof

Step	Hyp	Ref	Expression
1		ccased.1	⊢ ( 𝜑 → ( ( 𝜓 ∧ 𝜒 ) → 𝜂 ) )
2		ccased.2	⊢ ( 𝜑 → ( ( 𝜃 ∧ 𝜒 ) → 𝜂 ) )
3		ccased.3	⊢ ( 𝜑 → ( ( 𝜓 ∧ 𝜏 ) → 𝜂 ) )
4		ccased.4	⊢ ( 𝜑 → ( ( 𝜃 ∧ 𝜏 ) → 𝜂 ) )
5	1	com12	⊢ ( ( 𝜓 ∧ 𝜒 ) → ( 𝜑 → 𝜂 ) )
6	2	com12	⊢ ( ( 𝜃 ∧ 𝜒 ) → ( 𝜑 → 𝜂 ) )
7	3	com12	⊢ ( ( 𝜓 ∧ 𝜏 ) → ( 𝜑 → 𝜂 ) )
8	4	com12	⊢ ( ( 𝜃 ∧ 𝜏 ) → ( 𝜑 → 𝜂 ) )
9	5 6 7 8	ccase	⊢ ( ( ( 𝜓 ∨ 𝜃 ) ∧ ( 𝜒 ∨ 𝜏 ) ) → ( 𝜑 → 𝜂 ) )
10	9	com12	⊢ ( 𝜑 → ( ( ( 𝜓 ∨ 𝜃 ) ∧ ( 𝜒 ∨ 𝜏 ) ) → 𝜂 ) )