Mathbox for Richard Penner |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > ifpnot23 | Structured version Visualization version GIF version |
Description: Negation of conditional logical operator. (Contributed by RP, 18-Apr-2020.) |
Ref | Expression |
---|---|
ifpnot23 | ⊢ (¬ if-(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, ¬ 𝜓, ¬ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ianor 975 | . . . 4 ⊢ (¬ (𝜑 ∧ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓)) | |
2 | pm4.55 981 | . . . 4 ⊢ (¬ (¬ 𝜑 ∧ 𝜒) ↔ (𝜑 ∨ ¬ 𝜒)) | |
3 | 1, 2 | anbi12i 626 | . . 3 ⊢ ((¬ (𝜑 ∧ 𝜓) ∧ ¬ (¬ 𝜑 ∧ 𝜒)) ↔ ((¬ 𝜑 ∨ ¬ 𝜓) ∧ (𝜑 ∨ ¬ 𝜒))) |
4 | ioran 977 | . . 3 ⊢ (¬ ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)) ↔ (¬ (𝜑 ∧ 𝜓) ∧ ¬ (¬ 𝜑 ∧ 𝜒))) | |
5 | dfifp4 1058 | . . 3 ⊢ (if-(𝜑, ¬ 𝜓, ¬ 𝜒) ↔ ((¬ 𝜑 ∨ ¬ 𝜓) ∧ (𝜑 ∨ ¬ 𝜒))) | |
6 | 3, 4, 5 | 3bitr4i 304 | . 2 ⊢ (¬ ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)) ↔ if-(𝜑, ¬ 𝜓, ¬ 𝜒)) |
7 | df-ifp 1055 | . 2 ⊢ (if-(𝜑, 𝜓, 𝜒) ↔ ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒))) | |
8 | 6, 7 | xchnxbir 334 | 1 ⊢ (¬ if-(𝜑, 𝜓, 𝜒) ↔ if-(𝜑, ¬ 𝜓, ¬ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 207 ∧ wa 396 ∨ wo 841 if-wif 1054 |
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 208 df-an 397 df-or 842 df-ifp 1055 |
This theorem is referenced by: ifpnotnotb 39723 ifpnorcor 39724 ifpnancor 39725 ifpnot23b 39726 ifpnot23c 39728 ifpnot23d 39729 ifpdfnan 39730 ifpdfxor 39731 ifpor123g 39752 |
Copyright terms: Public domain | W3C validator |