Metamath Proof Explorer

Theorem ceqsex4v

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

Ref Expression
Hypotheses ceqsex4v.1 ⊢ A ∈ V
ceqsex4v.2 ⊢ B ∈ V
ceqsex4v.3 ⊢ C ∈ V
ceqsex4v.4 ⊢ D ∈ V
ceqsex4v.7 ⊢ x = A → φ ↔ ψ
ceqsex4v.8 ⊢ y = B → ψ ↔ χ
ceqsex4v.9 ⊢ z = C → χ ↔ θ
ceqsex4v.10 ⊢ w = D → θ ↔ τ
Assertion ceqsex4v ⊢ ∃ x ∃ y ∃ z ∃ w x = A ∧ y = B ∧ z = C ∧ w = D ∧ φ ↔ τ

Proof

Step Hyp Ref Expression
1 ceqsex4v.1 ⊢ A ∈ V
2 ceqsex4v.2 ⊢ B ∈ V
3 ceqsex4v.3 ⊢ C ∈ V
4 ceqsex4v.4 ⊢ D ∈ V
5 ceqsex4v.7 ⊢ x = A → φ ↔ ψ
6 ceqsex4v.8 ⊢ y = B → ψ ↔ χ
7 ceqsex4v.9 ⊢ z = C → χ ↔ θ
8 ceqsex4v.10 ⊢ w = D → θ ↔ τ
9 19.42vv ⊢ ∃ z ∃ w x = A ∧ y = B ∧ z = C ∧ w = D ∧ φ ↔ x = A ∧ y = B ∧ ∃ z ∃ w z = C ∧ w = D ∧ φ
10 3anass ⊢ x = A ∧ y = B ∧ z = C ∧ w = D ∧ φ ↔ x = A ∧ y = B ∧ z = C ∧ w = D ∧ φ
11 df-3an ⊢ z = C ∧ w = D ∧ φ ↔ z = C ∧ w = D ∧ φ
12 11 anbi2i ⊢ x = A ∧ y = B ∧ z = C ∧ w = D ∧ φ ↔ x = A ∧ y = B ∧ z = C ∧ w = D ∧ φ
13 10 12 bitr4i ⊢ x = A ∧ y = B ∧ z = C ∧ w = D ∧ φ ↔ x = A ∧ y = B ∧ z = C ∧ w = D ∧ φ
14 13 2exbii ⊢ ∃ z ∃ w x = A ∧ y = B ∧ z = C ∧ w = D ∧ φ ↔ ∃ z ∃ w x = A ∧ y = B ∧ z = C ∧ w = D ∧ φ
15 df-3an ⊢ x = A ∧ y = B ∧ ∃ z ∃ w z = C ∧ w = D ∧ φ ↔ x = A ∧ y = B ∧ ∃ z ∃ w z = C ∧ w = D ∧ φ
16 9 14 15 3bitr4i ⊢ ∃ z ∃ w x = A ∧ y = B ∧ z = C ∧ w = D ∧ φ ↔ x = A ∧ y = B ∧ ∃ z ∃ w z = C ∧ w = D ∧ φ
17 16 2exbii ⊢ ∃ x ∃ y ∃ z ∃ w x = A ∧ y = B ∧ z = C ∧ w = D ∧ φ ↔ ∃ x ∃ y x = A ∧ y = B ∧ ∃ z ∃ w z = C ∧ w = D ∧ φ
18 5 3anbi3d ⊢ x = A → z = C ∧ w = D ∧ φ ↔ z = C ∧ w = D ∧ ψ
19 18 2exbidv ⊢ x = A → ∃ z ∃ w z = C ∧ w = D ∧ φ ↔ ∃ z ∃ w z = C ∧ w = D ∧ ψ
20 6 3anbi3d ⊢ y = B → z = C ∧ w = D ∧ ψ ↔ z = C ∧ w = D ∧ χ
21 20 2exbidv ⊢ y = B → ∃ z ∃ w z = C ∧ w = D ∧ ψ ↔ ∃ z ∃ w z = C ∧ w = D ∧ χ
22 1 2 19 21 ceqsex2v ⊢ ∃ x ∃ y x = A ∧ y = B ∧ ∃ z ∃ w z = C ∧ w = D ∧ φ ↔ ∃ z ∃ w z = C ∧ w = D ∧ χ
23 3 4 7 8 ceqsex2v ⊢ ∃ z ∃ w z = C ∧ w = D ∧ χ ↔ τ
24 17 22 23 3bitri ⊢ ∃ x ∃ y ∃ z ∃ w x = A ∧ y = B ∧ z = C ∧ w = D ∧ φ ↔ τ