![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cases2 | Structured version Visualization version GIF version |
Description: Case disjunction according to the value of 𝜑. (Contributed by BJ, 6-Apr-2019.) (Proof shortened by Wolf Lammen, 28-Feb-2022.) |
Ref | Expression |
---|---|
cases2 | ⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)) ↔ ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm4.83 1022 | . 2 ⊢ (((𝜑 → ((𝜓 ∧ 𝜑) ∨ (𝜒 ∧ ¬ 𝜑))) ∧ (¬ 𝜑 → ((𝜓 ∧ 𝜑) ∨ (𝜒 ∧ ¬ 𝜑)))) ↔ ((𝜓 ∧ 𝜑) ∨ (𝜒 ∧ ¬ 𝜑))) | |
2 | dedlema 1041 | . . . 4 ⊢ (𝜑 → (𝜓 ↔ ((𝜓 ∧ 𝜑) ∨ (𝜒 ∧ ¬ 𝜑)))) | |
3 | 2 | pm5.74i 274 | . . 3 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → ((𝜓 ∧ 𝜑) ∨ (𝜒 ∧ ¬ 𝜑)))) |
4 | dedlemb 1042 | . . . 4 ⊢ (¬ 𝜑 → (𝜒 ↔ ((𝜓 ∧ 𝜑) ∨ (𝜒 ∧ ¬ 𝜑)))) | |
5 | 4 | pm5.74i 274 | . . 3 ⊢ ((¬ 𝜑 → 𝜒) ↔ (¬ 𝜑 → ((𝜓 ∧ 𝜑) ∨ (𝜒 ∧ ¬ 𝜑)))) |
6 | 3, 5 | anbi12i 629 | . 2 ⊢ (((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒)) ↔ ((𝜑 → ((𝜓 ∧ 𝜑) ∨ (𝜒 ∧ ¬ 𝜑))) ∧ (¬ 𝜑 → ((𝜓 ∧ 𝜑) ∨ (𝜒 ∧ ¬ 𝜑))))) |
7 | ancom 464 | . . 3 ⊢ ((𝜑 ∧ 𝜓) ↔ (𝜓 ∧ 𝜑)) | |
8 | ancom 464 | . . 3 ⊢ ((¬ 𝜑 ∧ 𝜒) ↔ (𝜒 ∧ ¬ 𝜑)) | |
9 | 7, 8 | orbi12i 912 | . 2 ⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)) ↔ ((𝜓 ∧ 𝜑) ∨ (𝜒 ∧ ¬ 𝜑))) |
10 | 1, 6, 9 | 3bitr4ri 307 | 1 ⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)) ↔ ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒))) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 ∨ wo 844 |
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 210 df-an 400 df-or 845 |
This theorem is referenced by: dfbi3 1045 dfifp2 1060 ifval 4466 ifpidg 40199 ifpim123g 40208 |
Copyright terms: Public domain | W3C validator |