Theorem ccase2

Description: Inference for combining cases. (Contributed by NM, 29-Jul-1999)

	Ref	Expression
Hypotheses	ccase2.1	$$⊢\left(\phi \wedge \psi \right)\to \tau$$
	ccase2.2	$$⊢\chi \to \tau$$
	ccase2.3	$$⊢\theta \to \tau$$
Assertion	ccase2	$$⊢\left(\left(\phi \vee \chi \right)\wedge \left(\psi \vee \theta \right)\right)\to \tau$$

Proof

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