Proof of Theorem pm5.18dc
Step | Hyp | Ref
| Expression |
1 | | df-dc 742 |
. 2
⊢
(DECID φ ↔
(φ ∨
¬ φ)) |
2 | | pm5.501 233 |
. . . . . . . 8
⊢ (φ → (¬ ψ ↔ (φ ↔ ¬ ψ))) |
3 | 2 | a1d 22 |
. . . . . . 7
⊢ (φ → (DECID ψ → (¬ ψ ↔ (φ ↔ ¬ ψ)))) |
4 | 3 | con1biddc 769 |
. . . . . 6
⊢ (φ → (DECID ψ → (¬ (φ ↔ ¬ ψ) ↔ ψ))) |
5 | 4 | imp 115 |
. . . . 5
⊢ ((φ ∧
DECID ψ) → (¬
(φ ↔ ¬ ψ) ↔ ψ)) |
6 | | pm5.501 233 |
. . . . . 6
⊢ (φ → (ψ ↔ (φ ↔ ψ))) |
7 | 6 | adantr 261 |
. . . . 5
⊢ ((φ ∧
DECID ψ) → (ψ ↔ (φ ↔ ψ))) |
8 | 5, 7 | bitr2d 178 |
. . . 4
⊢ ((φ ∧
DECID ψ) → ((φ ↔ ψ) ↔ ¬ (φ ↔ ¬ ψ))) |
9 | 8 | ex 108 |
. . 3
⊢ (φ → (DECID ψ → ((φ ↔ ψ) ↔ ¬ (φ ↔ ¬ ψ)))) |
10 | | dcn 745 |
. . . . . . 7
⊢
(DECID ψ →
DECID ¬ ψ) |
11 | | nbn2 612 |
. . . . . . . . 9
⊢ (¬
φ → (¬ ¬ ψ ↔ (φ ↔ ¬ ψ))) |
12 | 11 | a1d 22 |
. . . . . . . 8
⊢ (¬
φ → (DECID ¬
ψ → (¬ ¬ ψ ↔ (φ ↔ ¬ ψ)))) |
13 | 12 | con1biddc 769 |
. . . . . . 7
⊢ (¬
φ → (DECID ¬
ψ → (¬ (φ ↔ ¬ ψ) ↔ ¬ ψ))) |
14 | 10, 13 | syl5 28 |
. . . . . 6
⊢ (¬
φ → (DECID ψ → (¬ (φ ↔ ¬ ψ) ↔ ¬ ψ))) |
15 | 14 | imp 115 |
. . . . 5
⊢ ((¬
φ ∧
DECID ψ) → (¬
(φ ↔ ¬ ψ) ↔ ¬ ψ)) |
16 | | nbn2 612 |
. . . . . 6
⊢ (¬
φ → (¬ ψ ↔ (φ ↔ ψ))) |
17 | 16 | adantr 261 |
. . . . 5
⊢ ((¬
φ ∧
DECID ψ) → (¬
ψ ↔ (φ ↔ ψ))) |
18 | 15, 17 | bitr2d 178 |
. . . 4
⊢ ((¬
φ ∧
DECID ψ) → ((φ ↔ ψ) ↔ ¬ (φ ↔ ¬ ψ))) |
19 | 18 | ex 108 |
. . 3
⊢ (¬
φ → (DECID ψ → ((φ ↔ ψ) ↔ ¬ (φ ↔ ¬ ψ)))) |
20 | 9, 19 | jaoi 635 |
. 2
⊢ ((φ ∨ ¬
φ) → (DECID ψ → ((φ ↔ ψ) ↔ ¬ (φ ↔ ¬ ψ)))) |
21 | 1, 20 | sylbi 114 |
1
⊢
(DECID φ →
(DECID ψ → ((φ ↔ ψ) ↔ ¬ (φ ↔ ¬ ψ)))) |