Proof of Theorem xordidc
Step | Hyp | Ref
| Expression |
1 | | dcbi 921 |
. . . . 5
⊢
(DECID 𝜓 → (DECID 𝜒 → DECID
(𝜓 ↔ 𝜒))) |
2 | 1 | imp 123 |
. . . 4
⊢
((DECID 𝜓 ∧ DECID 𝜒) → DECID (𝜓 ↔ 𝜒)) |
3 | | annimdc 922 |
. . . . . 6
⊢
(DECID 𝜑 → (DECID (𝜓 ↔ 𝜒) → ((𝜑 ∧ ¬ (𝜓 ↔ 𝜒)) ↔ ¬ (𝜑 → (𝜓 ↔ 𝜒))))) |
4 | 3 | imp 123 |
. . . . 5
⊢
((DECID 𝜑 ∧ DECID (𝜓 ↔ 𝜒)) → ((𝜑 ∧ ¬ (𝜓 ↔ 𝜒)) ↔ ¬ (𝜑 → (𝜓 ↔ 𝜒)))) |
5 | | pm5.32 449 |
. . . . . 6
⊢ ((𝜑 → (𝜓 ↔ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒))) |
6 | 5 | notbii 658 |
. . . . 5
⊢ (¬
(𝜑 → (𝜓 ↔ 𝜒)) ↔ ¬ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒))) |
7 | 4, 6 | bitrdi 195 |
. . . 4
⊢
((DECID 𝜑 ∧ DECID (𝜓 ↔ 𝜒)) → ((𝜑 ∧ ¬ (𝜓 ↔ 𝜒)) ↔ ¬ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒)))) |
8 | 2, 7 | sylan2 284 |
. . 3
⊢
((DECID 𝜑 ∧ (DECID 𝜓 ∧ DECID 𝜒)) → ((𝜑 ∧ ¬ (𝜓 ↔ 𝜒)) ↔ ¬ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒)))) |
9 | | xornbidc 1373 |
. . . . . 6
⊢
(DECID 𝜓 → (DECID 𝜒 → ((𝜓 ⊻ 𝜒) ↔ ¬ (𝜓 ↔ 𝜒)))) |
10 | 9 | imp 123 |
. . . . 5
⊢
((DECID 𝜓 ∧ DECID 𝜒) → ((𝜓 ⊻ 𝜒) ↔ ¬ (𝜓 ↔ 𝜒))) |
11 | 10 | adantl 275 |
. . . 4
⊢
((DECID 𝜑 ∧ (DECID 𝜓 ∧ DECID 𝜒)) → ((𝜓 ⊻ 𝜒) ↔ ¬ (𝜓 ↔ 𝜒))) |
12 | 11 | anbi2d 460 |
. . 3
⊢
((DECID 𝜑 ∧ (DECID 𝜓 ∧ DECID 𝜒)) → ((𝜑 ∧ (𝜓 ⊻ 𝜒)) ↔ (𝜑 ∧ ¬ (𝜓 ↔ 𝜒)))) |
13 | | dcan 919 |
. . . . . 6
⊢
(DECID 𝜑 → (DECID 𝜓 → DECID
(𝜑 ∧ 𝜓))) |
14 | 13 | imp 123 |
. . . . 5
⊢
((DECID 𝜑 ∧ DECID 𝜓) → DECID (𝜑 ∧ 𝜓)) |
15 | 14 | adantrr 471 |
. . . 4
⊢
((DECID 𝜑 ∧ (DECID 𝜓 ∧ DECID 𝜒)) → DECID (𝜑 ∧ 𝜓)) |
16 | | dcan 919 |
. . . . . 6
⊢
(DECID 𝜑 → (DECID 𝜒 → DECID
(𝜑 ∧ 𝜒))) |
17 | 16 | imp 123 |
. . . . 5
⊢
((DECID 𝜑 ∧ DECID 𝜒) → DECID (𝜑 ∧ 𝜒)) |
18 | 17 | adantrl 470 |
. . . 4
⊢
((DECID 𝜑 ∧ (DECID 𝜓 ∧ DECID 𝜒)) → DECID (𝜑 ∧ 𝜒)) |
19 | | xornbidc 1373 |
. . . 4
⊢
(DECID (𝜑 ∧ 𝜓) → (DECID (𝜑 ∧ 𝜒) → (((𝜑 ∧ 𝜓) ⊻ (𝜑 ∧ 𝜒)) ↔ ¬ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒))))) |
20 | 15, 18, 19 | sylc 62 |
. . 3
⊢
((DECID 𝜑 ∧ (DECID 𝜓 ∧ DECID 𝜒)) → (((𝜑 ∧ 𝜓) ⊻ (𝜑 ∧ 𝜒)) ↔ ¬ ((𝜑 ∧ 𝜓) ↔ (𝜑 ∧ 𝜒)))) |
21 | 8, 12, 20 | 3bitr4d 219 |
. 2
⊢
((DECID 𝜑 ∧ (DECID 𝜓 ∧ DECID 𝜒)) → ((𝜑 ∧ (𝜓 ⊻ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ⊻ (𝜑 ∧ 𝜒)))) |
22 | 21 | exp32 363 |
1
⊢
(DECID 𝜑 → (DECID 𝜓 → (DECID
𝜒 → ((𝜑 ∧ (𝜓 ⊻ 𝜒)) ↔ ((𝜑 ∧ 𝜓) ⊻ (𝜑 ∧ 𝜒)))))) |