Proof of Theorem df3nandALT1
Step | Hyp | Ref
| Expression |
1 | | iman 405 |
. . 3
⊢ ((𝜑 → ((𝜓 ⊼ 𝜒) ∧ (𝜓 ⊼ 𝜒))) ↔ ¬ (𝜑 ∧ ¬ ((𝜓 ⊼ 𝜒) ∧ (𝜓 ⊼ 𝜒)))) |
2 | | imnan 403 |
. . . . . . . 8
⊢ ((𝜓 → ¬ 𝜒) ↔ ¬ (𝜓 ∧ 𝜒)) |
3 | 2 | biimpi 219 |
. . . . . . 7
⊢ ((𝜓 → ¬ 𝜒) → ¬ (𝜓 ∧ 𝜒)) |
4 | 3, 3 | jca 515 |
. . . . . 6
⊢ ((𝜓 → ¬ 𝜒) → (¬ (𝜓 ∧ 𝜒) ∧ ¬ (𝜓 ∧ 𝜒))) |
5 | 2 | biimpri 231 |
. . . . . . 7
⊢ (¬
(𝜓 ∧ 𝜒) → (𝜓 → ¬ 𝜒)) |
6 | 5 | adantl 485 |
. . . . . 6
⊢ ((¬
(𝜓 ∧ 𝜒) ∧ ¬ (𝜓 ∧ 𝜒)) → (𝜓 → ¬ 𝜒)) |
7 | 4, 6 | impbii 212 |
. . . . 5
⊢ ((𝜓 → ¬ 𝜒) ↔ (¬ (𝜓 ∧ 𝜒) ∧ ¬ (𝜓 ∧ 𝜒))) |
8 | | df-nan 1488 |
. . . . . 6
⊢ ((𝜓 ⊼ 𝜒) ↔ ¬ (𝜓 ∧ 𝜒)) |
9 | 8, 8 | anbi12i 630 |
. . . . 5
⊢ (((𝜓 ⊼ 𝜒) ∧ (𝜓 ⊼ 𝜒)) ↔ (¬ (𝜓 ∧ 𝜒) ∧ ¬ (𝜓 ∧ 𝜒))) |
10 | 7, 9 | bitr4i 281 |
. . . 4
⊢ ((𝜓 → ¬ 𝜒) ↔ ((𝜓 ⊼ 𝜒) ∧ (𝜓 ⊼ 𝜒))) |
11 | 10 | imbi2i 339 |
. . 3
⊢ ((𝜑 → (𝜓 → ¬ 𝜒)) ↔ (𝜑 → ((𝜓 ⊼ 𝜒) ∧ (𝜓 ⊼ 𝜒)))) |
12 | | df-nan 1488 |
. . . . 5
⊢ (((𝜓 ⊼ 𝜒) ⊼ (𝜓 ⊼ 𝜒)) ↔ ¬ ((𝜓 ⊼ 𝜒) ∧ (𝜓 ⊼ 𝜒))) |
13 | 12 | anbi2i 626 |
. . . 4
⊢ ((𝜑 ∧ ((𝜓 ⊼ 𝜒) ⊼ (𝜓 ⊼ 𝜒))) ↔ (𝜑 ∧ ¬ ((𝜓 ⊼ 𝜒) ∧ (𝜓 ⊼ 𝜒)))) |
14 | 13 | notbii 323 |
. . 3
⊢ (¬
(𝜑 ∧ ((𝜓 ⊼ 𝜒) ⊼ (𝜓 ⊼ 𝜒))) ↔ ¬ (𝜑 ∧ ¬ ((𝜓 ⊼ 𝜒) ∧ (𝜓 ⊼ 𝜒)))) |
15 | 1, 11, 14 | 3bitr4i 306 |
. 2
⊢ ((𝜑 → (𝜓 → ¬ 𝜒)) ↔ ¬ (𝜑 ∧ ((𝜓 ⊼ 𝜒) ⊼ (𝜓 ⊼ 𝜒)))) |
16 | | df-3nand 34324 |
. 2
⊢ ((𝜑 ⊼ 𝜓 ⊼ 𝜒) ↔ (𝜑 → (𝜓 → ¬ 𝜒))) |
17 | | df-nan 1488 |
. 2
⊢ ((𝜑 ⊼ ((𝜓 ⊼ 𝜒) ⊼ (𝜓 ⊼ 𝜒))) ↔ ¬ (𝜑 ∧ ((𝜓 ⊼ 𝜒) ⊼ (𝜓 ⊼ 𝜒)))) |
18 | 15, 16, 17 | 3bitr4i 306 |
1
⊢ ((𝜑 ⊼ 𝜓 ⊼ 𝜒) ↔ (𝜑 ⊼ ((𝜓 ⊼ 𝜒) ⊼ (𝜓 ⊼ 𝜒)))) |