Theorem ccased 563

Description: Deduction for combining cases.

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		ccased.2	. . . 4 ⊢ (φ → ((θ ∧ χ) → η))
3	1, 2	jaod 329	. . 3 ⊢ (φ → (((ψ ∧ χ) ∨ (θ ∧ χ)) → η))
4		ccased.3	. . . 4 ⊢ (φ → ((ψ ∧ τ) → η))
5		ccased.4	. . . 4 ⊢ (φ → ((θ ∧ τ) → η))
6	4, 5	jaod 329	. . 3 ⊢ (φ → (((ψ ∧ τ) ∨ (θ ∧ τ)) → η))
7	3, 6	jaod 329	. 2 ⊢ (φ → ((((ψ ∧ χ) ∨ (θ ∧ χ)) ∨ ((ψ ∧ τ) ∨ (θ ∧ τ))) → η))
8		caselem 561	. 2 ⊢ (((ψ ∨ θ) ∧ (χ ∨ τ)) ↔ (((ψ ∧ χ) ∨ (θ ∧ χ)) ∨ ((ψ ∧ τ) ∨ (θ ∧ τ))))
9	7, 8	syl5ib 181	1 ⊢ (φ → (((ψ ∨ θ) ∧ (χ ∨ τ)) → η))

Syntax hints:   → wi 2   ∨ wo 195   ∧ wa 196

This theorem is referenced by:  zaddclt 4590  zmulclt 4596  zltp1let 4597

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

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198

metamath.org