Theorem axtg5seg

Description: Five segments axiom, Axiom A5 of Schwabhauser p. 11. Take two triangles X Z U and A C V , a point Y on X Z , and a point B on A C . If all corresponding line segments except for Z U and C V are congruent ( i.e., X Y .A B , Y Z .B C , X U .A V , and Y U .B V ), then Z U and C V are also congruent. As noted in Axiom 5 of Tarski1999 p. 178, "this axiom is similar in character to the well-known theorems of Euclidean geometry that allow one to conclude, from hypotheses about the congruence of certain corresponding sides and angles in two triangles, the congruence of other corresponding sides and angles." (Contributed by Thierry Arnoux, 14-Mar-2019)

	Ref	Expression
Hypotheses	axtrkg.p	$$⊢P={\mathrm{Base}}_G$$
	axtrkg.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	axtrkg.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	axtrkg.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	axtg5seg.1	$$⊢\phi \to X\in P$$
	axtg5seg.2	$$⊢\phi \to Y\in P$$
	axtg5seg.3	$$⊢\phi \to Z\in P$$
	axtg5seg.4	$$⊢\phi \to A\in P$$
	axtg5seg.5	$$⊢\phi \to B\in P$$
	axtg5seg.6	$$⊢\phi \to C\in P$$
	axtg5seg.7	$$⊢\phi \to U\in P$$
	axtg5seg.8	$$⊢\phi \to V\in P$$
	axtg5seg.9	$$⊢\phi \to X\ne Y$$
	axtg5seg.10	$$⊢\phi \to Y\in \left(XIZ\right)$$
	axtg5seg.11	$$⊢\phi \to B\in \left(AIC\right)$$
	axtg5seg.12	$$⊢\phi \to X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}B$$
	axtg5seg.13	$$⊢\phi \to Y\underset{\dot{}}{-}Z=B\underset{\dot{}}{-}C$$
	axtg5seg.14	$$⊢\phi \to X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}V$$
	axtg5seg.15	$$⊢\phi \to Y\underset{\dot{}}{-}U=B\underset{\dot{}}{-}V$$
Assertion	axtg5seg	$$⊢\phi \to Z\underset{\dot{}}{-}U=C\underset{\dot{}}{-}V$$

Proof

