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

Proof

Step Hyp Ref Expression
1 ceqsex8v.1 ⊢ 𝐴 ∈ V
2 ceqsex8v.2 ⊢ 𝐵 ∈ V
3 ceqsex8v.3 ⊢ 𝐶 ∈ V
4 ceqsex8v.4 ⊢ 𝐷 ∈ V
5 ceqsex8v.5 ⊢ 𝐸 ∈ V
6 ceqsex8v.6 ⊢ 𝐹 ∈ V
7 ceqsex8v.7 ⊢ 𝐺 ∈ V
8 ceqsex8v.8 ⊢ 𝐻 ∈ V
9 ceqsex8v.9 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
10 ceqsex8v.10 ⊢ ( 𝑦 = 𝐵 → ( 𝜓 ↔ 𝜒 ) )
11 ceqsex8v.11 ⊢ ( 𝑧 = 𝐶 → ( 𝜒 ↔ 𝜃 ) )
12 ceqsex8v.12 ⊢ ( 𝑤 = 𝐷 → ( 𝜃 ↔ 𝜏 ) )
13 ceqsex8v.13 ⊢ ( 𝑣 = 𝐸 → ( 𝜏 ↔ 𝜂 ) )
14 ceqsex8v.14 ⊢ ( 𝑢 = 𝐹 → ( 𝜂 ↔ 𝜁 ) )
15 ceqsex8v.15 ⊢ ( 𝑡 = 𝐺 → ( 𝜁 ↔ 𝜎 ) )
16 ceqsex8v.16 ⊢ ( 𝑠 = 𝐻 → ( 𝜎 ↔ 𝜌 ) )
17 19.42vv ⊢ ( ∃ 𝑡 ∃ 𝑠 ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ) ∧ ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜑 ) ) ↔ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ) ∧ ∃ 𝑡 ∃ 𝑠 ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜑 ) ) )
18 17 2exbii ⊢ ( ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ∃ 𝑠 ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ) ∧ ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜑 ) ) ↔ ∃ 𝑣 ∃ 𝑢 ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ) ∧ ∃ 𝑡 ∃ 𝑠 ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜑 ) ) )
19 19.42vv ⊢ ( ∃ 𝑣 ∃ 𝑢 ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ) ∧ ∃ 𝑡 ∃ 𝑠 ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜑 ) ) ↔ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ) ∧ ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ∃ 𝑠 ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜑 ) ) )
20 18 19 bitri ⊢ ( ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ∃ 𝑠 ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ) ∧ ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜑 ) ) ↔ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ) ∧ ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ∃ 𝑠 ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜑 ) ) )
21 3anass ⊢ ( ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ) ∧ ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ) ∧ 𝜑 ) ↔ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ) ∧ ( ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ) ∧ 𝜑 ) ) )
22 df-3an ⊢ ( ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜑 ) ↔ ( ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ) ∧ 𝜑 ) )
23 22 anbi2i ⊢ ( ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ) ∧ ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜑 ) ) ↔ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ) ∧ ( ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ) ∧ 𝜑 ) ) )
24 21 23 bitr4i ⊢ ( ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ) ∧ ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ) ∧ 𝜑 ) ↔ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ) ∧ ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜑 ) ) )
25 24 2exbii ⊢ ( ∃ 𝑡 ∃ 𝑠 ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ) ∧ ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ) ∧ 𝜑 ) ↔ ∃ 𝑡 ∃ 𝑠 ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ) ∧ ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜑 ) ) )
26 25 2exbii ⊢ ( ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ∃ 𝑠 ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ) ∧ ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ) ∧ 𝜑 ) ↔ ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ∃ 𝑠 ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ) ∧ ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜑 ) ) )
27 df-3an ⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ∧ ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ∃ 𝑠 ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜑 ) ) ↔ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ) ∧ ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ∃ 𝑠 ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜑 ) ) )
28 20 26 27 3bitr4i ⊢ ( ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ∃ 𝑠 ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ) ∧ ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ) ∧ 𝜑 ) ↔ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ∧ ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ∃ 𝑠 ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜑 ) ) )
29 28 2exbii ⊢ ( ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ∃ 𝑠 ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ) ∧ ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ) ∧ 𝜑 ) ↔ ∃ 𝑧 ∃ 𝑤 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ∧ ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ∃ 𝑠 ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜑 ) ) )
30 29 2exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ∃ 𝑠 ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ) ∧ ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ) ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ∧ ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ∃ 𝑠 ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜑 ) ) )
31 9 3anbi3d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜑 ) ↔ ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜓 ) ) )
32 31 4exbidv ⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ∃ 𝑠 ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜑 ) ↔ ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ∃ 𝑠 ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜓 ) ) )
33 10 3anbi3d ⊢ ( 𝑦 = 𝐵 → ( ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜓 ) ↔ ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜒 ) ) )
34 33 4exbidv ⊢ ( 𝑦 = 𝐵 → ( ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ∃ 𝑠 ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜓 ) ↔ ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ∃ 𝑠 ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜒 ) ) )
35 11 3anbi3d ⊢ ( 𝑧 = 𝐶 → ( ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜒 ) ↔ ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜃 ) ) )
36 35 4exbidv ⊢ ( 𝑧 = 𝐶 → ( ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ∃ 𝑠 ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜒 ) ↔ ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ∃ 𝑠 ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜃 ) ) )
37 12 3anbi3d ⊢ ( 𝑤 = 𝐷 → ( ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜃 ) ↔ ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜏 ) ) )
38 37 4exbidv ⊢ ( 𝑤 = 𝐷 → ( ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ∃ 𝑠 ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜃 ) ↔ ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ∃ 𝑠 ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜏 ) ) )
39 1 2 3 4 32 34 36 38 ceqsex4v ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ∧ ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ∃ 𝑠 ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜑 ) ) ↔ ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ∃ 𝑠 ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜏 ) )
40 5 6 7 8 13 14 15 16 ceqsex4v ⊢ ( ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ∃ 𝑠 ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ∧ 𝜏 ) ↔ 𝜌 )
41 30 39 40 3bitri ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ∃ 𝑣 ∃ 𝑢 ∃ 𝑡 ∃ 𝑠 ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ) ∧ ( ( 𝑣 = 𝐸 ∧ 𝑢 = 𝐹 ) ∧ ( 𝑡 = 𝐺 ∧ 𝑠 = 𝐻 ) ) ∧ 𝜑 ) ↔ 𝜌 )