Metamath Proof Explorer

Theorem ceqsex3v

Description: Elimination of three existential quantifiers, using implicit substitution. (Contributed by NM, 16-Aug-2011)

Ref Expression
Hypotheses ceqsex3v.1 ⊢ A ∈ V
ceqsex3v.2 ⊢ B ∈ V
ceqsex3v.3 ⊢ C ∈ V
ceqsex3v.4 ⊢ x = A → φ ↔ ψ
ceqsex3v.5 ⊢ y = B → ψ ↔ χ
ceqsex3v.6 ⊢ z = C → χ ↔ θ
Assertion ceqsex3v ⊢ ∃ x ∃ y ∃ z x = A ∧ y = B ∧ z = C ∧ φ ↔ θ

Proof

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