Metamath Proof Explorer

Theorem ceqsex6v

Description: Elimination of six existential quantifiers, using implicit substitution. (Contributed by NM, 21-Sep-2011)

Ref Expression
Hypotheses ceqsex6v.1 ⊢ A ∈ V
ceqsex6v.2 ⊢ B ∈ V
ceqsex6v.3 ⊢ C ∈ V
ceqsex6v.4 ⊢ D ∈ V
ceqsex6v.5 ⊢ E ∈ V
ceqsex6v.6 ⊢ F ∈ V
ceqsex6v.7 ⊢ x = A → φ ↔ ψ
ceqsex6v.8 ⊢ y = B → ψ ↔ χ
ceqsex6v.9 ⊢ z = C → χ ↔ θ
ceqsex6v.10 ⊢ w = D → θ ↔ τ
ceqsex6v.11 ⊢ v = E → τ ↔ η
ceqsex6v.12 ⊢ u = F → η ↔ ζ
Assertion ceqsex6v ⊢ ∃ x ∃ y ∃ z ∃ w ∃ v ∃ u x = A ∧ y = B ∧ z = C ∧ w = D ∧ v = E ∧ u = F ∧ φ ↔ ζ

Proof

Step Hyp Ref Expression
1 ceqsex6v.1 ⊢ A ∈ V
2 ceqsex6v.2 ⊢ B ∈ V
3 ceqsex6v.3 ⊢ C ∈ V
4 ceqsex6v.4 ⊢ D ∈ V
5 ceqsex6v.5 ⊢ E ∈ V
6 ceqsex6v.6 ⊢ F ∈ V
7 ceqsex6v.7 ⊢ x = A → φ ↔ ψ
8 ceqsex6v.8 ⊢ y = B → ψ ↔ χ
9 ceqsex6v.9 ⊢ z = C → χ ↔ θ
10 ceqsex6v.10 ⊢ w = D → θ ↔ τ
11 ceqsex6v.11 ⊢ v = E → τ ↔ η
12 ceqsex6v.12 ⊢ u = F → η ↔ ζ
13 3anass ⊢ x = A ∧ y = B ∧ z = C ∧ w = D ∧ v = E ∧ u = F ∧ φ ↔ x = A ∧ y = B ∧ z = C ∧ w = D ∧ v = E ∧ u = F ∧ φ
14 13 3exbii ⊢ ∃ w ∃ v ∃ u x = A ∧ y = B ∧ z = C ∧ w = D ∧ v = E ∧ u = F ∧ φ ↔ ∃ w ∃ v ∃ u x = A ∧ y = B ∧ z = C ∧ w = D ∧ v = E ∧ u = F ∧ φ
15 19.42vvv ⊢ ∃ w ∃ v ∃ u x = A ∧ y = B ∧ z = C ∧ w = D ∧ v = E ∧ u = F ∧ φ ↔ x = A ∧ y = B ∧ z = C ∧ ∃ w ∃ v ∃ u w = D ∧ v = E ∧ u = F ∧ φ
16 14 15 bitri ⊢ ∃ w ∃ v ∃ u x = A ∧ y = B ∧ z = C ∧ w = D ∧ v = E ∧ u = F ∧ φ ↔ x = A ∧ y = B ∧ z = C ∧ ∃ w ∃ v ∃ u w = D ∧ v = E ∧ u = F ∧ φ
17 16 3exbii ⊢ ∃ x ∃ y ∃ z ∃ w ∃ v ∃ u x = A ∧ y = B ∧ z = C ∧ w = D ∧ v = E ∧ u = F ∧ φ ↔ ∃ x ∃ y ∃ z x = A ∧ y = B ∧ z = C ∧ ∃ w ∃ v ∃ u w = D ∧ v = E ∧ u = F ∧ φ
18 7 anbi2d ⊢ x = A → w = D ∧ v = E ∧ u = F ∧ φ ↔ w = D ∧ v = E ∧ u = F ∧ ψ
19 18 3exbidv ⊢ x = A → ∃ w ∃ v ∃ u w = D ∧ v = E ∧ u = F ∧ φ ↔ ∃ w ∃ v ∃ u w = D ∧ v = E ∧ u = F ∧ ψ
20 8 anbi2d ⊢ y = B → w = D ∧ v = E ∧ u = F ∧ ψ ↔ w = D ∧ v = E ∧ u = F ∧ χ
21 20 3exbidv ⊢ y = B → ∃ w ∃ v ∃ u w = D ∧ v = E ∧ u = F ∧ ψ ↔ ∃ w ∃ v ∃ u w = D ∧ v = E ∧ u = F ∧ χ
22 9 anbi2d ⊢ z = C → w = D ∧ v = E ∧ u = F ∧ χ ↔ w = D ∧ v = E ∧ u = F ∧ θ
23 22 3exbidv ⊢ z = C → ∃ w ∃ v ∃ u w = D ∧ v = E ∧ u = F ∧ χ ↔ ∃ w ∃ v ∃ u w = D ∧ v = E ∧ u = F ∧ θ
24 1 2 3 19 21 23 ceqsex3v ⊢ ∃ x ∃ y ∃ z x = A ∧ y = B ∧ z = C ∧ ∃ w ∃ v ∃ u w = D ∧ v = E ∧ u = F ∧ φ ↔ ∃ w ∃ v ∃ u w = D ∧ v = E ∧ u = F ∧ θ
25 4 5 6 10 11 12 ceqsex3v ⊢ ∃ w ∃ v ∃ u w = D ∧ v = E ∧ u = F ∧ θ ↔ ζ
26 24 25 bitri ⊢ ∃ x ∃ y ∃ z x = A ∧ y = B ∧ z = C ∧ ∃ w ∃ v ∃ u w = D ∧ v = E ∧ u = F ∧ φ ↔ ζ
27 17 26 bitri ⊢ ∃ x ∃ y ∃ z ∃ w ∃ v ∃ u x = A ∧ y = B ∧ z = C ∧ w = D ∧ v = E ∧ u = F ∧ φ ↔ ζ