Metamath Proof Explorer


Theorem cgsex4gOLD

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 cgsex4gOLD.1 x = A y = B z = C w = D χ
cgsex4gOLD.2 χ φ ψ
Assertion cgsex4gOLD A R B S C R D S x y z w χ φ ψ

Proof

Step Hyp Ref Expression
1 cgsex4gOLD.1 x = A y = B z = C w = D χ
2 cgsex4gOLD.2 χ φ ψ
3 2 biimpa χ φ ψ
4 3 exlimivv z w χ φ ψ
5 4 exlimivv x y z w χ φ ψ
6 elisset A R x x = A
7 elisset B S y y = B
8 6 7 anim12i A R B S x x = A y y = B
9 exdistrv x y x = A y = B x x = A y y = B
10 8 9 sylibr A R B S x y x = A y = B
11 elisset C R z z = C
12 elisset D S w w = D
13 11 12 anim12i C R D S z z = C w w = D
14 exdistrv z w z = C w = D z z = C w w = D
15 13 14 sylibr C R D S z w z = C w = D
16 10 15 anim12i A R B S C R D S x y x = A y = B z w z = C w = D
17 excom y z w x = A y = B z = C w = D z y w x = A y = B z = C w = D
18 17 exbii x y z w x = A y = B z = C w = D x z y w x = A y = B z = C w = D
19 4exdistrv x z y w x = A y = B z = C w = D x y x = A y = B z w z = C w = D
20 18 19 bitri x y z w x = A y = B z = C w = D x y x = A y = B z w z = C w = D
21 16 20 sylibr A R B S C R D S x y z w x = A y = B z = C w = D
22 1 2eximi z w x = A y = B z = C w = D z w χ
23 22 2eximi x y z w x = 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 χ φ ψ