Theorem ccased 563

Description: Deduction for combining cases.

Hypotheses

Ref	Expression
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

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

Proof of Theorem ccased

Step	Hyp	Ref	Expression
1		ccased.1	. . . 4 |- (ph -> ((ps /\ ch) -> et))
2		ccased.2	. . . 4 |- (ph -> ((th /\ ch) -> et))
3	1, 2	jaod 329	. . 3 |- (ph -> (((ps /\ ch) \/ (th /\ ch)) -> et))
4		ccased.3	. . . 4 |- (ph -> ((ps /\ ta ) -> et))
5		ccased.4	. . . 4 |- (ph -> ((th /\ ta ) -> et))
6	4, 5	jaod 329	. . 3 |- (ph -> (((ps /\ ta ) \/ (th /\ ta )) -> et))
7	3, 6	jaod 329	. 2 |- (ph -> ((((ps /\ ch) \/ (th /\ ch)) \/ ((ps /\ ta ) \/ (th /\ ta ))) -> et))
8		caselem 561	. 2 |- (((ps \/ th) /\ (ch \/ ta )) <-> (((ps /\ ch) \/ (th /\ ch)) \/ ((ps /\ ta ) \/ (th /\ ta ))))
9	7, 8	syl5ib 181	1 |- (ph -> (((ps \/ th) /\ (ch \/ ta )) -> et))

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

This theorem is referenced by:  zaddclt 4590  zmulclt 4596  zltp1let 4597

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