Proof of Theorem lukshef-ax2
Step | Hyp | Ref
| Expression |
1 | | nannan 1492 |
. . . 4
⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ↔ (𝜑 → (𝜓 ∧ 𝜒))) |
2 | 1 | biimpi 219 |
. . 3
⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) → (𝜑 → (𝜓 ∧ 𝜒))) |
3 | | simpr 488 |
. . . . 5
⊢ ((𝜓 ∧ 𝜒) → 𝜒) |
4 | 3 | imim2i 16 |
. . . 4
⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → (𝜑 → 𝜒)) |
5 | | simpl 486 |
. . . . . 6
⊢ ((𝜓 ∧ 𝜒) → 𝜓) |
6 | 5 | imim2i 16 |
. . . . 5
⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → (𝜑 → 𝜓)) |
7 | | pm2.27 42 |
. . . . . . 7
⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓)) |
8 | 7 | anim2d 615 |
. . . . . 6
⊢ (𝜑 → ((𝜃 ∧ (𝜑 → 𝜓)) → (𝜃 ∧ 𝜓))) |
9 | 8 | expdimp 456 |
. . . . 5
⊢ ((𝜑 ∧ 𝜃) → ((𝜑 → 𝜓) → (𝜃 ∧ 𝜓))) |
10 | 6, 9 | syl5com 31 |
. . . 4
⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → ((𝜑 ∧ 𝜃) → (𝜃 ∧ 𝜓))) |
11 | | ancr 550 |
. . . . 5
⊢ ((𝜑 → 𝜒) → (𝜑 → (𝜒 ∧ 𝜑))) |
12 | 11 | anim1i 618 |
. . . 4
⊢ (((𝜑 → 𝜒) ∧ ((𝜑 ∧ 𝜃) → (𝜃 ∧ 𝜓))) → ((𝜑 → (𝜒 ∧ 𝜑)) ∧ ((𝜑 ∧ 𝜃) → (𝜃 ∧ 𝜓)))) |
13 | 4, 10, 12 | syl2anc 587 |
. . 3
⊢ ((𝜑 → (𝜓 ∧ 𝜒)) → ((𝜑 → (𝜒 ∧ 𝜑)) ∧ ((𝜑 ∧ 𝜃) → (𝜃 ∧ 𝜓)))) |
14 | | con3 156 |
. . . . 5
⊢ (((𝜑 ∧ 𝜃) → (𝜃 ∧ 𝜓)) → (¬ (𝜃 ∧ 𝜓) → ¬ (𝜑 ∧ 𝜃))) |
15 | | df-nan 1487 |
. . . . 5
⊢ ((𝜃 ⊼ 𝜓) ↔ ¬ (𝜃 ∧ 𝜓)) |
16 | | df-nan 1487 |
. . . . 5
⊢ ((𝜑 ⊼ 𝜃) ↔ ¬ (𝜑 ∧ 𝜃)) |
17 | 14, 15, 16 | 3imtr4g 299 |
. . . 4
⊢ (((𝜑 ∧ 𝜃) → (𝜃 ∧ 𝜓)) → ((𝜃 ⊼ 𝜓) → (𝜑 ⊼ 𝜃))) |
18 | 17 | anim2i 620 |
. . 3
⊢ (((𝜑 → (𝜒 ∧ 𝜑)) ∧ ((𝜑 ∧ 𝜃) → (𝜃 ∧ 𝜓))) → ((𝜑 → (𝜒 ∧ 𝜑)) ∧ ((𝜃 ⊼ 𝜓) → (𝜑 ⊼ 𝜃)))) |
19 | | nannan 1492 |
. . . . 5
⊢ ((𝜑 ⊼ (𝜒 ⊼ 𝜑)) ↔ (𝜑 → (𝜒 ∧ 𝜑))) |
20 | 19 | biimpri 231 |
. . . 4
⊢ ((𝜑 → (𝜒 ∧ 𝜑)) → (𝜑 ⊼ (𝜒 ⊼ 𝜑))) |
21 | | nanim 1493 |
. . . . 5
⊢ (((𝜃 ⊼ 𝜓) → (𝜑 ⊼ 𝜃)) ↔ ((𝜃 ⊼ 𝜓) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))) |
22 | 21 | biimpi 219 |
. . . 4
⊢ (((𝜃 ⊼ 𝜓) → (𝜑 ⊼ 𝜃)) → ((𝜃 ⊼ 𝜓) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))) |
23 | 20, 22 | anim12i 616 |
. . 3
⊢ (((𝜑 → (𝜒 ∧ 𝜑)) ∧ ((𝜃 ⊼ 𝜓) → (𝜑 ⊼ 𝜃))) → ((𝜑 ⊼ (𝜒 ⊼ 𝜑)) ∧ ((𝜃 ⊼ 𝜓) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))) |
24 | 2, 13, 18, 23 | 4syl 19 |
. 2
⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) → ((𝜑 ⊼ (𝜒 ⊼ 𝜑)) ∧ ((𝜃 ⊼ 𝜓) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))) |
25 | | nannan 1492 |
. 2
⊢ (((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜑)) ⊼ ((𝜃 ⊼ 𝜓) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))) ↔ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) → ((𝜑 ⊼ (𝜒 ⊼ 𝜑)) ∧ ((𝜃 ⊼ 𝜓) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃)))))) |
26 | 24, 25 | mpbir 234 |
1
⊢ ((𝜑 ⊼ (𝜓 ⊼ 𝜒)) ⊼ ((𝜑 ⊼ (𝜒 ⊼ 𝜑)) ⊼ ((𝜃 ⊼ 𝜓) ⊼ ((𝜑 ⊼ 𝜃) ⊼ (𝜑 ⊼ 𝜃))))) |