Proof of Theorem 3reeanv
Step | Hyp | Ref
| Expression |
1 | | r19.41v 2764 |
. . 3
⊢ (∃x ∈ A (∃y ∈ B (φ ∧ ψ) ∧ ∃z ∈ C χ) ↔ (∃x ∈ A ∃y ∈ B (φ ∧ ψ) ∧ ∃z ∈ C χ)) |
2 | | reeanv 2778 |
. . . 4
⊢ (∃x ∈ A ∃y ∈ B (φ ∧ ψ) ↔ (∃x ∈ A φ ∧ ∃y ∈ B ψ)) |
3 | 2 | anbi1i 676 |
. . 3
⊢ ((∃x ∈ A ∃y ∈ B (φ ∧ ψ) ∧ ∃z ∈ C χ) ↔ ((∃x ∈ A φ ∧ ∃y ∈ B ψ) ∧ ∃z ∈ C χ)) |
4 | 1, 3 | bitri 240 |
. 2
⊢ (∃x ∈ A (∃y ∈ B (φ ∧ ψ) ∧ ∃z ∈ C χ) ↔ ((∃x ∈ A φ ∧ ∃y ∈ B ψ) ∧ ∃z ∈ C χ)) |
5 | | df-3an 936 |
. . . . 5
⊢ ((φ ∧ ψ ∧ χ) ↔ ((φ ∧ ψ) ∧ χ)) |
6 | 5 | 2rexbii 2641 |
. . . 4
⊢ (∃y ∈ B ∃z ∈ C (φ ∧ ψ ∧ χ) ↔ ∃y ∈ B ∃z ∈ C ((φ ∧ ψ) ∧ χ)) |
7 | | reeanv 2778 |
. . . 4
⊢ (∃y ∈ B ∃z ∈ C ((φ ∧ ψ) ∧ χ) ↔ (∃y ∈ B (φ ∧ ψ) ∧ ∃z ∈ C χ)) |
8 | 6, 7 | bitri 240 |
. . 3
⊢ (∃y ∈ B ∃z ∈ C (φ ∧ ψ ∧ χ) ↔ (∃y ∈ B (φ ∧ ψ) ∧ ∃z ∈ C χ)) |
9 | 8 | rexbii 2639 |
. 2
⊢ (∃x ∈ A ∃y ∈ B ∃z ∈ C (φ ∧ ψ ∧ χ) ↔ ∃x ∈ A (∃y ∈ B (φ ∧ ψ) ∧ ∃z ∈ C χ)) |
10 | | df-3an 936 |
. 2
⊢ ((∃x ∈ A φ ∧ ∃y ∈ B ψ ∧ ∃z ∈ C χ) ↔ ((∃x ∈ A φ ∧ ∃y ∈ B ψ) ∧ ∃z ∈ C χ)) |
11 | 4, 9, 10 | 3bitr4i 268 |
1
⊢ (∃x ∈ A ∃y ∈ B ∃z ∈ C (φ ∧ ψ ∧ χ) ↔ (∃x ∈ A φ ∧ ∃y ∈ B ψ ∧ ∃z ∈ C χ)) |