Theorem ccase 562

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		caselem 561	. 2 |- (((ph \/ ch) /\ (ps \/ th)) <-> (((ph /\ ps) \/ (ch /\ ps)) \/ ((ph /\ th) \/ (ch /\ th))))
2		ccase.1	. . . 4 |- ((ph /\ ps) -> ta )
3		ccase.2	. . . 4 |- ((ch /\ ps) -> ta )
4	2, 3	jaoi 275	. . 3 |- (((ph /\ ps) \/ (ch /\ ps)) -> ta )
5		ccase.3	. . . 4 |- ((ph /\ th) -> ta )
6		ccase.4	. . . 4 |- ((ch /\ th) -> ta )
7	5, 6	jaoi 275	. . 3 |- (((ph /\ th) \/ (ch /\ th)) -> ta )
8	4, 7	jaoi 275	. 2 |- ((((ph /\ ps) \/ (ch /\ ps)) \/ ((ph /\ th) \/ (ch /\ th))) -> ta )
9	1, 8	sylbi 174	1 |- (((ph \/ ch) /\ (ps \/ th)) -> ta )

Syntax hints:   -> wi 2   \/ wo 195   /\ wa 196

This theorem is referenced by:  ccase2 564  addge0 4324  lt2sq 4414  nn0addclt 4551  nn0ltp1let 4556

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

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198

metamath.org