| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > ccased | Structured version Visualization version GIF version | ||
| Description: Deduction for combining cases. (Contributed by NM, 9-May-2004.) |
| Ref | Expression |
|---|---|
| ccased.1 | ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜂)) |
| ccased.2 | ⊢ (𝜑 → ((𝜃 ∧ 𝜒) → 𝜂)) |
| ccased.3 | ⊢ (𝜑 → ((𝜓 ∧ 𝜏) → 𝜂)) |
| ccased.4 | ⊢ (𝜑 → ((𝜃 ∧ 𝜏) → 𝜂)) |
| Ref | Expression |
|---|---|
| ccased | ⊢ (𝜑 → (((𝜓 ∨ 𝜃) ∧ (𝜒 ∨ 𝜏)) → 𝜂)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ccased.1 | . . . 4 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜂)) | |
| 2 | 1 | com12 32 | . . 3 ⊢ ((𝜓 ∧ 𝜒) → (𝜑 → 𝜂)) |
| 3 | ccased.2 | . . . 4 ⊢ (𝜑 → ((𝜃 ∧ 𝜒) → 𝜂)) | |
| 4 | 3 | com12 32 | . . 3 ⊢ ((𝜃 ∧ 𝜒) → (𝜑 → 𝜂)) |
| 5 | ccased.3 | . . . 4 ⊢ (𝜑 → ((𝜓 ∧ 𝜏) → 𝜂)) | |
| 6 | 5 | com12 32 | . . 3 ⊢ ((𝜓 ∧ 𝜏) → (𝜑 → 𝜂)) |
| 7 | ccased.4 | . . . 4 ⊢ (𝜑 → ((𝜃 ∧ 𝜏) → 𝜂)) | |
| 8 | 7 | com12 32 | . . 3 ⊢ ((𝜃 ∧ 𝜏) → (𝜑 → 𝜂)) |
| 9 | 2, 4, 6, 8 | ccase 1038 | . 2 ⊢ (((𝜓 ∨ 𝜃) ∧ (𝜒 ∨ 𝜏)) → (𝜑 → 𝜂)) |
| 10 | 9 | com12 32 | 1 ⊢ (𝜑 → (((𝜓 ∨ 𝜃) ∧ (𝜒 ∨ 𝜏)) → 𝜂)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∨ wo 848 |
| 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 849 |
| This theorem is referenced by: fvf1pr 7327 resf1extb 7956 fpwwe2lem12 10682 mulge0 11781 zmulcl 12666 lcmabs 16642 pospo 18390 mulgass 19129 indistopon 23008 lgsdir2lem5 27373 outsideofeq 36131 weiunpo 36466 smprngopr 38059 cdlemg33 40713 monotoddzzfi 42954 acongtr 42990 |
| Copyright terms: Public domain | W3C validator |