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 ⊢ 𝐴 ∈ V
ceqsex6v.2 ⊢ 𝐵 ∈ V
ceqsex6v.3 ⊢ 𝐶 ∈ V
ceqsex6v.4 ⊢ 𝐷 ∈ V
ceqsex6v.5 ⊢ 𝐸 ∈ V
ceqsex6v.6 ⊢ 𝐹 ∈ V
ceqsex6v.7 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
ceqsex6v.8 ⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
ceqsex6v.9 ⊢ ( 𝑧 = 𝐶 → ( 𝜒 ↔ 𝜃 ) )
ceqsex6v.10 ⊢ ( 𝑤 = 𝐷 → ( 𝜃 ↔ 𝜏 ) )
ceqsex6v.11 ⊢ ( 𝑣 = 𝐸 → ( 𝜏 ↔ 𝜂 ) )
ceqsex6v.12 ⊢ ( 𝑢 = 𝐹 → ( 𝜂 ↔ 𝜁 ) )
Assertion ceqsex6v ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ∧ ( 𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ 𝜑 ) ↔ 𝜁 )

Proof

Step Hyp Ref Expression
1 ceqsex6v.1 ⊢ 𝐴 ∈ V
2 ceqsex6v.2 ⊢ 𝐵 ∈ V
3 ceqsex6v.3 ⊢ 𝐶 ∈ V
4 ceqsex6v.4 ⊢ 𝐷 ∈ V
5 ceqsex6v.5 ⊢ 𝐸 ∈ V
6 ceqsex6v.6 ⊢ 𝐹 ∈ V
7 ceqsex6v.7 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
8 ceqsex6v.8 ⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
9 ceqsex6v.9 ⊢ ( 𝑧 = 𝐶 → ( 𝜒 ↔ 𝜃 ) )
10 ceqsex6v.10 ⊢ ( 𝑤 = 𝐷 → ( 𝜃 ↔ 𝜏 ) )
11 ceqsex6v.11 ⊢ ( 𝑣 = 𝐸 → ( 𝜏 ↔ 𝜂 ) )
12 ceqsex6v.12 ⊢ ( 𝑢 = 𝐹 → ( 𝜂 ↔ 𝜁 ) )
13 3anass ⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ∧ ( 𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ 𝜑 ) ↔ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ∧ ( ( 𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ 𝜑 ) ) )
14 13 3exbii ⊢ ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ∧ ( 𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ 𝜑 ) ↔ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ∧ ( ( 𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ 𝜑 ) ) )
15 19.42vvv ⊢ ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ∧ ( ( 𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ 𝜑 ) ) ↔ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ 𝜑 ) ) )
16 14 15 bitri ⊢ ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ∧ ( 𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ 𝜑 ) ↔ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ 𝜑 ) ) )
17 16 3exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ∧ ( 𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ 𝜑 ) ) )
18 7 anbi2d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ 𝜑 ) ↔ ( ( 𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ 𝜓 ) ) )
19 18 3exbidv ⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ 𝜑 ) ↔ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ 𝜓 ) ) )
20 8 anbi2d ⊢ ( 𝑦 = 𝐵 → ( ( ( 𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ 𝜓 ) ↔ ( ( 𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ 𝜒 ) ) )
21 20 3exbidv ⊢ ( 𝑦 = 𝐵 → ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ 𝜓 ) ↔ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ 𝜒 ) ) )
22 9 anbi2d ⊢ ( 𝑧 = 𝐶 → ( ( ( 𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ 𝜒 ) ↔ ( ( 𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ 𝜃 ) ) )
23 22 3exbidv ⊢ ( 𝑧 = 𝐶 → ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ 𝜒 ) ↔ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ 𝜃 ) ) )
24 1 2 3 19 21 23 ceqsex3v ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ∧ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ 𝜑 ) ) ↔ ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ 𝜃 ) )
25 4 5 6 10 11 12 ceqsex3v ⊢ ( ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ 𝜃 ) ↔ 𝜁 )
26 17 24 25 3bitri ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ∧ ( 𝑤 = 𝐷 ∧ 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ 𝜑 ) ↔ 𝜁 )