Theorem ccase 755

Description: Inference for combining cases.

Hypotheses

Ref	Expression
ccase.1	|- ((ph /\ ps) -> ta)
ccase.2	|- ((ch /\ ps) -> ta)
ccase.3	|- ((ph /\ th) -> ta)
ccase.4	|- ((ch /\ th) -> ta)

Assertion

Ref	Expression
ccase	|- (((ph \/ ch) /\ (ps \/ th)) -> ta)

Proof of Theorem ccase

Step	Hyp	Ref	Expression
1		anddi 607	. . 3 |- (((ph \/ ch) /\ (ps \/ th)) <-> (((ph /\ ps) \/ (ph /\ th)) \/ ((ch /\ ps) \/ (ch /\ th))))
2		or4 264	. . 3 |- ((((ph /\ ps) \/ (ph /\ th)) \/ ((ch /\ ps) \/ (ch /\ th))) <-> (((ph /\ ps) \/ (ch /\ ps)) \/ ((ph /\ th) \/ (ch /\ th))))
3	1, 2	bitr 173	. 2 |- (((ph \/ ch) /\ (ps \/ th)) <-> (((ph /\ ps) \/ (ch /\ ps)) \/ ((ph /\ th) \/ (ch /\ th))))
4		ccase.1	. . . 4 |- ((ph /\ ps) -> ta)
5		ccase.2	. . . 4 |- ((ch /\ ps) -> ta)
6	4, 5	jaoi 341	. . 3 |- (((ph /\ ps) \/ (ch /\ ps)) -> ta)
7		ccase.3	. . . 4 |- ((ph /\ th) -> ta)
8		ccase.4	. . . 4 |- ((ch /\ th) -> ta)
9	7, 8	jaoi 341	. . 3 |- (((ph /\ th) \/ (ch /\ th)) -> ta)
10	6, 9	jaoi 341	. 2 |- ((((ph /\ ps) \/ (ch /\ ps)) \/ ((ph /\ th) \/ (ch /\ th))) -> ta)
11	3, 10	sylbi 199	1 |- (((ph \/ ch) /\ (ps \/ th)) -> ta)

Syntax hints:   -> wi 3   \/ wo 222   /\ wa 223

This theorem is referenced by:  ccase2 757  addge0 5599  lt2msq 5881  nn0addclt 6120  nn0ltp1let 6127  bccl2t 6971  efif1lem5 8734  efif1lem7 8736

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225

Copyright terms: Public domain