Metamath Proof Explorer


Theorem ceqsex8v

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

Ref Expression
Hypotheses ceqsex8v.1 A V
ceqsex8v.2 B V
ceqsex8v.3 C V
ceqsex8v.4 D V
ceqsex8v.5 E V
ceqsex8v.6 F V
ceqsex8v.7 G V
ceqsex8v.8 H V
ceqsex8v.9 x = A φ ψ
ceqsex8v.10 y = B ψ χ
ceqsex8v.11 z = C χ θ
ceqsex8v.12 w = D θ τ
ceqsex8v.13 v = E τ η
ceqsex8v.14 u = F η ζ
ceqsex8v.15 t = G ζ σ
ceqsex8v.16 s = H σ ρ
Assertion ceqsex8v x y z w v u t s x = A y = B z = C w = D v = E u = F t = G s = H φ ρ

Proof

Step Hyp Ref Expression
1 ceqsex8v.1 A V
2 ceqsex8v.2 B V
3 ceqsex8v.3 C V
4 ceqsex8v.4 D V
5 ceqsex8v.5 E V
6 ceqsex8v.6 F V
7 ceqsex8v.7 G V
8 ceqsex8v.8 H V
9 ceqsex8v.9 x = A φ ψ
10 ceqsex8v.10 y = B ψ χ
11 ceqsex8v.11 z = C χ θ
12 ceqsex8v.12 w = D θ τ
13 ceqsex8v.13 v = E τ η
14 ceqsex8v.14 u = F η ζ
15 ceqsex8v.15 t = G ζ σ
16 ceqsex8v.16 s = H σ ρ
17 19.42vv t s x = A y = B z = C w = D v = E u = F t = G s = H φ x = A y = B z = C w = D t s v = E u = F t = G s = H φ
18 17 2exbii v u t s x = A y = B z = C w = D v = E u = F t = G s = H φ v u x = A y = B z = C w = D t s v = E u = F t = G s = H φ
19 19.42vv v u x = A y = B z = C w = D t s v = E u = F t = G s = H φ x = A y = B z = C w = D v u t s v = E u = F t = G s = H φ
20 18 19 bitri v u t s x = A y = B z = C w = D v = E u = F t = G s = H φ x = A y = B z = C w = D v u t s v = E u = F t = G s = H φ
21 3anass x = A y = B z = C w = D v = E u = F t = G s = H φ x = A y = B z = C w = D v = E u = F t = G s = H φ
22 df-3an v = E u = F t = G s = H φ v = E u = F t = G s = H φ
23 22 anbi2i x = A y = B z = C w = D v = E u = F t = G s = H φ x = A y = B z = C w = D v = E u = F t = G s = H φ
24 21 23 bitr4i x = A y = B z = C w = D v = E u = F t = G s = H φ x = A y = B z = C w = D v = E u = F t = G s = H φ
25 24 2exbii t s x = A y = B z = C w = D v = E u = F t = G s = H φ t s x = A y = B z = C w = D v = E u = F t = G s = H φ
26 25 2exbii v u t s x = A y = B z = C w = D v = E u = F t = G s = H φ v u t s x = A y = B z = C w = D v = E u = F t = G s = H φ
27 df-3an x = A y = B z = C w = D v u t s v = E u = F t = G s = H φ x = A y = B z = C w = D v u t s v = E u = F t = G s = H φ
28 20 26 27 3bitr4i v u t s x = A y = B z = C w = D v = E u = F t = G s = H φ x = A y = B z = C w = D v u t s v = E u = F t = G s = H φ
29 28 2exbii z w v u t s x = A y = B z = C w = D v = E u = F t = G s = H φ z w x = A y = B z = C w = D v u t s v = E u = F t = G s = H φ
30 29 2exbii x y z w v u t s x = A y = B z = C w = D v = E u = F t = G s = H φ x y z w x = A y = B z = C w = D v u t s v = E u = F t = G s = H φ
31 9 3anbi3d x = A v = E u = F t = G s = H φ v = E u = F t = G s = H ψ
32 31 4exbidv x = A v u t s v = E u = F t = G s = H φ v u t s v = E u = F t = G s = H ψ
33 10 3anbi3d y = B v = E u = F t = G s = H ψ v = E u = F t = G s = H χ
34 33 4exbidv y = B v u t s v = E u = F t = G s = H ψ v u t s v = E u = F t = G s = H χ
35 11 3anbi3d z = C v = E u = F t = G s = H χ v = E u = F t = G s = H θ
36 35 4exbidv z = C v u t s v = E u = F t = G s = H χ v u t s v = E u = F t = G s = H θ
37 12 3anbi3d w = D v = E u = F t = G s = H θ v = E u = F t = G s = H τ
38 37 4exbidv w = D v u t s v = E u = F t = G s = H θ v u t s v = E u = F t = G s = H τ
39 1 2 3 4 32 34 36 38 ceqsex4v x y z w x = A y = B z = C w = D v u t s v = E u = F t = G s = H φ v u t s v = E u = F t = G s = H τ
40 5 6 7 8 13 14 15 16 ceqsex4v v u t s v = E u = F t = G s = H τ ρ
41 39 40 bitri x y z w x = A y = B z = C w = D v u t s v = E u = F t = G s = H φ ρ
42 30 41 bitri x y z w v u t s x = A y = B z = C w = D v = E u = F t = G s = H φ ρ