Step	Hyp	Ref	Expression
1		axtrkg.p	$$⊢P={\mathrm{Base}}_G$$
2		axtrkg.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		axtrkg.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		axtrkg.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
5		axtg5seg.1	$$⊢\phi \to X\in P$$
6		axtg5seg.2	$$⊢\phi \to Y\in P$$
7		axtg5seg.3	$$⊢\phi \to Z\in P$$
8		axtg5seg.4	$$⊢\phi \to A\in P$$
9		axtg5seg.5	$$⊢\phi \to B\in P$$
10		axtg5seg.6	$$⊢\phi \to C\in P$$
11		axtg5seg.7	$$⊢\phi \to U\in P$$
12		axtg5seg.8	$$⊢\phi \to V\in P$$
13		axtg5seg.9	$$⊢\phi \to X\ne Y$$
14		axtg5seg.10	$$⊢\phi \to Y\in \left(XIZ\right)$$
15		axtg5seg.11	$$⊢\phi \to B\in \left(AIC\right)$$
16		axtg5seg.12	$$⊢\phi \to X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}B$$
17		axtg5seg.13	$$⊢\phi \to Y\underset{\dot{}}{-}Z=B\underset{\dot{}}{-}C$$
18		axtg5seg.14	$$⊢\phi \to X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}V$$
19		axtg5seg.15	$$⊢\phi \to Y\underset{\dot{}}{-}U=B\underset{\dot{}}{-}V$$
20		df-trkg	$$⊢{𝒢}_{\mathrm{Tarski}}=\left({𝒢}_{\mathrm{Tarski}}^C\cap {𝒢}_{\mathrm{Tarski}}^B\right)\cap \left({𝒢}_{\mathrm{Tarski}}^{\mathrm{CB}}\cap \left\{f|\underset{\dot{}}{[}{\mathrm{Base}}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Itv}\left(f\right)/i\underset{\dot{}}{]}{Line}_{𝒢}\left(f\right)=\left(x\in p,y\in \left(p\setminus \left\{x\right\}\right)⟼\left\{z\in p|\left(z\in \left(xiy\right)\vee x\in \left(ziy\right)\vee y\in \left(xiz\right)\right)\right\}\right)\right\}\right)$$
21		inss2	$$⊢\left({𝒢}_{\mathrm{Tarski}}^C\cap {𝒢}_{\mathrm{Tarski}}^B\right)\cap \left({𝒢}_{\mathrm{Tarski}}^{\mathrm{CB}}\cap \left\{f|\underset{\dot{}}{[}{\mathrm{Base}}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Itv}\left(f\right)/i\underset{\dot{}}{]}{Line}_{𝒢}\left(f\right)=\left(x\in p,y\in \left(p\setminus \left\{x\right\}\right)⟼\left\{z\in p|\left(z\in \left(xiy\right)\vee x\in \left(ziy\right)\vee y\in \left(xiz\right)\right)\right\}\right)\right\}\right)\subseteq {𝒢}_{\mathrm{Tarski}}^{\mathrm{CB}}\cap \left\{f|\underset{\dot{}}{[}{\mathrm{Base}}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Itv}\left(f\right)/i\underset{\dot{}}{]}{Line}_{𝒢}\left(f\right)=\left(x\in p,y\in \left(p\setminus \left\{x\right\}\right)⟼\left\{z\in p|\left(z\in \left(xiy\right)\vee x\in \left(ziy\right)\vee y\in \left(xiz\right)\right)\right\}\right)\right\}$$
22		inss1	$$⊢{𝒢}_{\mathrm{Tarski}}^{\mathrm{CB}}\cap \left\{f|\underset{\dot{}}{[}{\mathrm{Base}}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Itv}\left(f\right)/i\underset{\dot{}}{]}{Line}_{𝒢}\left(f\right)=\left(x\in p,y\in \left(p\setminus \left\{x\right\}\right)⟼\left\{z\in p|\left(z\in \left(xiy\right)\vee x\in \left(ziy\right)\vee y\in \left(xiz\right)\right)\right\}\right)\right\}\subseteq {𝒢}_{\mathrm{Tarski}}^{\mathrm{CB}}$$
23	21 22	sstri	$$⊢\left({𝒢}_{\mathrm{Tarski}}^C\cap {𝒢}_{\mathrm{Tarski}}^B\right)\cap \left({𝒢}_{\mathrm{Tarski}}^{\mathrm{CB}}\cap \left\{f|\underset{\dot{}}{[}{\mathrm{Base}}_f/p\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{Itv}\left(f\right)/i\underset{\dot{}}{]}{Line}_{𝒢}\left(f\right)=\left(x\in p,y\in \left(p\setminus \left\{x\right\}\right)⟼\left\{z\in p|\left(z\in \left(xiy\right)\vee x\in \left(ziy\right)\vee y\in \left(xiz\right)\right)\right\}\right)\right\}\right)\subseteq {𝒢}_{\mathrm{Tarski}}^{\mathrm{CB}}$$
24	20 23	eqsstri	$$⊢{𝒢}_{\mathrm{Tarski}}\subseteq {𝒢}_{\mathrm{Tarski}}^{\mathrm{CB}}$$
25	24 4	sselid	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}^{\mathrm{CB}}$$
26	1 2 3	istrkgcb	$$⊢G\in {𝒢}_{\mathrm{Tarski}}^{\mathrm{CB}}\leftrightarrow \left(G\in \mathrm{V}\wedge \left(\forall x\in P\forall y\in P\forall z\in P\forall u\in P\forall a\in P\forall b\in P\forall c\in P\forall v\in P\left(\left(\left(x\ne y\wedge y\in \left(xIz\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(x\underset{\dot{}}{-}y=a\underset{\dot{}}{-}b\wedge y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(x\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)\wedge \forall x\in P\forall y\in P\forall a\in P\forall b\in P\exists z\in P\left(y\in \left(xIz\right)\wedge y\underset{\dot{}}{-}z=a\underset{\dot{}}{-}b\right)\right)\right)$$
27	26	simprbi	$$⊢G\in {𝒢}_{\mathrm{Tarski}}^{\mathrm{CB}}\to \left(\forall x\in P\forall y\in P\forall z\in P\forall u\in P\forall a\in P\forall b\in P\forall c\in P\forall v\in P\left(\left(\left(x\ne y\wedge y\in \left(xIz\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(x\underset{\dot{}}{-}y=a\underset{\dot{}}{-}b\wedge y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(x\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)\wedge \forall x\in P\forall y\in P\forall a\in P\forall b\in P\exists z\in P\left(y\in \left(xIz\right)\wedge y\underset{\dot{}}{-}z=a\underset{\dot{}}{-}b\right)\right)$$
28	27	simpld	$$⊢G\in {𝒢}_{\mathrm{Tarski}}^{\mathrm{CB}}\to \forall x\in P\forall y\in P\forall z\in P\forall u\in P\forall a\in P\forall b\in P\forall c\in P\forall v\in P\left(\left(\left(x\ne y\wedge y\in \left(xIz\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(x\underset{\dot{}}{-}y=a\underset{\dot{}}{-}b\wedge y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(x\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)$$
29	25 28	syl	$$⊢\phi \to \forall x\in P\forall y\in P\forall z\in P\forall u\in P\forall a\in P\forall b\in P\forall c\in P\forall v\in P\left(\left(\left(x\ne y\wedge y\in \left(xIz\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(x\underset{\dot{}}{-}y=a\underset{\dot{}}{-}b\wedge y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(x\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)$$
30		neeq1	$$⊢x=X\to \left(x\ne y\leftrightarrow X\ne y\right)$$
31		oveq1	$$⊢x=X\to xIz=XIz$$
32	31	eleq2d	$$⊢x=X\to \left(y\in \left(xIz\right)\leftrightarrow y\in \left(XIz\right)\right)$$
33	30 32	3anbi12d	$$⊢x=X\to \left(\left(x\ne y\wedge y\in \left(xIz\right)\wedge b\in \left(aIc\right)\right)\leftrightarrow \left(X\ne y\wedge y\in \left(XIz\right)\wedge b\in \left(aIc\right)\right)\right)$$
34		oveq1	$$⊢x=X\to x\underset{\dot{}}{-}y=X\underset{\dot{}}{-}y$$
35	34	eqeq1d	$$⊢x=X\to \left(x\underset{\dot{}}{-}y=a\underset{\dot{}}{-}b\leftrightarrow X\underset{\dot{}}{-}y=a\underset{\dot{}}{-}b\right)$$
36	35	anbi1d	$$⊢x=X\to \left(\left(x\underset{\dot{}}{-}y=a\underset{\dot{}}{-}b\wedge y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\leftrightarrow \left(X\underset{\dot{}}{-}y=a\underset{\dot{}}{-}b\wedge y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\right)$$
37		oveq1	$$⊢x=X\to x\underset{\dot{}}{-}u=X\underset{\dot{}}{-}u$$
38	37	eqeq1d	$$⊢x=X\to \left(x\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\leftrightarrow X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\right)$$
39	38	anbi1d	$$⊢x=X\to \left(\left(x\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\leftrightarrow \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)$$
40	36 39	anbi12d	$$⊢x=X\to \left(\left(\left(x\underset{\dot{}}{-}y=a\underset{\dot{}}{-}b\wedge y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(x\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\leftrightarrow \left(\left(X\underset{\dot{}}{-}y=a\underset{\dot{}}{-}b\wedge y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)$$
41	33 40	anbi12d	$$⊢x=X\to \left(\left(\left(x\ne y\wedge y\in \left(xIz\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(x\underset{\dot{}}{-}y=a\underset{\dot{}}{-}b\wedge y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(x\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\leftrightarrow \left(\left(X\ne y\wedge y\in \left(XIz\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}y=a\underset{\dot{}}{-}b\wedge y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\right)$$
42	41	imbi1d	$$⊢x=X\to \left(\left(\left(\left(x\ne y\wedge y\in \left(xIz\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(x\underset{\dot{}}{-}y=a\underset{\dot{}}{-}b\wedge y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(x\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)\leftrightarrow \left(\left(\left(X\ne y\wedge y\in \left(XIz\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}y=a\underset{\dot{}}{-}b\wedge y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)\right)$$
43	42	ralbidv	$$⊢x=X\to \left(\forall v\in P\left(\left(\left(x\ne y\wedge y\in \left(xIz\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(x\underset{\dot{}}{-}y=a\underset{\dot{}}{-}b\wedge y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(x\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)\leftrightarrow \forall v\in P\left(\left(\left(X\ne y\wedge y\in \left(XIz\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}y=a\underset{\dot{}}{-}b\wedge y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)\right)$$
44	43	2ralbidv	$$⊢x=X\to \left(\forall b\in P\forall c\in P\forall v\in P\left(\left(\left(x\ne y\wedge y\in \left(xIz\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(x\underset{\dot{}}{-}y=a\underset{\dot{}}{-}b\wedge y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(x\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)\leftrightarrow \forall b\in P\forall c\in P\forall v\in P\left(\left(\left(X\ne y\wedge y\in \left(XIz\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}y=a\underset{\dot{}}{-}b\wedge y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)\right)$$
45	44	2ralbidv	$$⊢x=X\to \left(\forall u\in P\forall a\in P\forall b\in P\forall c\in P\forall v\in P\left(\left(\left(x\ne y\wedge y\in \left(xIz\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(x\underset{\dot{}}{-}y=a\underset{\dot{}}{-}b\wedge y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(x\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)\leftrightarrow \forall u\in P\forall a\in P\forall b\in P\forall c\in P\forall v\in P\left(\left(\left(X\ne y\wedge y\in \left(XIz\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}y=a\underset{\dot{}}{-}b\wedge y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)\right)$$
46		neeq2	$$⊢y=Y\to \left(X\ne y\leftrightarrow X\ne Y\right)$$
47		eleq1	$$⊢y=Y\to \left(y\in \left(XIz\right)\leftrightarrow Y\in \left(XIz\right)\right)$$
48	46 47	3anbi12d	$$⊢y=Y\to \left(\left(X\ne y\wedge y\in \left(XIz\right)\wedge b\in \left(aIc\right)\right)\leftrightarrow \left(X\ne Y\wedge Y\in \left(XIz\right)\wedge b\in \left(aIc\right)\right)\right)$$
49		oveq2	$$⊢y=Y\to X\underset{\dot{}}{-}y=X\underset{\dot{}}{-}Y$$
50	49	eqeq1d	$$⊢y=Y\to \left(X\underset{\dot{}}{-}y=a\underset{\dot{}}{-}b\leftrightarrow X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\right)$$
51		oveq1	$$⊢y=Y\to y\underset{\dot{}}{-}z=Y\underset{\dot{}}{-}z$$
52	51	eqeq1d	$$⊢y=Y\to \left(y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\leftrightarrow Y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)$$
53	50 52	anbi12d	$$⊢y=Y\to \left(\left(X\underset{\dot{}}{-}y=a\underset{\dot{}}{-}b\wedge y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\leftrightarrow \left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\right)$$
54		oveq1	$$⊢y=Y\to y\underset{\dot{}}{-}u=Y\underset{\dot{}}{-}u$$
55	54	eqeq1d	$$⊢y=Y\to \left(y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\leftrightarrow Y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)$$
56	55	anbi2d	$$⊢y=Y\to \left(\left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\leftrightarrow \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)$$
57	53 56	anbi12d	$$⊢y=Y\to \left(\left(\left(X\underset{\dot{}}{-}y=a\underset{\dot{}}{-}b\wedge y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\leftrightarrow \left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)$$
58	48 57	anbi12d	$$⊢y=Y\to \left(\left(\left(X\ne y\wedge y\in \left(XIz\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}y=a\underset{\dot{}}{-}b\wedge y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\leftrightarrow \left(\left(X\ne Y\wedge Y\in \left(XIz\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\right)$$
59	58	imbi1d	$$⊢y=Y\to \left(\left(\left(\left(X\ne y\wedge y\in \left(XIz\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}y=a\underset{\dot{}}{-}b\wedge y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)\leftrightarrow \left(\left(\left(X\ne Y\wedge Y\in \left(XIz\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)\right)$$
60	59	ralbidv	$$⊢y=Y\to \left(\forall v\in P\left(\left(\left(X\ne y\wedge y\in \left(XIz\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}y=a\underset{\dot{}}{-}b\wedge y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)\leftrightarrow \forall v\in P\left(\left(\left(X\ne Y\wedge Y\in \left(XIz\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)\right)$$
61	60	2ralbidv	$$⊢y=Y\to \left(\forall b\in P\forall c\in P\forall v\in P\left(\left(\left(X\ne y\wedge y\in \left(XIz\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}y=a\underset{\dot{}}{-}b\wedge y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)\leftrightarrow \forall b\in P\forall c\in P\forall v\in P\left(\left(\left(X\ne Y\wedge Y\in \left(XIz\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)\right)$$
62	61	2ralbidv	$$⊢y=Y\to \left(\forall u\in P\forall a\in P\forall b\in P\forall c\in P\forall v\in P\left(\left(\left(X\ne y\wedge y\in \left(XIz\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}y=a\underset{\dot{}}{-}b\wedge y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)\leftrightarrow \forall u\in P\forall a\in P\forall b\in P\forall c\in P\forall v\in P\left(\left(\left(X\ne Y\wedge Y\in \left(XIz\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)\right)$$
63		oveq2	$$⊢z=Z\to XIz=XIZ$$
64	63	eleq2d	$$⊢z=Z\to \left(Y\in \left(XIz\right)\leftrightarrow Y\in \left(XIZ\right)\right)$$
65	64	3anbi2d	$$⊢z=Z\to \left(\left(X\ne Y\wedge Y\in \left(XIz\right)\wedge b\in \left(aIc\right)\right)\leftrightarrow \left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge b\in \left(aIc\right)\right)\right)$$
66		oveq2	$$⊢z=Z\to Y\underset{\dot{}}{-}z=Y\underset{\dot{}}{-}Z$$
67	66	eqeq1d	$$⊢z=Z\to \left(Y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\leftrightarrow Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)$$
68	67	anbi2d	$$⊢z=Z\to \left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\leftrightarrow \left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)\right)$$
69	68	anbi1d	$$⊢z=Z\to \left(\left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\leftrightarrow \left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)$$
70	65 69	anbi12d	$$⊢z=Z\to \left(\left(\left(X\ne Y\wedge Y\in \left(XIz\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\leftrightarrow \left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\right)$$
71		oveq1	$$⊢z=Z\to z\underset{\dot{}}{-}u=Z\underset{\dot{}}{-}u$$
72	71	eqeq1d	$$⊢z=Z\to \left(z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\leftrightarrow Z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)$$
73	70 72	imbi12d	$$⊢z=Z\to \left(\left(\left(\left(X\ne Y\wedge Y\in \left(XIz\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)\leftrightarrow \left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to Z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)\right)$$
74	73	ralbidv	$$⊢z=Z\to \left(\forall v\in P\left(\left(\left(X\ne Y\wedge Y\in \left(XIz\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)\leftrightarrow \forall v\in P\left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to Z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)\right)$$
75	74	2ralbidv	$$⊢z=Z\to \left(\forall b\in P\forall c\in P\forall v\in P\left(\left(\left(X\ne Y\wedge Y\in \left(XIz\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)\leftrightarrow \forall b\in P\forall c\in P\forall v\in P\left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to Z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)\right)$$
76	75	2ralbidv	$$⊢z=Z\to \left(\forall u\in P\forall a\in P\forall b\in P\forall c\in P\forall v\in P\left(\left(\left(X\ne Y\wedge Y\in \left(XIz\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)\leftrightarrow \forall u\in P\forall a\in P\forall b\in P\forall c\in P\forall v\in P\left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to Z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)\right)$$
77	45 62 76	rspc3v	$$⊢\left(X\in P\wedge Y\in P\wedge Z\in P\right)\to \left(\forall x\in P\forall y\in P\forall z\in P\forall u\in P\forall a\in P\forall b\in P\forall c\in P\forall v\in P\left(\left(\left(x\ne y\wedge y\in \left(xIz\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(x\underset{\dot{}}{-}y=a\underset{\dot{}}{-}b\wedge y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(x\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)\to \forall u\in P\forall a\in P\forall b\in P\forall c\in P\forall v\in P\left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to Z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)\right)$$
78	5 6 7 77	syl3anc	$$⊢\phi \to \left(\forall x\in P\forall y\in P\forall z\in P\forall u\in P\forall a\in P\forall b\in P\forall c\in P\forall v\in P\left(\left(\left(x\ne y\wedge y\in \left(xIz\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(x\underset{\dot{}}{-}y=a\underset{\dot{}}{-}b\wedge y\underset{\dot{}}{-}z=b\underset{\dot{}}{-}c\right)\wedge \left(x\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)\to \forall u\in P\forall a\in P\forall b\in P\forall c\in P\forall v\in P\left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to Z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)\right)$$
79	29 78	mpd	$$⊢\phi \to \forall u\in P\forall a\in P\forall b\in P\forall c\in P\forall v\in P\left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to Z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)$$
80		oveq2	$$⊢u=U\to X\underset{\dot{}}{-}u=X\underset{\dot{}}{-}U$$
81	80	eqeq1d	$$⊢u=U\to \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\leftrightarrow X\underset{\dot{}}{-}U=a\underset{\dot{}}{-}v\right)$$
82		oveq2	$$⊢u=U\to Y\underset{\dot{}}{-}u=Y\underset{\dot{}}{-}U$$
83	82	eqeq1d	$$⊢u=U\to \left(Y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\leftrightarrow Y\underset{\dot{}}{-}U=b\underset{\dot{}}{-}v\right)$$
84	81 83	anbi12d	$$⊢u=U\to \left(\left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\leftrightarrow \left(X\underset{\dot{}}{-}U=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=b\underset{\dot{}}{-}v\right)\right)$$
85	84	anbi2d	$$⊢u=U\to \left(\left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\leftrightarrow \left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}U=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=b\underset{\dot{}}{-}v\right)\right)\right)$$
86	85	anbi2d	$$⊢u=U\to \left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\leftrightarrow \left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}U=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=b\underset{\dot{}}{-}v\right)\right)\right)\right)$$
87		oveq2	$$⊢u=U\to Z\underset{\dot{}}{-}u=Z\underset{\dot{}}{-}U$$
88	87	eqeq1d	$$⊢u=U\to \left(Z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\leftrightarrow Z\underset{\dot{}}{-}U=c\underset{\dot{}}{-}v\right)$$
89	86 88	imbi12d	$$⊢u=U\to \left(\left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to Z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)\leftrightarrow \left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}U=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=b\underset{\dot{}}{-}v\right)\right)\right)\to Z\underset{\dot{}}{-}U=c\underset{\dot{}}{-}v\right)\right)$$
90	89	2ralbidv	$$⊢u=U\to \left(\forall c\in P\forall v\in P\left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to Z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)\leftrightarrow \forall c\in P\forall v\in P\left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}U=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=b\underset{\dot{}}{-}v\right)\right)\right)\to Z\underset{\dot{}}{-}U=c\underset{\dot{}}{-}v\right)\right)$$
91		oveq1	$$⊢a=A\to aIc=AIc$$
92	91	eleq2d	$$⊢a=A\to \left(b\in \left(aIc\right)\leftrightarrow b\in \left(AIc\right)\right)$$
93	92	3anbi3d	$$⊢a=A\to \left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge b\in \left(aIc\right)\right)\leftrightarrow \left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge b\in \left(AIc\right)\right)\right)$$
94		oveq1	$$⊢a=A\to a\underset{\dot{}}{-}b=A\underset{\dot{}}{-}b$$
95	94	eqeq2d	$$⊢a=A\to \left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\leftrightarrow X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}b\right)$$
96	95	anbi1d	$$⊢a=A\to \left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)\leftrightarrow \left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)\right)$$
97		oveq1	$$⊢a=A\to a\underset{\dot{}}{-}v=A\underset{\dot{}}{-}v$$
98	97	eqeq2d	$$⊢a=A\to \left(X\underset{\dot{}}{-}U=a\underset{\dot{}}{-}v\leftrightarrow X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}v\right)$$
99	98	anbi1d	$$⊢a=A\to \left(\left(X\underset{\dot{}}{-}U=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=b\underset{\dot{}}{-}v\right)\leftrightarrow \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=b\underset{\dot{}}{-}v\right)\right)$$
100	96 99	anbi12d	$$⊢a=A\to \left(\left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}U=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=b\underset{\dot{}}{-}v\right)\right)\leftrightarrow \left(\left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=b\underset{\dot{}}{-}v\right)\right)\right)$$
101	93 100	anbi12d	$$⊢a=A\to \left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}U=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=b\underset{\dot{}}{-}v\right)\right)\right)\leftrightarrow \left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge b\in \left(AIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=b\underset{\dot{}}{-}v\right)\right)\right)\right)$$
102	101	imbi1d	$$⊢a=A\to \left(\left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}U=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=b\underset{\dot{}}{-}v\right)\right)\right)\to Z\underset{\dot{}}{-}U=c\underset{\dot{}}{-}v\right)\leftrightarrow \left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge b\in \left(AIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=b\underset{\dot{}}{-}v\right)\right)\right)\to Z\underset{\dot{}}{-}U=c\underset{\dot{}}{-}v\right)\right)$$
103	102	2ralbidv	$$⊢a=A\to \left(\forall c\in P\forall v\in P\left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}U=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=b\underset{\dot{}}{-}v\right)\right)\right)\to Z\underset{\dot{}}{-}U=c\underset{\dot{}}{-}v\right)\leftrightarrow \forall c\in P\forall v\in P\left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge b\in \left(AIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=b\underset{\dot{}}{-}v\right)\right)\right)\to Z\underset{\dot{}}{-}U=c\underset{\dot{}}{-}v\right)\right)$$
104		eleq1	$$⊢b=B\to \left(b\in \left(AIc\right)\leftrightarrow B\in \left(AIc\right)\right)$$
105	104	3anbi3d	$$⊢b=B\to \left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge b\in \left(AIc\right)\right)\leftrightarrow \left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge B\in \left(AIc\right)\right)\right)$$
106		oveq2	$$⊢b=B\to A\underset{\dot{}}{-}b=A\underset{\dot{}}{-}B$$
107	106	eqeq2d	$$⊢b=B\to \left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}b\leftrightarrow X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}B\right)$$
108		oveq1	$$⊢b=B\to b\underset{\dot{}}{-}c=B\underset{\dot{}}{-}c$$
109	108	eqeq2d	$$⊢b=B\to \left(Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\leftrightarrow Y\underset{\dot{}}{-}Z=B\underset{\dot{}}{-}c\right)$$
110	107 109	anbi12d	$$⊢b=B\to \left(\left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)\leftrightarrow \left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}B\wedge Y\underset{\dot{}}{-}Z=B\underset{\dot{}}{-}c\right)\right)$$
111		oveq1	$$⊢b=B\to b\underset{\dot{}}{-}v=B\underset{\dot{}}{-}v$$
112	111	eqeq2d	$$⊢b=B\to \left(Y\underset{\dot{}}{-}U=b\underset{\dot{}}{-}v\leftrightarrow Y\underset{\dot{}}{-}U=B\underset{\dot{}}{-}v\right)$$
113	112	anbi2d	$$⊢b=B\to \left(\left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=b\underset{\dot{}}{-}v\right)\leftrightarrow \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=B\underset{\dot{}}{-}v\right)\right)$$
114	110 113	anbi12d	$$⊢b=B\to \left(\left(\left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=b\underset{\dot{}}{-}v\right)\right)\leftrightarrow \left(\left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}B\wedge Y\underset{\dot{}}{-}Z=B\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=B\underset{\dot{}}{-}v\right)\right)\right)$$
115	105 114	anbi12d	$$⊢b=B\to \left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge b\in \left(AIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=b\underset{\dot{}}{-}v\right)\right)\right)\leftrightarrow \left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge B\in \left(AIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}B\wedge Y\underset{\dot{}}{-}Z=B\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=B\underset{\dot{}}{-}v\right)\right)\right)\right)$$
116	115	imbi1d	$$⊢b=B\to \left(\left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge b\in \left(AIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=b\underset{\dot{}}{-}v\right)\right)\right)\to Z\underset{\dot{}}{-}U=c\underset{\dot{}}{-}v\right)\leftrightarrow \left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge B\in \left(AIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}B\wedge Y\underset{\dot{}}{-}Z=B\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=B\underset{\dot{}}{-}v\right)\right)\right)\to Z\underset{\dot{}}{-}U=c\underset{\dot{}}{-}v\right)\right)$$
117	116	2ralbidv	$$⊢b=B\to \left(\forall c\in P\forall v\in P\left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge b\in \left(AIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=b\underset{\dot{}}{-}v\right)\right)\right)\to Z\underset{\dot{}}{-}U=c\underset{\dot{}}{-}v\right)\leftrightarrow \forall c\in P\forall v\in P\left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge B\in \left(AIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}B\wedge Y\underset{\dot{}}{-}Z=B\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=B\underset{\dot{}}{-}v\right)\right)\right)\to Z\underset{\dot{}}{-}U=c\underset{\dot{}}{-}v\right)\right)$$
118	90 103 117	rspc3v	$$⊢\left(U\in P\wedge A\in P\wedge B\in P\right)\to \left(\forall u\in P\forall a\in P\forall b\in P\forall c\in P\forall v\in P\left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to Z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)\to \forall c\in P\forall v\in P\left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge B\in \left(AIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}B\wedge Y\underset{\dot{}}{-}Z=B\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=B\underset{\dot{}}{-}v\right)\right)\right)\to Z\underset{\dot{}}{-}U=c\underset{\dot{}}{-}v\right)\right)$$
119	11 8 9 118	syl3anc	$$⊢\phi \to \left(\forall u\in P\forall a\in P\forall b\in P\forall c\in P\forall v\in P\left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge b\in \left(aIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=a\underset{\dot{}}{-}b\wedge Y\underset{\dot{}}{-}Z=b\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}u=a\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}u=b\underset{\dot{}}{-}v\right)\right)\right)\to Z\underset{\dot{}}{-}u=c\underset{\dot{}}{-}v\right)\to \forall c\in P\forall v\in P\left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge B\in \left(AIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}B\wedge Y\underset{\dot{}}{-}Z=B\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=B\underset{\dot{}}{-}v\right)\right)\right)\to Z\underset{\dot{}}{-}U=c\underset{\dot{}}{-}v\right)\right)$$
120	79 119	mpd	$$⊢\phi \to \forall c\in P\forall v\in P\left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge B\in \left(AIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}B\wedge Y\underset{\dot{}}{-}Z=B\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=B\underset{\dot{}}{-}v\right)\right)\right)\to Z\underset{\dot{}}{-}U=c\underset{\dot{}}{-}v\right)$$
121	13 14 15	3jca	$$⊢\phi \to \left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge B\in \left(AIC\right)\right)$$
122	16 17	jca	$$⊢\phi \to \left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}B\wedge Y\underset{\dot{}}{-}Z=B\underset{\dot{}}{-}C\right)$$
123	18 19	jca	$$⊢\phi \to \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}V\wedge Y\underset{\dot{}}{-}U=B\underset{\dot{}}{-}V\right)$$
124	121 122 123	jca32	$$⊢\phi \to \left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge B\in \left(AIC\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}B\wedge Y\underset{\dot{}}{-}Z=B\underset{\dot{}}{-}C\right)\wedge \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}V\wedge Y\underset{\dot{}}{-}U=B\underset{\dot{}}{-}V\right)\right)\right)$$
125		oveq2	$$⊢c=C\to AIc=AIC$$
126	125	eleq2d	$$⊢c=C\to \left(B\in \left(AIc\right)\leftrightarrow B\in \left(AIC\right)\right)$$
127	126	3anbi3d	$$⊢c=C\to \left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge B\in \left(AIc\right)\right)\leftrightarrow \left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge B\in \left(AIC\right)\right)\right)$$
128		oveq2	$$⊢c=C\to B\underset{\dot{}}{-}c=B\underset{\dot{}}{-}C$$
129	128	eqeq2d	$$⊢c=C\to \left(Y\underset{\dot{}}{-}Z=B\underset{\dot{}}{-}c\leftrightarrow Y\underset{\dot{}}{-}Z=B\underset{\dot{}}{-}C\right)$$
130	129	anbi2d	$$⊢c=C\to \left(\left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}B\wedge Y\underset{\dot{}}{-}Z=B\underset{\dot{}}{-}c\right)\leftrightarrow \left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}B\wedge Y\underset{\dot{}}{-}Z=B\underset{\dot{}}{-}C\right)\right)$$
131	130	anbi1d	$$⊢c=C\to \left(\left(\left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}B\wedge Y\underset{\dot{}}{-}Z=B\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=B\underset{\dot{}}{-}v\right)\right)\leftrightarrow \left(\left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}B\wedge Y\underset{\dot{}}{-}Z=B\underset{\dot{}}{-}C\right)\wedge \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=B\underset{\dot{}}{-}v\right)\right)\right)$$
132	127 131	anbi12d	$$⊢c=C\to \left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge B\in \left(AIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}B\wedge Y\underset{\dot{}}{-}Z=B\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=B\underset{\dot{}}{-}v\right)\right)\right)\leftrightarrow \left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge B\in \left(AIC\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}B\wedge Y\underset{\dot{}}{-}Z=B\underset{\dot{}}{-}C\right)\wedge \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=B\underset{\dot{}}{-}v\right)\right)\right)\right)$$
133		oveq1	$$⊢c=C\to c\underset{\dot{}}{-}v=C\underset{\dot{}}{-}v$$
134	133	eqeq2d	$$⊢c=C\to \left(Z\underset{\dot{}}{-}U=c\underset{\dot{}}{-}v\leftrightarrow Z\underset{\dot{}}{-}U=C\underset{\dot{}}{-}v\right)$$
135	132 134	imbi12d	$$⊢c=C\to \left(\left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge B\in \left(AIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}B\wedge Y\underset{\dot{}}{-}Z=B\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=B\underset{\dot{}}{-}v\right)\right)\right)\to Z\underset{\dot{}}{-}U=c\underset{\dot{}}{-}v\right)\leftrightarrow \left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge B\in \left(AIC\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}B\wedge Y\underset{\dot{}}{-}Z=B\underset{\dot{}}{-}C\right)\wedge \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=B\underset{\dot{}}{-}v\right)\right)\right)\to Z\underset{\dot{}}{-}U=C\underset{\dot{}}{-}v\right)\right)$$
136		oveq2	$$⊢v=V\to A\underset{\dot{}}{-}v=A\underset{\dot{}}{-}V$$
137	136	eqeq2d	$$⊢v=V\to \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}v\leftrightarrow X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}V\right)$$
138		oveq2	$$⊢v=V\to B\underset{\dot{}}{-}v=B\underset{\dot{}}{-}V$$
139	138	eqeq2d	$$⊢v=V\to \left(Y\underset{\dot{}}{-}U=B\underset{\dot{}}{-}v\leftrightarrow Y\underset{\dot{}}{-}U=B\underset{\dot{}}{-}V\right)$$
140	137 139	anbi12d	$$⊢v=V\to \left(\left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=B\underset{\dot{}}{-}v\right)\leftrightarrow \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}V\wedge Y\underset{\dot{}}{-}U=B\underset{\dot{}}{-}V\right)\right)$$
141	140	anbi2d	$$⊢v=V\to \left(\left(\left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}B\wedge Y\underset{\dot{}}{-}Z=B\underset{\dot{}}{-}C\right)\wedge \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=B\underset{\dot{}}{-}v\right)\right)\leftrightarrow \left(\left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}B\wedge Y\underset{\dot{}}{-}Z=B\underset{\dot{}}{-}C\right)\wedge \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}V\wedge Y\underset{\dot{}}{-}U=B\underset{\dot{}}{-}V\right)\right)\right)$$
142	141	anbi2d	$$⊢v=V\to \left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge B\in \left(AIC\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}B\wedge Y\underset{\dot{}}{-}Z=B\underset{\dot{}}{-}C\right)\wedge \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=B\underset{\dot{}}{-}v\right)\right)\right)\leftrightarrow \left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge B\in \left(AIC\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}B\wedge Y\underset{\dot{}}{-}Z=B\underset{\dot{}}{-}C\right)\wedge \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}V\wedge Y\underset{\dot{}}{-}U=B\underset{\dot{}}{-}V\right)\right)\right)\right)$$
143		oveq2	$$⊢v=V\to C\underset{\dot{}}{-}v=C\underset{\dot{}}{-}V$$
144	143	eqeq2d	$$⊢v=V\to \left(Z\underset{\dot{}}{-}U=C\underset{\dot{}}{-}v\leftrightarrow Z\underset{\dot{}}{-}U=C\underset{\dot{}}{-}V\right)$$
145	142 144	imbi12d	$$⊢v=V\to \left(\left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge B\in \left(AIC\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}B\wedge Y\underset{\dot{}}{-}Z=B\underset{\dot{}}{-}C\right)\wedge \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=B\underset{\dot{}}{-}v\right)\right)\right)\to Z\underset{\dot{}}{-}U=C\underset{\dot{}}{-}v\right)\leftrightarrow \left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge B\in \left(AIC\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}B\wedge Y\underset{\dot{}}{-}Z=B\underset{\dot{}}{-}C\right)\wedge \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}V\wedge Y\underset{\dot{}}{-}U=B\underset{\dot{}}{-}V\right)\right)\right)\to Z\underset{\dot{}}{-}U=C\underset{\dot{}}{-}V\right)\right)$$
146	135 145	rspc2v	$$⊢\left(C\in P\wedge V\in P\right)\to \left(\forall c\in P\forall v\in P\left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge B\in \left(AIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}B\wedge Y\underset{\dot{}}{-}Z=B\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=B\underset{\dot{}}{-}v\right)\right)\right)\to Z\underset{\dot{}}{-}U=c\underset{\dot{}}{-}v\right)\to \left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge B\in \left(AIC\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}B\wedge Y\underset{\dot{}}{-}Z=B\underset{\dot{}}{-}C\right)\wedge \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}V\wedge Y\underset{\dot{}}{-}U=B\underset{\dot{}}{-}V\right)\right)\right)\to Z\underset{\dot{}}{-}U=C\underset{\dot{}}{-}V\right)\right)$$
147	10 12 146	syl2anc	$$⊢\phi \to \left(\forall c\in P\forall v\in P\left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge B\in \left(AIc\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}B\wedge Y\underset{\dot{}}{-}Z=B\underset{\dot{}}{-}c\right)\wedge \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}v\wedge Y\underset{\dot{}}{-}U=B\underset{\dot{}}{-}v\right)\right)\right)\to Z\underset{\dot{}}{-}U=c\underset{\dot{}}{-}v\right)\to \left(\left(\left(X\ne Y\wedge Y\in \left(XIZ\right)\wedge B\in \left(AIC\right)\right)\wedge \left(\left(X\underset{\dot{}}{-}Y=A\underset{\dot{}}{-}B\wedge Y\underset{\dot{}}{-}Z=B\underset{\dot{}}{-}C\right)\wedge \left(X\underset{\dot{}}{-}U=A\underset{\dot{}}{-}V\wedge Y\underset{\dot{}}{-}U=B\underset{\dot{}}{-}V\right)\right)\right)\to Z\underset{\dot{}}{-}U=C\underset{\dot{}}{-}V\right)\right)$$
148	120 124 147	mp2d	$$⊢\phi \to Z\underset{\dot{}}{-}U=C\underset{\dot{}}{-}V$$