Proof of Theorem xordidc
Step | Hyp | Ref
| Expression |
1 | | dcbi 843 |
. . . . 5
⊢
(DECID ψ →
(DECID χ →
DECID (ψ ↔ χ))) |
2 | 1 | imp 115 |
. . . 4
⊢
((DECID ψ ∧ DECID χ) → DECID (ψ ↔ χ)) |
3 | | annimdc 844 |
. . . . . 6
⊢
(DECID φ →
(DECID (ψ ↔ χ) → ((φ ∧ ¬
(ψ ↔ χ)) ↔ ¬ (φ → (ψ ↔ χ))))) |
4 | 3 | imp 115 |
. . . . 5
⊢
((DECID φ ∧ DECID (ψ ↔ χ)) → ((φ ∧ ¬
(ψ ↔ χ)) ↔ ¬ (φ → (ψ ↔ χ)))) |
5 | | pm5.32 426 |
. . . . . 6
⊢ ((φ → (ψ ↔ χ)) ↔ ((φ ∧ ψ) ↔ (φ ∧ χ))) |
6 | 5 | notbii 593 |
. . . . 5
⊢ (¬
(φ → (ψ ↔ χ)) ↔ ¬ ((φ ∧ ψ) ↔ (φ ∧ χ))) |
7 | 4, 6 | syl6bb 185 |
. . . 4
⊢
((DECID φ ∧ DECID (ψ ↔ χ)) → ((φ ∧ ¬
(ψ ↔ χ)) ↔ ¬ ((φ ∧ ψ) ↔ (φ ∧ χ)))) |
8 | 2, 7 | sylan2 270 |
. . 3
⊢
((DECID φ ∧ (DECID ψ ∧
DECID χ)) → ((φ ∧ ¬
(ψ ↔ χ)) ↔ ¬ ((φ ∧ ψ) ↔ (φ ∧ χ)))) |
9 | | xornbidc 1279 |
. . . . . 6
⊢
(DECID ψ →
(DECID χ → ((ψ ⊻ χ) ↔ ¬ (ψ ↔ χ)))) |
10 | 9 | imp 115 |
. . . . 5
⊢
((DECID ψ ∧ DECID χ) → ((ψ ⊻ χ) ↔ ¬ (ψ ↔ χ))) |
11 | 10 | adantl 262 |
. . . 4
⊢
((DECID φ ∧ (DECID ψ ∧
DECID χ)) → ((ψ ⊻ χ) ↔ ¬ (ψ ↔ χ))) |
12 | 11 | anbi2d 437 |
. . 3
⊢
((DECID φ ∧ (DECID ψ ∧
DECID χ)) → ((φ ∧ (ψ ⊻ χ)) ↔ (φ ∧ ¬
(ψ ↔ χ)))) |
13 | | dcan 841 |
. . . . . 6
⊢
(DECID φ →
(DECID ψ →
DECID (φ ∧ ψ))) |
14 | 13 | imp 115 |
. . . . 5
⊢
((DECID φ ∧ DECID ψ) → DECID (φ ∧ ψ)) |
15 | 14 | adantrr 448 |
. . . 4
⊢
((DECID φ ∧ (DECID ψ ∧
DECID χ)) →
DECID (φ ∧ ψ)) |
16 | | dcan 841 |
. . . . . 6
⊢
(DECID φ →
(DECID χ →
DECID (φ ∧ χ))) |
17 | 16 | imp 115 |
. . . . 5
⊢
((DECID φ ∧ DECID χ) → DECID (φ ∧ χ)) |
18 | 17 | adantrl 447 |
. . . 4
⊢
((DECID φ ∧ (DECID ψ ∧
DECID χ)) →
DECID (φ ∧ χ)) |
19 | | xornbidc 1279 |
. . . 4
⊢
(DECID (φ ∧ ψ) →
(DECID (φ ∧ χ) →
(((φ ∧
ψ) ⊻ (φ ∧ χ)) ↔ ¬ ((φ ∧ ψ) ↔ (φ ∧ χ))))) |
20 | 15, 18, 19 | sylc 56 |
. . 3
⊢
((DECID φ ∧ (DECID ψ ∧
DECID χ)) →
(((φ ∧
ψ) ⊻ (φ ∧ χ)) ↔ ¬ ((φ ∧ ψ) ↔ (φ ∧ χ)))) |
21 | 8, 12, 20 | 3bitr4d 209 |
. 2
⊢
((DECID φ ∧ (DECID ψ ∧
DECID χ)) → ((φ ∧ (ψ ⊻ χ)) ↔ ((φ ∧ ψ) ⊻ (φ ∧ χ)))) |
22 | 21 | exp32 347 |
1
⊢
(DECID φ →
(DECID ψ →
(DECID χ → ((φ ∧ (ψ ⊻ χ)) ↔ ((φ ∧ ψ) ⊻ (φ ∧ χ)))))) |