![]() |
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 4830 prel12g 4869 injresinjlem 13823 prodmo 15969 nn0rppwr 16595 nn0expgcd 16598 nn0gcdsq 16786 symgextf1 19454 cnmsgnsubg 21613 zseo 28421 dvdsexpnn0 42348 zaddcom 42459 zmulcom 42463 kelac2lem 43053 omcl3g 43324 usgrexmpl2trifr 47932 |
Copyright terms: Public domain | W3C validator |