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  7241  resf1extb  7864  fpwwe2lem12  10530  mulge0  11632  zmulcl  12518  lcmabs  16513  pospo  18246  mulgass  19021  indistopon  22914  lgsdir2lem5  27265  outsideofeq  36163  weiunpo  36498  smprngopr  38091  cdlemg33  40749  monotoddzzfi  42974  acongtr  43010