Theorem ccased 1038

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

Hypotheses

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

Assertion

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

Proof of Theorem ccased

Step	Hyp	Ref	Expression
1		ccased.1	. . . 4 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜂))
2	1	com12 32	. . 3 ⊢ ((𝜓 ∧ 𝜒) → (𝜑 → 𝜂))
3		ccased.2	. . . 4 ⊢ (𝜑 → ((𝜃 ∧ 𝜒) → 𝜂))
4	3	com12 32	. . 3 ⊢ ((𝜃 ∧ 𝜒) → (𝜑 → 𝜂))
5		ccased.3	. . . 4 ⊢ (𝜑 → ((𝜓 ∧ 𝜏) → 𝜂))
6	5	com12 32	. . 3 ⊢ ((𝜓 ∧ 𝜏) → (𝜑 → 𝜂))
7		ccased.4	. . . 4 ⊢ (𝜑 → ((𝜃 ∧ 𝜏) → 𝜂))
8	7	com12 32	. . 3 ⊢ ((𝜃 ∧ 𝜏) → (𝜑 → 𝜂))
9	2, 4, 6, 8	ccase 1037	. 2 ⊢ (((𝜓 ∨ 𝜃) ∧ (𝜒 ∨ 𝜏)) → (𝜑 → 𝜂))
10	9	com12 32	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:  fvf1pr  7247  resf1extb  7870  fpwwe2lem12  10540  mulge0  11642  zmulcl  12527  lcmabs  16518  pospo  18251  mulgass  19026  indistopon  22917  lgsdir2lem5  27268  outsideofeq  36195  weiunpo  36530  smprngopr  38112  cdlemg33  40830  monotoddzzfi  43059  acongtr  43095