Theorem ccase 1043

Description: Inference for combining cases. (Contributed by NM, 29-Jul-1999.) (Proof shortened by Wolf Lammen, 6-Jan-2013.)

Hypotheses

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

Assertion

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

Proof of Theorem ccase

Step	Hyp	Ref	Expression
1		ccase.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜏)
2		ccase.2	. . 3 ⊢ ((𝜒 ∧ 𝜓) → 𝜏)
3	1, 2	jaoian 964	. 2 ⊢ (((𝜑 ∨ 𝜒) ∧ 𝜓) → 𝜏)
4		ccase.3	. . 3 ⊢ ((𝜑 ∧ 𝜃) → 𝜏)
5		ccase.4	. . 3 ⊢ ((𝜒 ∧ 𝜃) → 𝜏)
6	4, 5	jaoian 964	. 2 ⊢ (((𝜑 ∨ 𝜒) ∧ 𝜃) → 𝜏)
7	3, 6	jaodan 965	1 ⊢ (((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜃)) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 396   ∨ wo 853

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 208  df-an 397  df-or 854

This theorem is referenced by:  ccased  1044  ccase2  1045  ssprsseq  4756  prel12g  4795  injresinjlem  13736  prodmo  15892  nn0rppwr  16521  nn0expgcd  16524  nn0gcdsq  16713  symgextf1  19387  cnmsgnsubg  21552  zseo  28432  dvdsexpnn0  42811  zaddcom  42954  zmulcom  42958  kelac2lem  43509  omcl3g  43779  usgrexmpl2trifr  48528