Theorem ccased 913

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 27	. . 3 ⊢ ((ψ ∧ χ) → (φ → η))
3		ccased.2	. . . 4 ⊢ (φ → ((θ ∧ χ) → η))
4	3	com12 27	. . 3 ⊢ ((θ ∧ χ) → (φ → η))
5		ccased.3	. . . 4 ⊢ (φ → ((ψ ∧ τ) → η))
6	5	com12 27	. . 3 ⊢ ((ψ ∧ τ) → (φ → η))
7		ccased.4	. . . 4 ⊢ (φ → ((θ ∧ τ) → η))
8	7	com12 27	. . 3 ⊢ ((θ ∧ τ) → (φ → η))
9	2, 4, 6, 8	ccase 912	. 2 ⊢ (((ψ ∨ θ) ∧ (χ ∨ τ)) → (φ → η))
10	9	com12 27	1 ⊢ (φ → (((ψ ∨ θ) ∧ (χ ∨ τ)) → η))

Syntax hints:   → wi 4   ∨ wo 357   ∧ wa 358

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 177  df-or 359  df-an 360

This theorem is referenced by: (None)