Theorem ccased 1054

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 33	. . 3 ⊢ ((𝜓 ∧ 𝜒) → (𝜑 → 𝜂))
3		ccased.2	. . . 4 ⊢ (𝜑 → ((𝜃 ∧ 𝜒) → 𝜂))
4	3	com12 33	. . 3 ⊢ ((𝜃 ∧ 𝜒) → (𝜑 → 𝜂))
5		ccased.3	. . . 4 ⊢ (𝜑 → ((𝜓 ∧ 𝜏) → 𝜂))
6	5	com12 33	. . 3 ⊢ ((𝜓 ∧ 𝜏) → (𝜑 → 𝜂))
7		ccased.4	. . . 4 ⊢ (𝜑 → ((𝜃 ∧ 𝜏) → 𝜂))
8	7	com12 33	. . 3 ⊢ ((𝜃 ∧ 𝜏) → (𝜑 → 𝜂))
9	2, 4, 6, 8	ccase 1053	. 2 ⊢ (((𝜓 ∨ 𝜃) ∧ (𝜒 ∨ 𝜏)) → (𝜑 → 𝜂))
10	9	com12 33	1 ⊢ (𝜑 → (((𝜓 ∨ 𝜃) ∧ (𝜒 ∨ 𝜏)) → 𝜂))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862

This theorem is used by:  fvf1pr  7316  resf1extb  7940  fpwwe2lem12  10645  mulge0  11750  zmulcl  12661  lcmabs  16688  pospo  18424  mulgass  19208  indistopon  23195  lgsdir2lem5  27530  outsideofeq  36642  weiunpo  37016  smprngopr  38743  cdlemg33  41525  monotoddzzfi  43709  acongtr  43745  smprngprmrng  49144