Step | Hyp | Ref
| Expression |
1 | | cgsex4g.2 |
. . . . 5
⊢ (𝜒 → (𝜑 ↔ 𝜓)) |
2 | 1 | biimpa 477 |
. . . 4
⊢ ((𝜒 ∧ 𝜑) → 𝜓) |
3 | 2 | exlimivv 1935 |
. . 3
⊢
(∃𝑧∃𝑤(𝜒 ∧ 𝜑) → 𝜓) |
4 | 3 | exlimivv 1935 |
. 2
⊢
(∃𝑥∃𝑦∃𝑧∃𝑤(𝜒 ∧ 𝜑) → 𝜓) |
5 | | elisset 2815 |
. . . . . . 7
⊢ (𝐴 ∈ 𝑅 → ∃𝑥 𝑥 = 𝐴) |
6 | | elisset 2815 |
. . . . . . 7
⊢ (𝐵 ∈ 𝑆 → ∃𝑦 𝑦 = 𝐵) |
7 | 5, 6 | anim12i 613 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵)) |
8 | | elisset 2815 |
. . . . . . 7
⊢ (𝐶 ∈ 𝑅 → ∃𝑧 𝑧 = 𝐶) |
9 | | elisset 2815 |
. . . . . . 7
⊢ (𝐷 ∈ 𝑆 → ∃𝑤 𝑤 = 𝐷) |
10 | 8, 9 | anim12i 613 |
. . . . . 6
⊢ ((𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆) → (∃𝑧 𝑧 = 𝐶 ∧ ∃𝑤 𝑤 = 𝐷)) |
11 | 7, 10 | anim12i 613 |
. . . . 5
⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → ((∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵) ∧ (∃𝑧 𝑧 = 𝐶 ∧ ∃𝑤 𝑤 = 𝐷))) |
12 | | 19.42vv 1961 |
. . . . . . 7
⊢
(∃𝑧∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) ↔ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ ∃𝑧∃𝑤(𝑧 = 𝐶 ∧ 𝑤 = 𝐷))) |
13 | 12 | 2exbii 1851 |
. . . . . 6
⊢
(∃𝑥∃𝑦∃𝑧∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) ↔ ∃𝑥∃𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ ∃𝑧∃𝑤(𝑧 = 𝐶 ∧ 𝑤 = 𝐷))) |
14 | | 19.41vv 1954 |
. . . . . 6
⊢
(∃𝑥∃𝑦((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ ∃𝑧∃𝑤(𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) ↔ (∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ ∃𝑧∃𝑤(𝑧 = 𝐶 ∧ 𝑤 = 𝐷))) |
15 | | exdistrv 1959 |
. . . . . . 7
⊢
(∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ↔ (∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵)) |
16 | | exdistrv 1959 |
. . . . . . 7
⊢
(∃𝑧∃𝑤(𝑧 = 𝐶 ∧ 𝑤 = 𝐷) ↔ (∃𝑧 𝑧 = 𝐶 ∧ ∃𝑤 𝑤 = 𝐷)) |
17 | 15, 16 | anbi12i 627 |
. . . . . 6
⊢
((∃𝑥∃𝑦(𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ ∃𝑧∃𝑤(𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) ↔ ((∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵) ∧ (∃𝑧 𝑧 = 𝐶 ∧ ∃𝑤 𝑤 = 𝐷))) |
18 | 13, 14, 17 | 3bitri 296 |
. . . . 5
⊢
(∃𝑥∃𝑦∃𝑧∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) ↔ ((∃𝑥 𝑥 = 𝐴 ∧ ∃𝑦 𝑦 = 𝐵) ∧ (∃𝑧 𝑧 = 𝐶 ∧ ∃𝑤 𝑤 = 𝐷))) |
19 | 11, 18 | sylibr 233 |
. . . 4
⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → ∃𝑥∃𝑦∃𝑧∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷))) |
20 | | cgsex4g.1 |
. . . . . 6
⊢ (((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) → 𝜒) |
21 | 20 | 2eximi 1838 |
. . . . 5
⊢
(∃𝑧∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) → ∃𝑧∃𝑤𝜒) |
22 | 21 | 2eximi 1838 |
. . . 4
⊢
(∃𝑥∃𝑦∃𝑧∃𝑤((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) ∧ (𝑧 = 𝐶 ∧ 𝑤 = 𝐷)) → ∃𝑥∃𝑦∃𝑧∃𝑤𝜒) |
23 | 19, 22 | syl 17 |
. . 3
⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → ∃𝑥∃𝑦∃𝑧∃𝑤𝜒) |
24 | 1 | biimprcd 249 |
. . . . . 6
⊢ (𝜓 → (𝜒 → 𝜑)) |
25 | 24 | ancld 551 |
. . . . 5
⊢ (𝜓 → (𝜒 → (𝜒 ∧ 𝜑))) |
26 | 25 | 2eximdv 1922 |
. . . 4
⊢ (𝜓 → (∃𝑧∃𝑤𝜒 → ∃𝑧∃𝑤(𝜒 ∧ 𝜑))) |
27 | 26 | 2eximdv 1922 |
. . 3
⊢ (𝜓 → (∃𝑥∃𝑦∃𝑧∃𝑤𝜒 → ∃𝑥∃𝑦∃𝑧∃𝑤(𝜒 ∧ 𝜑))) |
28 | 23, 27 | syl5com 31 |
. 2
⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → (𝜓 → ∃𝑥∃𝑦∃𝑧∃𝑤(𝜒 ∧ 𝜑))) |
29 | 4, 28 | impbid2 225 |
1
⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆)) → (∃𝑥∃𝑦∃𝑧∃𝑤(𝜒 ∧ 𝜑) ↔ 𝜓)) |