Proof of Theorem nanass
Step | Hyp | Ref
| Expression |
1 | | bicom1 220 |
. . . 4
⊢ ((𝜑 ↔ 𝜒) → (𝜒 ↔ 𝜑)) |
2 | | nanbi2 1497 |
. . . 4
⊢ ((𝜑 ↔ 𝜒) → ((𝜓 ⊼ 𝜑) ↔ (𝜓 ⊼ 𝜒))) |
3 | 1, 2 | nanbi12d 1504 |
. . 3
⊢ ((𝜑 ↔ 𝜒) → ((𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜒)))) |
4 | | nannan 1492 |
. . . . . 6
⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ↔ (𝜑 → (𝜓 ∧ 𝜒))) |
5 | | simpr 485 |
. . . . . . 7
⊢ ((𝜓 ∧ 𝜒) → 𝜒) |
6 | 5 | imim2i 16 |
. . . . . 6
⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → (𝜑 → 𝜒)) |
7 | 4, 6 | sylbi 216 |
. . . . 5
⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) → (𝜑 → 𝜒)) |
8 | | nannan 1492 |
. . . . . 6
⊢ ((𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ (𝜒 → (𝜓 ∧ 𝜑))) |
9 | | simpr 485 |
. . . . . . 7
⊢ ((𝜓 ∧ 𝜑) → 𝜑) |
10 | 9 | imim2i 16 |
. . . . . 6
⊢ ((𝜒 → (𝜓 ∧ 𝜑)) → (𝜒 → 𝜑)) |
11 | 8, 10 | sylbi 216 |
. . . . 5
⊢ ((𝜒 ⊼ (𝜓 ⊼ 𝜑)) → (𝜒 → 𝜑)) |
12 | 7, 11 | impbid21d 210 |
. . . 4
⊢ ((𝜒 ⊼ (𝜓 ⊼ 𝜑)) → ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) → (𝜑 ↔ 𝜒))) |
13 | | nanan 1488 |
. . . . . 6
⊢ ((𝜑 ∧ (𝜓 ⊼ 𝜒)) ↔ ¬ (𝜑 ⊼ (𝜓 ⊼ 𝜒))) |
14 | | simpl 483 |
. . . . . 6
⊢ ((𝜑 ∧ (𝜓 ⊼ 𝜒)) → 𝜑) |
15 | 13, 14 | sylbir 234 |
. . . . 5
⊢ (¬
(𝜑 ⊼ (𝜓 ⊼ 𝜒)) → 𝜑) |
16 | | nanan 1488 |
. . . . . 6
⊢ ((𝜒 ∧ (𝜓 ⊼ 𝜑)) ↔ ¬ (𝜒 ⊼ (𝜓 ⊼ 𝜑))) |
17 | | simpl 483 |
. . . . . 6
⊢ ((𝜒 ∧ (𝜓 ⊼ 𝜑)) → 𝜒) |
18 | 16, 17 | sylbir 234 |
. . . . 5
⊢ (¬
(𝜒 ⊼ (𝜓 ⊼ 𝜑)) → 𝜒) |
19 | | pm5.1im 262 |
. . . . 5
⊢ (𝜑 → (𝜒 → (𝜑 ↔ 𝜒))) |
20 | 15, 18, 19 | syl2imc 41 |
. . . 4
⊢ (¬
(𝜒 ⊼ (𝜓 ⊼ 𝜑)) → (¬ (𝜑 ⊼ (𝜓 ⊼ 𝜒)) → (𝜑 ↔ 𝜒))) |
21 | 12, 20 | bija 382 |
. . 3
⊢ (((𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜒))) → (𝜑 ↔ 𝜒)) |
22 | 3, 21 | impbii 208 |
. 2
⊢ ((𝜑 ↔ 𝜒) ↔ ((𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜒)))) |
23 | | nancom 1491 |
. . . . 5
⊢ ((𝜓 ⊼ 𝜑) ↔ (𝜑 ⊼ 𝜓)) |
24 | 23 | nanbi2i 1500 |
. . . 4
⊢ ((𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ (𝜒 ⊼ (𝜑 ⊼ 𝜓))) |
25 | | nancom 1491 |
. . . 4
⊢ ((𝜒 ⊼ (𝜑 ⊼ 𝜓)) ↔ ((𝜑 ⊼ 𝜓) ⊼ 𝜒)) |
26 | 24, 25 | bitri 274 |
. . 3
⊢ ((𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ ((𝜑 ⊼ 𝜓) ⊼ 𝜒)) |
27 | 26 | bibi1i 339 |
. 2
⊢ (((𝜒 ⊼ (𝜓 ⊼ 𝜑)) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜒))) ↔ (((𝜑 ⊼ 𝜓) ⊼ 𝜒) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜒)))) |
28 | 22, 27 | bitri 274 |
1
⊢ ((𝜑 ↔ 𝜒) ↔ (((𝜑 ⊼ 𝜓) ⊼ 𝜒) ↔ (𝜑 ⊼ (𝜓 ⊼ 𝜒)))) |