Theorem ccase 1035

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 954	. 2 ⊢ (((𝜑 ∨ 𝜒) ∧ 𝜓) → 𝜏)
4		ccase.3	. . 3 ⊢ ((𝜑 ∧ 𝜃) → 𝜏)
5		ccase.4	. . 3 ⊢ ((𝜒 ∧ 𝜃) → 𝜏)
6	4, 5	jaoian 954	. 2 ⊢ (((𝜑 ∨ 𝜒) ∧ 𝜃) → 𝜏)
7	3, 6	jaodan 955	1 ⊢ (((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜃)) → 𝜏)

Syntax hints:   → wi 4   ∧ wa 394   ∨ wo 845

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 206  df-an 395  df-or 846

This theorem is referenced by:  ccased  1036  ccase2  1037  ssprsseq  4830  prel12g  4866  injresinjlem  13788  prodmo  15916  nn0gcdsq  16727  symgextf1  19388  cnmsgnsubg  21526  nn0rppwr  42028  nn0expgcd  42030  dvdsexpnn0  42036  zaddcom  42142  zmulcom  42146  kelac2lem  42630  omcl3g  42905