|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > ccase | Structured version Visualization version GIF version | ||
| Description: Inference for combining cases. (Contributed by NM, 29-Jul-1999.) (Proof shortened by Wolf Lammen, 6-Jan-2013.) | 
| Ref | Expression | 
|---|---|
| ccase.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝜏) | 
| ccase.2 | ⊢ ((𝜒 ∧ 𝜓) → 𝜏) | 
| ccase.3 | ⊢ ((𝜑 ∧ 𝜃) → 𝜏) | 
| ccase.4 | ⊢ ((𝜒 ∧ 𝜃) → 𝜏) | 
| Ref | Expression | 
|---|---|
| ccase | ⊢ (((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜃)) → 𝜏) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | ccase.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜏) | |
| 2 | ccase.2 | . . 3 ⊢ ((𝜒 ∧ 𝜓) → 𝜏) | |
| 3 | 1, 2 | jaoian 958 | . 2 ⊢ (((𝜑 ∨ 𝜒) ∧ 𝜓) → 𝜏) | 
| 4 | ccase.3 | . . 3 ⊢ ((𝜑 ∧ 𝜃) → 𝜏) | |
| 5 | ccase.4 | . . 3 ⊢ ((𝜒 ∧ 𝜃) → 𝜏) | |
| 6 | 4, 5 | jaoian 958 | . 2 ⊢ (((𝜑 ∨ 𝜒) ∧ 𝜃) → 𝜏) | 
| 7 | 3, 6 | jaodan 959 | 1 ⊢ (((𝜑 ∨ 𝜒) ∧ (𝜓 ∨ 𝜃)) → 𝜏) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 ∨ wo 847 | 
| 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 207 df-an 396 df-or 848 | 
| This theorem is referenced by: ccased 1038 ccase2 1039 ssprsseq 4824 prel12g 4863 injresinjlem 13827 prodmo 15973 nn0rppwr 16599 nn0expgcd 16602 nn0gcdsq 16790 symgextf1 19440 cnmsgnsubg 21596 zseo 28407 dvdsexpnn0 42374 zaddcom 42487 zmulcom 42491 kelac2lem 43081 omcl3g 43352 usgrexmpl2trifr 48001 | 
| Copyright terms: Public domain | W3C validator |