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	$$⊢\left(\phi \wedge \psi \right)\to \tau$$
	ccase.2	$$⊢\left(\chi \wedge \psi \right)\to \tau$$
	ccase.3	$$⊢\left(\phi \wedge \theta \right)\to \tau$$
	ccase.4	$$⊢\left(\chi \wedge \theta \right)\to \tau$$
Assertion	ccase	$$⊢\left(\left(\phi \vee \chi \right)\wedge \left(\psi \vee \theta \right)\right)\to \tau$$

Proof

Step	Hyp	Ref	Expression
1		ccase.1	$$⊢\left(\phi \wedge \psi \right)\to \tau$$
2		ccase.2	$$⊢\left(\chi \wedge \psi \right)\to \tau$$
3		ccase.3	$$⊢\left(\phi \wedge \theta \right)\to \tau$$
4		ccase.4	$$⊢\left(\chi \wedge \theta \right)\to \tau$$
5	1 2	jaoian	$$⊢\left(\left(\phi \vee \chi \right)\wedge \psi \right)\to \tau$$
6	3 4	jaoian	$$⊢\left(\left(\phi \vee \chi \right)\wedge \theta \right)\to \tau$$
7	5 6	jaodan	$$⊢\left(\left(\phi \vee \chi \right)\wedge \left(\psi \vee \theta \right)\right)\to \tau$$