axtgupdim2ALTV

Description: Alternate version of axtgupdim2 . (Contributed by Thierry Arnoux, 29-May-2019) (New usage is discouraged.)

	Ref	Expression
Hypotheses	istrkg2d.p	$⊢ P = {Base}_{G}$
	istrkg2d.d	$⊢ \underset{˙}{-} = dist (G)$
	istrkg2d.i	$⊢ I = Itv (G)$
	axtgupdim2ALTV.x	$⊢ φ \to X \in P$
	axtgupdim2ALTV.y	$⊢ φ \to Y \in P$
	axtgupdim2ALTV.z	$⊢ φ \to Z \in P$
	axtgupdim2ALTV.u	$⊢ φ \to U \in P$
	axtgupdim2ALTV.v	$⊢ φ \to V \in P$
	axtgupdim2ALTV.0	$⊢ φ \to U \neq V$
	axtgupdim2ALTV.1	$⊢ φ \to X \underset{˙}{-} U = X \underset{˙}{-} V$
	axtgupdim2ALTV.2	$⊢ φ \to Y \underset{˙}{-} U = Y \underset{˙}{-} V$
	axtgupdim2ALTV.3	$⊢ φ \to Z \underset{˙}{-} U = Z \underset{˙}{-} V$
	axtgupdim2ALTV.g	$⊢ φ \to G \in 𝒢_{Tarski}^{2D}$
Assertion	axtgupdim2ALTV	$⊢ φ \to (Z \in (X I Y) \lor X \in (Z I Y) \lor Y \in (X I Z))$

Proof

