Proof of Theorem eeeanv
Step | Hyp | Ref
| Expression |
1 | | eeanv 2350 |
. . 3
⊢
(∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓)) |
2 | 1 | anbi1i 627 |
. 2
⊢
((∃𝑥∃𝑦(𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒) ↔ ((∃𝑥𝜑 ∧ ∃𝑦𝜓) ∧ ∃𝑧𝜒)) |
3 | | df-3an 1091 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒)) |
4 | 3 | exbii 1855 |
. . . . 5
⊢
(∃𝑧(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ∃𝑧((𝜑 ∧ 𝜓) ∧ 𝜒)) |
5 | | 19.42v 1962 |
. . . . 5
⊢
(∃𝑧((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒)) |
6 | 4, 5 | bitri 278 |
. . . 4
⊢
(∃𝑧(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒)) |
7 | 6 | 2exbii 1856 |
. . 3
⊢
(∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ∃𝑥∃𝑦((𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒)) |
8 | | nfv 1922 |
. . . . . 6
⊢
Ⅎ𝑦𝜒 |
9 | 8 | nfex 2323 |
. . . . 5
⊢
Ⅎ𝑦∃𝑧𝜒 |
10 | 9 | 19.41 2233 |
. . . 4
⊢
(∃𝑦((𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒) ↔ (∃𝑦(𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒)) |
11 | 10 | exbii 1855 |
. . 3
⊢
(∃𝑥∃𝑦((𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒) ↔ ∃𝑥(∃𝑦(𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒)) |
12 | | nfv 1922 |
. . . . 5
⊢
Ⅎ𝑥𝜒 |
13 | 12 | nfex 2323 |
. . . 4
⊢
Ⅎ𝑥∃𝑧𝜒 |
14 | 13 | 19.41 2233 |
. . 3
⊢
(∃𝑥(∃𝑦(𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒) ↔ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒)) |
15 | 7, 11, 14 | 3bitri 300 |
. 2
⊢
(∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ∧ ∃𝑧𝜒)) |
16 | | df-3an 1091 |
. 2
⊢
((∃𝑥𝜑 ∧ ∃𝑦𝜓 ∧ ∃𝑧𝜒) ↔ ((∃𝑥𝜑 ∧ ∃𝑦𝜓) ∧ ∃𝑧𝜒)) |
17 | 2, 15, 16 | 3bitr4i 306 |
1
⊢
(∃𝑥∃𝑦∃𝑧(𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓 ∧ ∃𝑧𝜒)) |