ceqsex8v

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

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

Proof

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

Metamath Proof Explorer

Theorem ceqsex8v

Proof