Theorem ccased

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

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

Proof

Step	Hyp	Ref	Expression
1		ccased.1	|- ( ph -> ( ( ps /\ ch ) -> et ) )
2		ccased.2	|- ( ph -> ( ( th /\ ch ) -> et ) )
3		ccased.3	|- ( ph -> ( ( ps /\ ta ) -> et ) )
4		ccased.4	|- ( ph -> ( ( th /\ ta ) -> et ) )
5	1	com12	|- ( ( ps /\ ch ) -> ( ph -> et ) )
6	2	com12	|- ( ( th /\ ch ) -> ( ph -> et ) )
7	3	com12	|- ( ( ps /\ ta ) -> ( ph -> et ) )
8	4	com12	|- ( ( th /\ ta ) -> ( ph -> et ) )
9	5 6 7 8	ccase	|- ( ( ( ps \/ th ) /\ ( ch \/ ta ) ) -> ( ph -> et ) )
10	9	com12	|- ( ph -> ( ( ( ps \/ th ) /\ ( ch \/ ta ) ) -> et ) )