Proof of Theorem con4biddc
Step | Hyp | Ref
| Expression |
1 | | con4biddc.1 |
. . . . . 6
⊢ (𝜑 → (DECID
𝜓 →
(DECID 𝜒
→ (¬ 𝜓 ↔ ¬
𝜒)))) |
2 | | biimpr 129 |
. . . . . 6
⊢ ((¬
𝜓 ↔ ¬ 𝜒) → (¬ 𝜒 → ¬ 𝜓)) |
3 | 1, 2 | syl8 71 |
. . . . 5
⊢ (𝜑 → (DECID
𝜓 →
(DECID 𝜒
→ (¬ 𝜒 → ¬
𝜓)))) |
4 | | condc 839 |
. . . . . 6
⊢
(DECID 𝜒 → ((¬ 𝜒 → ¬ 𝜓) → (𝜓 → 𝜒))) |
5 | 4 | a2i 11 |
. . . . 5
⊢
((DECID 𝜒 → (¬ 𝜒 → ¬ 𝜓)) → (DECID 𝜒 → (𝜓 → 𝜒))) |
6 | 3, 5 | syl6 33 |
. . . 4
⊢ (𝜑 → (DECID
𝜓 →
(DECID 𝜒
→ (𝜓 → 𝜒)))) |
7 | 6 | imp31 254 |
. . 3
⊢ (((𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → (𝜓 → 𝜒)) |
8 | | biimp 117 |
. . . . . 6
⊢ ((¬
𝜓 ↔ ¬ 𝜒) → (¬ 𝜓 → ¬ 𝜒)) |
9 | 1, 8 | syl8 71 |
. . . . 5
⊢ (𝜑 → (DECID
𝜓 →
(DECID 𝜒
→ (¬ 𝜓 → ¬
𝜒)))) |
10 | | condc 839 |
. . . . . 6
⊢
(DECID 𝜓 → ((¬ 𝜓 → ¬ 𝜒) → (𝜒 → 𝜓))) |
11 | 10 | imim2d 54 |
. . . . 5
⊢
(DECID 𝜓 → ((DECID 𝜒 → (¬ 𝜓 → ¬ 𝜒)) → (DECID 𝜒 → (𝜒 → 𝜓)))) |
12 | 9, 11 | sylcom 28 |
. . . 4
⊢ (𝜑 → (DECID
𝜓 →
(DECID 𝜒
→ (𝜒 → 𝜓)))) |
13 | 12 | imp31 254 |
. . 3
⊢ (((𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → (𝜒 → 𝜓)) |
14 | 7, 13 | impbid 128 |
. 2
⊢ (((𝜑 ∧ DECID 𝜓) ∧ DECID 𝜒) → (𝜓 ↔ 𝜒)) |
15 | 14 | exp31 362 |
1
⊢ (𝜑 → (DECID
𝜓 →
(DECID 𝜒
→ (𝜓 ↔ 𝜒)))) |