Theorem ccase 1037

Description: Inference for combining cases. (Contributed by NM, 29-Jul-1999.) (Proof shortened by Wolf Lammen, 6-Jan-2013.)

Hypotheses

Ref	Expression
ccase.1	⊢ ((𝜑 ∧ 𝜓) → 𝜏)
ccase.2	⊢ ((𝜒 ∧ 𝜓) → 𝜏)
ccase.3	⊢ ((𝜑 ∧ 𝜃) → 𝜏)
ccase.4	⊢ ((𝜒 ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
ccase	⊢ (((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜃)) → 𝜏)

Proof of Theorem ccase

Step	Hyp	Ref	Expression
1		ccase.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜏)
2		ccase.2	. . 3 ⊢ ((𝜒 ∧ 𝜓) → 𝜏)
3	1, 2	jaoian 958	. 2 ⊢ (((𝜑 ∨ 𝜒) ∧ 𝜓) → 𝜏)
4		ccase.3	. . 3 ⊢ ((𝜑 ∧ 𝜃) → 𝜏)
5		ccase.4	. . 3 ⊢ ((𝜒 ∧ 𝜃) → 𝜏)
6	4, 5	jaoian 958	. 2 ⊢ (((𝜑 ∨ 𝜒) ∧ 𝜃) → 𝜏)
7	3, 6	jaodan 959	1 ⊢ (((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜃)) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 847

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848

This theorem is referenced by:  ccased  1038  ccase2  1039  ssprsseq  4805  prel12g  4844  injresinjlem  13808  prodmo  15955  nn0rppwr  16581  nn0expgcd  16584  nn0gcdsq  16772  symgextf1  19408  cnmsgnsubg  21550  zseo  28343  dvdsexpnn0  42348  zaddcom  42461  zmulcom  42465  kelac2lem  43054  omcl3g  43324  usgrexmpl2trifr  47969