Proof of Theorem xor3dc
Step | Hyp | Ref
| Expression |
1 | | dcn 745 |
. . . . . 6
⊢
(DECID ψ →
DECID ¬ ψ) |
2 | | dcbi 843 |
. . . . . 6
⊢
(DECID φ →
(DECID ¬ ψ →
DECID (φ ↔ ¬
ψ))) |
3 | 1, 2 | syl5 28 |
. . . . 5
⊢
(DECID φ →
(DECID ψ →
DECID (φ ↔ ¬
ψ))) |
4 | 3 | imp 115 |
. . . 4
⊢
((DECID φ ∧ DECID ψ) → DECID (φ ↔ ¬ ψ)) |
5 | | pm5.18dc 776 |
. . . . . . 7
⊢
(DECID φ →
(DECID ψ → ((φ ↔ ψ) ↔ ¬ (φ ↔ ¬ ψ)))) |
6 | 5 | imp 115 |
. . . . . 6
⊢
((DECID φ ∧ DECID ψ) → ((φ ↔ ψ) ↔ ¬ (φ ↔ ¬ ψ))) |
7 | 6 | a1d 22 |
. . . . 5
⊢
((DECID φ ∧ DECID ψ) → (DECID (φ ↔ ¬ ψ) → ((φ ↔ ψ) ↔ ¬ (φ ↔ ¬ ψ)))) |
8 | 7 | con2biddc 773 |
. . . 4
⊢
((DECID φ ∧ DECID ψ) → (DECID (φ ↔ ¬ ψ) → ((φ ↔ ¬ ψ) ↔ ¬ (φ ↔ ψ)))) |
9 | 4, 8 | mpd 13 |
. . 3
⊢
((DECID φ ∧ DECID ψ) → ((φ ↔ ¬ ψ) ↔ ¬ (φ ↔ ψ))) |
10 | 9 | bicomd 129 |
. 2
⊢
((DECID φ ∧ DECID ψ) → (¬ (φ ↔ ψ) ↔ (φ ↔ ¬ ψ))) |
11 | 10 | ex 108 |
1
⊢
(DECID φ →
(DECID ψ → (¬
(φ ↔ ψ) ↔ (φ ↔ ¬ ψ)))) |