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 ⊢ 𝐴 ∈ V
ceqsex3v.2 ⊢ 𝐵 ∈ V
ceqsex3v.3 ⊢ 𝐶 ∈ V
ceqsex3v.4 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
ceqsex3v.5 ⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
ceqsex3v.6 ⊢ ( 𝑧 = 𝐶 → ( 𝜒 ↔ 𝜃 ) )
Assertion ceqsex3v ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ∧ 𝜑 ) ↔ 𝜃 )

Proof

Step Hyp Ref Expression
1 ceqsex3v.1 ⊢ 𝐴 ∈ V
2 ceqsex3v.2 ⊢ 𝐵 ∈ V
3 ceqsex3v.3 ⊢ 𝐶 ∈ V
4 ceqsex3v.4 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
5 ceqsex3v.5 ⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
6 ceqsex3v.6 ⊢ ( 𝑧 = 𝐶 → ( 𝜒 ↔ 𝜃 ) )
7 anass ⊢ ( ( ( 𝑥 = 𝐴 ∧ ( 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ) ∧ 𝜑 ) ↔ ( 𝑥 = 𝐴 ∧ ( ( 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ∧ 𝜑 ) ) )
8 3anass ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ↔ ( 𝑥 = 𝐴 ∧ ( 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ) )
9 8 anbi1i ⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ∧ 𝜑 ) ↔ ( ( 𝑥 = 𝐴 ∧ ( 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ) ∧ 𝜑 ) )
10 df-3an ⊢ ( ( 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ∧ 𝜑 ) ↔ ( ( 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ∧ 𝜑 ) )
11 10 anbi2i ⊢ ( ( 𝑥 = 𝐴 ∧ ( 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ∧ 𝜑 ) ) ↔ ( 𝑥 = 𝐴 ∧ ( ( 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ∧ 𝜑 ) ) )
12 7 9 11 3bitr4i ⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ∧ 𝜑 ) ↔ ( 𝑥 = 𝐴 ∧ ( 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ∧ 𝜑 ) ) )
13 12 2exbii ⊢ ( ∃ 𝑦 ∃ 𝑧 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ∧ 𝜑 ) ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = 𝐴 ∧ ( 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ∧ 𝜑 ) ) )
14 19.42vv ⊢ ( ∃ 𝑦 ∃ 𝑧 ( 𝑥 = 𝐴 ∧ ( 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ∧ 𝜑 ) ) ↔ ( 𝑥 = 𝐴 ∧ ∃ 𝑦 ∃ 𝑧 ( 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ∧ 𝜑 ) ) )
15 13 14 bitri ⊢ ( ∃ 𝑦 ∃ 𝑧 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ∧ 𝜑 ) ↔ ( 𝑥 = 𝐴 ∧ ∃ 𝑦 ∃ 𝑧 ( 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ∧ 𝜑 ) ) )
16 15 exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ∧ 𝜑 ) ↔ ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ∃ 𝑦 ∃ 𝑧 ( 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ∧ 𝜑 ) ) )
17 4 3anbi3d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ∧ 𝜑 ) ↔ ( 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ∧ 𝜓 ) ) )
18 17 2exbidv ⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑦 ∃ 𝑧 ( 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ∧ 𝜑 ) ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ∧ 𝜓 ) ) )
19 1 18 ceqsexv ⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ∃ 𝑦 ∃ 𝑧 ( 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ∧ 𝜑 ) ) ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ∧ 𝜓 ) )
20 2 3 5 6 ceqsex2v ⊢ ( ∃ 𝑦 ∃ 𝑧 ( 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ∧ 𝜓 ) ↔ 𝜃 )
21 19 20 bitri ⊢ ( ∃ 𝑥 ( 𝑥 = 𝐴 ∧ ∃ 𝑦 ∃ 𝑧 ( 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ∧ 𝜑 ) ) ↔ 𝜃 )
22 16 21 bitri ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ∧ 𝑧 = 𝐶 ) ∧ 𝜑 ) ↔ 𝜃 )