Theorem ccase

Description: Inference for combining cases. (Contributed by NM, 29-Jul-1999) (Proof shortened by Wolf Lammen, 6-Jan-2013)

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

Proof

Step	Hyp	Ref	Expression
1		ccase.1	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜏 )
2		ccase.2	⊢ ( ( 𝜒 ∧ 𝜓 ) → 𝜏 )
3		ccase.3	⊢ ( ( 𝜑 ∧ 𝜃 ) → 𝜏 )
4		ccase.4	⊢ ( ( 𝜒 ∧ 𝜃 ) → 𝜏 )
5	1 2	jaoian	⊢ ( ( ( 𝜑 ∨ 𝜒 ) ∧ 𝜓 ) → 𝜏 )
6	3 4	jaoian	⊢ ( ( ( 𝜑 ∨ 𝜒 ) ∧ 𝜃 ) → 𝜏 )
7	5 6	jaodan	⊢ ( ( ( 𝜑 ∨ 𝜒 ) ∧ ( 𝜓 ∨ 𝜃 ) ) → 𝜏 )