Metamath Proof Explorer

Theorem cgsex4gOLDOLD

Description: Obsolete version of cgsex4g as of 28-Jun-2024. (Contributed by NM, 5-Aug-1995) Avoid ax-10 . (Revised by Gino Giotto, 20-Aug-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses cgsex4gOLDOLD.1 ⊢x=A∧y=B∧z=C∧w=D→χ
cgsex4gOLDOLD.2 ⊢χ→φ↔ψ
Assertion cgsex4gOLDOLD ⊢A∈R∧B∈S∧C∈R∧D∈S→∃x∃y∃z∃wχ∧φ↔ψ

Proof

Step Hyp Ref Expression
1 cgsex4gOLDOLD.1 ⊢x=A∧y=B∧z=C∧w=D→χ
2 cgsex4gOLDOLD.2 ⊢χ→φ↔ψ
3 2 biimpa ⊢χ∧φ→ψ
4 3 exlimivv ⊢∃z∃wχ∧φ→ψ
5 4 exlimivv ⊢∃x∃y∃z∃wχ∧φ→ψ
6 elisset ⊢A∈R→∃xx=A
7 elisset ⊢B∈S→∃yy=B
8 6 7 anim12i ⊢A∈R∧B∈S→∃xx=A∧∃yy=B
9 exdistrv ⊢∃x∃yx=A∧y=B↔∃xx=A∧∃yy=B
10 8 9 sylibr ⊢A∈R∧B∈S→∃x∃yx=A∧y=B
11 elisset ⊢C∈R→∃zz=C
12 elisset ⊢D∈S→∃ww=D
13 11 12 anim12i ⊢C∈R∧D∈S→∃zz=C∧∃ww=D
14 exdistrv ⊢∃z∃wz=C∧w=D↔∃zz=C∧∃ww=D
15 13 14 sylibr ⊢C∈R∧D∈S→∃z∃wz=C∧w=D
16 10 15 anim12i ⊢A∈R∧B∈S∧C∈R∧D∈S→∃x∃yx=A∧y=B∧∃z∃wz=C∧w=D
17 excom ⊢∃y∃z∃wx=A∧y=B∧z=C∧w=D↔∃z∃y∃wx=A∧y=B∧z=C∧w=D
18 17 exbii ⊢∃x∃y∃z∃wx=A∧y=B∧z=C∧w=D↔∃x∃z∃y∃wx=A∧y=B∧z=C∧w=D
19 4exdistrv ⊢∃x∃z∃y∃wx=A∧y=B∧z=C∧w=D↔∃x∃yx=A∧y=B∧∃z∃wz=C∧w=D
20 18 19 bitri ⊢∃x∃y∃z∃wx=A∧y=B∧z=C∧w=D↔∃x∃yx=A∧y=B∧∃z∃wz=C∧w=D
21 16 20 sylibr ⊢A∈R∧B∈S∧C∈R∧D∈S→∃x∃y∃z∃wx=A∧y=B∧z=C∧w=D
22 1 2eximi ⊢∃z∃wx=A∧y=B∧z=C∧w=D→∃z∃wχ
23 22 2eximi ⊢∃x∃y∃z∃wx=A∧y=B∧z=C∧w=D→∃x∃y∃z∃wχ
24 21 23 syl ⊢A∈R∧B∈S∧C∈R∧D∈S→∃x∃y∃z∃wχ
25 2 biimprcd ⊢ψ→χ→φ
26 25 ancld ⊢ψ→χ→χ∧φ
27 26 2eximdv ⊢ψ→∃z∃wχ→∃z∃wχ∧φ
28 27 2eximdv ⊢ψ→∃x∃y∃z∃wχ→∃x∃y∃z∃wχ∧φ
29 24 28 syl5com ⊢A∈R∧B∈S∧C∈R∧D∈S→ψ→∃x∃y∃z∃wχ∧φ
30 5 29 impbid2 ⊢A∈R∧B∈S∧C∈R∧D∈S→∃x∃y∃z∃wχ∧φ↔ψ