Step	Hyp	Ref	Expression
1		istrkg2d.p	$⊢ P = {Base}_{G}$
2		istrkg2d.d	$⊢ \underset{˙}{-} = dist (G)$
3		istrkg2d.i	$⊢ I = Itv (G)$
4		axtgupdim2ALTV.x	$⊢ φ \to X \in P$
5		axtgupdim2ALTV.y	$⊢ φ \to Y \in P$
6		axtgupdim2ALTV.z	$⊢ φ \to Z \in P$
7		axtgupdim2ALTV.u	$⊢ φ \to U \in P$
8		axtgupdim2ALTV.v	$⊢ φ \to V \in P$
9		axtgupdim2ALTV.0	$⊢ φ \to U \neq V$
10		axtgupdim2ALTV.1	$⊢ φ \to X \underset{˙}{-} U = X \underset{˙}{-} V$
11		axtgupdim2ALTV.2	$⊢ φ \to Y \underset{˙}{-} U = Y \underset{˙}{-} V$
12		axtgupdim2ALTV.3	$⊢ φ \to Z \underset{˙}{-} U = Z \underset{˙}{-} V$
13		axtgupdim2ALTV.g	$⊢ φ \to G \in 𝒢_{Tarski}^{2D}$
14	10 11 12	3jca	$⊢ φ \to (X \underset{˙}{-} U = X \underset{˙}{-} V \land Y \underset{˙}{-} U = Y \underset{˙}{-} V \land Z \underset{˙}{-} U = Z \underset{˙}{-} V)$
15	1 2 3	istrkg2d	$⊢ G \in 𝒢_{Tarski}^{2D} \leftrightarrow (G \in V \land (\exists x \in P \exists y \in P \exists z \in P \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)) \land \forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall v \in P (((x \underset{˙}{-} u = x \underset{˙}{-} v \land y \underset{˙}{-} u = y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v) \land u \neq v) \to (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)))))$
16	13 15	sylib	$⊢ φ \to (G \in V \land (\exists x \in P \exists y \in P \exists z \in P \neg (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)) \land \forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall v \in P (((x \underset{˙}{-} u = x \underset{˙}{-} v \land y \underset{˙}{-} u = y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v) \land u \neq v) \to (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)))))$
17	16	simprrd	$⊢ φ \to \forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall v \in P (((x \underset{˙}{-} u = x \underset{˙}{-} v \land y \underset{˙}{-} u = y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v) \land u \neq v) \to (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)))$
18		oveq1	$⊢ x = X \to x \underset{˙}{-} u = X \underset{˙}{-} u$
19		oveq1	$⊢ x = X \to x \underset{˙}{-} v = X \underset{˙}{-} v$
20	18 19	eqeq12d	$⊢ x = X \to (x \underset{˙}{-} u = x \underset{˙}{-} v \leftrightarrow X \underset{˙}{-} u = X \underset{˙}{-} v)$
21	20	3anbi1d	$⊢ x = X \to ((x \underset{˙}{-} u = x \underset{˙}{-} v \land y \underset{˙}{-} u = y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v) \leftrightarrow (X \underset{˙}{-} u = X \underset{˙}{-} v \land y \underset{˙}{-} u = y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v))$
22	21	anbi1d	$⊢ x = X \to (((x \underset{˙}{-} u = x \underset{˙}{-} v \land y \underset{˙}{-} u = y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v) \land u \neq v) \leftrightarrow ((X \underset{˙}{-} u = X \underset{˙}{-} v \land y \underset{˙}{-} u = y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v) \land u \neq v))$
23		oveq1	$⊢ x = X \to x I y = X I y$
24	23	eleq2d	$⊢ x = X \to (z \in (x I y) \leftrightarrow z \in (X I y))$
25		eleq1	$⊢ x = X \to (x \in (z I y) \leftrightarrow X \in (z I y))$
26		oveq1	$⊢ x = X \to x I z = X I z$
27	26	eleq2d	$⊢ x = X \to (y \in (x I z) \leftrightarrow y \in (X I z))$
28	24 25 27	3orbi123d	$⊢ x = X \to ((z \in (x I y) \lor x \in (z I y) \lor y \in (x I z)) \leftrightarrow (z \in (X I y) \lor X \in (z I y) \lor y \in (X I z)))$
29	22 28	imbi12d	$⊢ x = X \to ((((x \underset{˙}{-} u = x \underset{˙}{-} v \land y \underset{˙}{-} u = y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v) \land u \neq v) \to (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))) \leftrightarrow (((X \underset{˙}{-} u = X \underset{˙}{-} v \land y \underset{˙}{-} u = y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v) \land u \neq v) \to (z \in (X I y) \lor X \in (z I y) \lor y \in (X I z))))$
30	29	2ralbidv	$⊢ x = X \to (\forall u \in P \forall v \in P (((x \underset{˙}{-} u = x \underset{˙}{-} v \land y \underset{˙}{-} u = y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v) \land u \neq v) \to (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))) \leftrightarrow \forall u \in P \forall v \in P (((X \underset{˙}{-} u = X \underset{˙}{-} v \land y \underset{˙}{-} u = y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v) \land u \neq v) \to (z \in (X I y) \lor X \in (z I y) \lor y \in (X I z))))$
31		oveq1	$⊢ y = Y \to y \underset{˙}{-} u = Y \underset{˙}{-} u$
32		oveq1	$⊢ y = Y \to y \underset{˙}{-} v = Y \underset{˙}{-} v$
33	31 32	eqeq12d	$⊢ y = Y \to (y \underset{˙}{-} u = y \underset{˙}{-} v \leftrightarrow Y \underset{˙}{-} u = Y \underset{˙}{-} v)$
34	33	3anbi2d	$⊢ y = Y \to ((X \underset{˙}{-} u = X \underset{˙}{-} v \land y \underset{˙}{-} u = y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v) \leftrightarrow (X \underset{˙}{-} u = X \underset{˙}{-} v \land Y \underset{˙}{-} u = Y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v))$
35	34	anbi1d	$⊢ y = Y \to (((X \underset{˙}{-} u = X \underset{˙}{-} v \land y \underset{˙}{-} u = y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v) \land u \neq v) \leftrightarrow ((X \underset{˙}{-} u = X \underset{˙}{-} v \land Y \underset{˙}{-} u = Y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v) \land u \neq v))$
36		oveq2	$⊢ y = Y \to X I y = X I Y$
37	36	eleq2d	$⊢ y = Y \to (z \in (X I y) \leftrightarrow z \in (X I Y))$
38		oveq2	$⊢ y = Y \to z I y = z I Y$
39	38	eleq2d	$⊢ y = Y \to (X \in (z I y) \leftrightarrow X \in (z I Y))$
40		eleq1	$⊢ y = Y \to (y \in (X I z) \leftrightarrow Y \in (X I z))$
41	37 39 40	3orbi123d	$⊢ y = Y \to ((z \in (X I y) \lor X \in (z I y) \lor y \in (X I z)) \leftrightarrow (z \in (X I Y) \lor X \in (z I Y) \lor Y \in (X I z)))$
42	35 41	imbi12d	$⊢ y = Y \to ((((X \underset{˙}{-} u = X \underset{˙}{-} v \land y \underset{˙}{-} u = y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v) \land u \neq v) \to (z \in (X I y) \lor X \in (z I y) \lor y \in (X I z))) \leftrightarrow (((X \underset{˙}{-} u = X \underset{˙}{-} v \land Y \underset{˙}{-} u = Y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v) \land u \neq v) \to (z \in (X I Y) \lor X \in (z I Y) \lor Y \in (X I z))))$
43	42	2ralbidv	$⊢ y = Y \to (\forall u \in P \forall v \in P (((X \underset{˙}{-} u = X \underset{˙}{-} v \land y \underset{˙}{-} u = y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v) \land u \neq v) \to (z \in (X I y) \lor X \in (z I y) \lor y \in (X I z))) \leftrightarrow \forall u \in P \forall v \in P (((X \underset{˙}{-} u = X \underset{˙}{-} v \land Y \underset{˙}{-} u = Y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v) \land u \neq v) \to (z \in (X I Y) \lor X \in (z I Y) \lor Y \in (X I z))))$
44		oveq1	$⊢ z = Z \to z \underset{˙}{-} u = Z \underset{˙}{-} u$
45		oveq1	$⊢ z = Z \to z \underset{˙}{-} v = Z \underset{˙}{-} v$
46	44 45	eqeq12d	$⊢ z = Z \to (z \underset{˙}{-} u = z \underset{˙}{-} v \leftrightarrow Z \underset{˙}{-} u = Z \underset{˙}{-} v)$
47	46	3anbi3d	$⊢ z = Z \to ((X \underset{˙}{-} u = X \underset{˙}{-} v \land Y \underset{˙}{-} u = Y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v) \leftrightarrow (X \underset{˙}{-} u = X \underset{˙}{-} v \land Y \underset{˙}{-} u = Y \underset{˙}{-} v \land Z \underset{˙}{-} u = Z \underset{˙}{-} v))$
48	47	anbi1d	$⊢ z = Z \to (((X \underset{˙}{-} u = X \underset{˙}{-} v \land Y \underset{˙}{-} u = Y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v) \land u \neq v) \leftrightarrow ((X \underset{˙}{-} u = X \underset{˙}{-} v \land Y \underset{˙}{-} u = Y \underset{˙}{-} v \land Z \underset{˙}{-} u = Z \underset{˙}{-} v) \land u \neq v))$
49		eleq1	$⊢ z = Z \to (z \in (X I Y) \leftrightarrow Z \in (X I Y))$
50		oveq1	$⊢ z = Z \to z I Y = Z I Y$
51	50	eleq2d	$⊢ z = Z \to (X \in (z I Y) \leftrightarrow X \in (Z I Y))$
52		oveq2	$⊢ z = Z \to X I z = X I Z$
53	52	eleq2d	$⊢ z = Z \to (Y \in (X I z) \leftrightarrow Y \in (X I Z))$
54	49 51 53	3orbi123d	$⊢ z = Z \to ((z \in (X I Y) \lor X \in (z I Y) \lor Y \in (X I z)) \leftrightarrow (Z \in (X I Y) \lor X \in (Z I Y) \lor Y \in (X I Z)))$
55	48 54	imbi12d	$⊢ z = Z \to ((((X \underset{˙}{-} u = X \underset{˙}{-} v \land Y \underset{˙}{-} u = Y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v) \land u \neq v) \to (z \in (X I Y) \lor X \in (z I Y) \lor Y \in (X I z))) \leftrightarrow (((X \underset{˙}{-} u = X \underset{˙}{-} v \land Y \underset{˙}{-} u = Y \underset{˙}{-} v \land Z \underset{˙}{-} u = Z \underset{˙}{-} v) \land u \neq v) \to (Z \in (X I Y) \lor X \in (Z I Y) \lor Y \in (X I Z))))$
56	55	2ralbidv	$⊢ z = Z \to (\forall u \in P \forall v \in P (((X \underset{˙}{-} u = X \underset{˙}{-} v \land Y \underset{˙}{-} u = Y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v) \land u \neq v) \to (z \in (X I Y) \lor X \in (z I Y) \lor Y \in (X I z))) \leftrightarrow \forall u \in P \forall v \in P (((X \underset{˙}{-} u = X \underset{˙}{-} v \land Y \underset{˙}{-} u = Y \underset{˙}{-} v \land Z \underset{˙}{-} u = Z \underset{˙}{-} v) \land u \neq v) \to (Z \in (X I Y) \lor X \in (Z I Y) \lor Y \in (X I Z))))$
57	30 43 56	rspc3v	$⊢ (X \in P \land Y \in P \land Z \in P) \to (\forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall v \in P (((x \underset{˙}{-} u = x \underset{˙}{-} v \land y \underset{˙}{-} u = y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v) \land u \neq v) \to (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))) \to \forall u \in P \forall v \in P (((X \underset{˙}{-} u = X \underset{˙}{-} v \land Y \underset{˙}{-} u = Y \underset{˙}{-} v \land Z \underset{˙}{-} u = Z \underset{˙}{-} v) \land u \neq v) \to (Z \in (X I Y) \lor X \in (Z I Y) \lor Y \in (X I Z))))$
58	4 5 6 57	syl3anc	$⊢ φ \to (\forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall v \in P (((x \underset{˙}{-} u = x \underset{˙}{-} v \land y \underset{˙}{-} u = y \underset{˙}{-} v \land z \underset{˙}{-} u = z \underset{˙}{-} v) \land u \neq v) \to (z \in (x I y) \lor x \in (z I y) \lor y \in (x I z))) \to \forall u \in P \forall v \in P (((X \underset{˙}{-} u = X \underset{˙}{-} v \land Y \underset{˙}{-} u = Y \underset{˙}{-} v \land Z \underset{˙}{-} u = Z \underset{˙}{-} v) \land u \neq v) \to (Z \in (X I Y) \lor X \in (Z I Y) \lor Y \in (X I Z))))$
59	17 58	mpd	$⊢ φ \to \forall u \in P \forall v \in P (((X \underset{˙}{-} u = X \underset{˙}{-} v \land Y \underset{˙}{-} u = Y \underset{˙}{-} v \land Z \underset{˙}{-} u = Z \underset{˙}{-} v) \land u \neq v) \to (Z \in (X I Y) \lor X \in (Z I Y) \lor Y \in (X I Z)))$
60		oveq2	$⊢ u = U \to X \underset{˙}{-} u = X \underset{˙}{-} U$
61	60	eqeq1d	$⊢ u = U \to (X \underset{˙}{-} u = X \underset{˙}{-} v \leftrightarrow X \underset{˙}{-} U = X \underset{˙}{-} v)$
62		oveq2	$⊢ u = U \to Y \underset{˙}{-} u = Y \underset{˙}{-} U$
63	62	eqeq1d	$⊢ u = U \to (Y \underset{˙}{-} u = Y \underset{˙}{-} v \leftrightarrow Y \underset{˙}{-} U = Y \underset{˙}{-} v)$
64		oveq2	$⊢ u = U \to Z \underset{˙}{-} u = Z \underset{˙}{-} U$
65	64	eqeq1d	$⊢ u = U \to (Z \underset{˙}{-} u = Z \underset{˙}{-} v \leftrightarrow Z \underset{˙}{-} U = Z \underset{˙}{-} v)$
66	61 63 65	3anbi123d	$⊢ u = U \to ((X \underset{˙}{-} u = X \underset{˙}{-} v \land Y \underset{˙}{-} u = Y \underset{˙}{-} v \land Z \underset{˙}{-} u = Z \underset{˙}{-} v) \leftrightarrow (X \underset{˙}{-} U = X \underset{˙}{-} v \land Y \underset{˙}{-} U = Y \underset{˙}{-} v \land Z \underset{˙}{-} U = Z \underset{˙}{-} v))$
67		neeq1	$⊢ u = U \to (u \neq v \leftrightarrow U \neq v)$
68	66 67	anbi12d	$⊢ u = U \to (((X \underset{˙}{-} u = X \underset{˙}{-} v \land Y \underset{˙}{-} u = Y \underset{˙}{-} v \land Z \underset{˙}{-} u = Z \underset{˙}{-} v) \land u \neq v) \leftrightarrow ((X \underset{˙}{-} U = X \underset{˙}{-} v \land Y \underset{˙}{-} U = Y \underset{˙}{-} v \land Z \underset{˙}{-} U = Z \underset{˙}{-} v) \land U \neq v))$
69	68	imbi1d	$⊢ u = U \to ((((X \underset{˙}{-} u = X \underset{˙}{-} v \land Y \underset{˙}{-} u = Y \underset{˙}{-} v \land Z \underset{˙}{-} u = Z \underset{˙}{-} v) \land u \neq v) \to (Z \in (X I Y) \lor X \in (Z I Y) \lor Y \in (X I Z))) \leftrightarrow (((X \underset{˙}{-} U = X \underset{˙}{-} v \land Y \underset{˙}{-} U = Y \underset{˙}{-} v \land Z \underset{˙}{-} U = Z \underset{˙}{-} v) \land U \neq v) \to (Z \in (X I Y) \lor X \in (Z I Y) \lor Y \in (X I Z))))$
70		oveq2	$⊢ v = V \to X \underset{˙}{-} v = X \underset{˙}{-} V$
71	70	eqeq2d	$⊢ v = V \to (X \underset{˙}{-} U = X \underset{˙}{-} v \leftrightarrow X \underset{˙}{-} U = X \underset{˙}{-} V)$
72		oveq2	$⊢ v = V \to Y \underset{˙}{-} v = Y \underset{˙}{-} V$
73	72	eqeq2d	$⊢ v = V \to (Y \underset{˙}{-} U = Y \underset{˙}{-} v \leftrightarrow Y \underset{˙}{-} U = Y \underset{˙}{-} V)$
74		oveq2	$⊢ v = V \to Z \underset{˙}{-} v = Z \underset{˙}{-} V$
75	74	eqeq2d	$⊢ v = V \to (Z \underset{˙}{-} U = Z \underset{˙}{-} v \leftrightarrow Z \underset{˙}{-} U = Z \underset{˙}{-} V)$
76	71 73 75	3anbi123d	$⊢ v = V \to ((X \underset{˙}{-} U = X \underset{˙}{-} v \land Y \underset{˙}{-} U = Y \underset{˙}{-} v \land Z \underset{˙}{-} U = Z \underset{˙}{-} v) \leftrightarrow (X \underset{˙}{-} U = X \underset{˙}{-} V \land Y \underset{˙}{-} U = Y \underset{˙}{-} V \land Z \underset{˙}{-} U = Z \underset{˙}{-} V))$
77		neeq2	$⊢ v = V \to (U \neq v \leftrightarrow U \neq V)$
78	76 77	anbi12d	$⊢ v = V \to (((X \underset{˙}{-} U = X \underset{˙}{-} v \land Y \underset{˙}{-} U = Y \underset{˙}{-} v \land Z \underset{˙}{-} U = Z \underset{˙}{-} v) \land U \neq v) \leftrightarrow ((X \underset{˙}{-} U = X \underset{˙}{-} V \land Y \underset{˙}{-} U = Y \underset{˙}{-} V \land Z \underset{˙}{-} U = Z \underset{˙}{-} V) \land U \neq V))$
79	78	imbi1d	$⊢ v = V \to ((((X \underset{˙}{-} U = X \underset{˙}{-} v \land Y \underset{˙}{-} U = Y \underset{˙}{-} v \land Z \underset{˙}{-} U = Z \underset{˙}{-} v) \land U \neq v) \to (Z \in (X I Y) \lor X \in (Z I Y) \lor Y \in (X I Z))) \leftrightarrow (((X \underset{˙}{-} U = X \underset{˙}{-} V \land Y \underset{˙}{-} U = Y \underset{˙}{-} V \land Z \underset{˙}{-} U = Z \underset{˙}{-} V) \land U \neq V) \to (Z \in (X I Y) \lor X \in (Z I Y) \lor Y \in (X I Z))))$
80	69 79	rspc2v	$⊢ (U \in P \land V \in P) \to (\forall u \in P \forall v \in P (((X \underset{˙}{-} u = X \underset{˙}{-} v \land Y \underset{˙}{-} u = Y \underset{˙}{-} v \land Z \underset{˙}{-} u = Z \underset{˙}{-} v) \land u \neq v) \to (Z \in (X I Y) \lor X \in (Z I Y) \lor Y \in (X I Z))) \to (((X \underset{˙}{-} U = X \underset{˙}{-} V \land Y \underset{˙}{-} U = Y \underset{˙}{-} V \land Z \underset{˙}{-} U = Z \underset{˙}{-} V) \land U \neq V) \to (Z \in (X I Y) \lor X \in (Z I Y) \lor Y \in (X I Z))))$
81	7 8 80	syl2anc	$⊢ φ \to (\forall u \in P \forall v \in P (((X \underset{˙}{-} u = X \underset{˙}{-} v \land Y \underset{˙}{-} u = Y \underset{˙}{-} v \land Z \underset{˙}{-} u = Z \underset{˙}{-} v) \land u \neq v) \to (Z \in (X I Y) \lor X \in (Z I Y) \lor Y \in (X I Z))) \to (((X \underset{˙}{-} U = X \underset{˙}{-} V \land Y \underset{˙}{-} U = Y \underset{˙}{-} V \land Z \underset{˙}{-} U = Z \underset{˙}{-} V) \land U \neq V) \to (Z \in (X I Y) \lor X \in (Z I Y) \lor Y \in (X I Z))))$
82	59 81	mpd	$⊢ φ \to (((X \underset{˙}{-} U = X \underset{˙}{-} V \land Y \underset{˙}{-} U = Y \underset{˙}{-} V \land Z \underset{˙}{-} U = Z \underset{˙}{-} V) \land U \neq V) \to (Z \in (X I Y) \lor X \in (Z I Y) \lor Y \in (X I Z)))$
83	14 9 82	mp2and	$⊢ φ \to (Z \in (X I Y) \lor X \in (Z I Y) \lor Y \in (X I Z))$

Metamath Proof Explorer

Theorem axtgupdim2ALTV

Proof