Theorem ccase2

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

	Ref	Expression
Hypotheses	ccase2.1	|- ( ( ph /\ ps ) -> ta )
	ccase2.2	|- ( ch -> ta )
	ccase2.3	|- ( th -> ta )
Assertion	ccase2	|- ( ( ( ph \/ ch ) /\ ( ps \/ th ) ) -> ta )

Proof

Step	Hyp	Ref	Expression
1		ccase2.1	|- ( ( ph /\ ps ) -> ta )
2		ccase2.2	|- ( ch -> ta )
3		ccase2.3	|- ( th -> ta )
4	2	adantr	|- ( ( ch /\ ps ) -> ta )
5	3	adantl	|- ( ( ph /\ th ) -> ta )
6	3	adantl	|- ( ( ch /\ th ) -> ta )
7	1 4 5 6	ccase	|- ( ( ( ph \/ ch ) /\ ( ps \/ th ) ) -> ta )