perpprlng

Description: If two lines A and B have a common perpendicular C and lie in the same plane H , then they are parallel. Theorem 12.9 of Schwabhauser p. 122. (Contributed by Thierry Arnoux, 5-Jul-2026)

	Ref	Expression
Hypotheses	perpprlng.p	$⊢ P = {Base}_{G}$
	perpprlng.l	$⊢ L = {Line}_{𝒢} (G)$
	perpprlng.e	No typesetting found for \|- E = ( PlnG ` G ) with typecode \|-
	perpprlng.r	No typesetting found for \|- .\|\| = ( parlnG ` G ) with typecode \|-
	perpprlng.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	perpprlng.h	$⊢ φ \to H \in ran E$
	perpprlng.a	$⊢ φ \to A \subseteq H$
	perpprlng.b	$⊢ φ \to B \subseteq H$
	perpprlng.1	$⊢ φ \to C \subseteq H$
	perpprlng.q	$⊢ φ \to A ⟂_{𝒢} (G) C$
	perpprlng.2	$⊢ φ \to B ⟂_{𝒢} (G) C$
Assertion	perpprlng	$⊢ φ \to A \underset{˙}{∥} B$

Proof

Step	Hyp	Ref	Expression
1		perpprlng.p	$⊢ P = {Base}_{G}$
2		perpprlng.l	$⊢ L = {Line}_{𝒢} (G)$
3		perpprlng.e	Could not format E = ( PlnG ` G ) : No typesetting found for \|- E = ( PlnG ` G ) with typecode \|-
4		perpprlng.r	Could not format .\|\| = ( parlnG ` G ) : No typesetting found for \|- .\|\| = ( parlnG ` G ) with typecode \|-
5		perpprlng.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		perpprlng.h	$⊢ φ \to H \in ran E$
7		perpprlng.a	$⊢ φ \to A \subseteq H$
8		perpprlng.b	$⊢ φ \to B \subseteq H$
9		perpprlng.1	$⊢ φ \to C \subseteq H$
10		perpprlng.q	$⊢ φ \to A ⟂_{𝒢} (G) C$
11		perpprlng.2	$⊢ φ \to B ⟂_{𝒢} (G) C$
12	5	adantr	$⊢ (φ \land A \cap B = \emptyset) \to G \in 𝒢_{Tarski}$
13	2 5 10	perpln1	$⊢ φ \to A \in ran L$
14	13	adantr	$⊢ (φ \land A \cap B = \emptyset) \to A \in ran L$
15	2 5 11	perpln1	$⊢ φ \to B \in ran L$
16	15	adantr	$⊢ (φ \land A \cap B = \emptyset) \to B \in ran L$
17	6	adantr	$⊢ (φ \land A \cap B = \emptyset) \to H \in ran E$
18	7	adantr	$⊢ (φ \land A \cap B = \emptyset) \to A \subseteq H$
19	8	adantr	$⊢ (φ \land A \cap B = \emptyset) \to B \subseteq H$
20		simpr	$⊢ (φ \land A \cap B = \emptyset) \to A \cap B = \emptyset$
21	2 3 4 12 14 16 17 18 19 20	prlngd	$⊢ (φ \land A \cap B = \emptyset) \to A \underset{˙}{∥} B$
22	5	adantr	$⊢ (φ \land A \cap B \neq \emptyset) \to G \in 𝒢_{Tarski}$
23	13	adantr	$⊢ (φ \land A \cap B \neq \emptyset) \to A \in ran L$
24	2 3 4 22 23	prlngref	$⊢ (φ \land A \cap B \neq \emptyset) \to A \underset{˙}{∥} A$
25		simpr	$⊢ (φ \land A \cap B \neq \emptyset) \to A \cap B \neq \emptyset$
26	5	ad7antr	$⊢ (((((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land x \in C) \land y \in (B ∖ C)) \land y \neq x) \land z \in (A ∖ C)) \land z \neq x) \to G \in 𝒢_{Tarski}$
27	2 5 10	perpln2	$⊢ φ \to C \in ran L$
28	27	ad7antr	$⊢ (((((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land x \in C) \land y \in (B ∖ C)) \land y \neq x) \land z \in (A ∖ C)) \land z \neq x) \to C \in ran L$
29	6	ad7antr	$⊢ (((((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land x \in C) \land y \in (B ∖ C)) \land y \neq x) \land z \in (A ∖ C)) \land z \neq x) \to H \in ran E$
30		simp-5r	$⊢ (((((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land x \in C) \land y \in (B ∖ C)) \land y \neq x) \land z \in (A ∖ C)) \land z \neq x) \to x \in C$
31	9	ad7antr	$⊢ (((((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land x \in C) \land y \in (B ∖ C)) \land y \neq x) \land z \in (A ∖ C)) \land z \neq x) \to C \subseteq H$
32	7	ad7antr	$⊢ (((((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land x \in C) \land y \in (B ∖ C)) \land y \neq x) \land z \in (A ∖ C)) \land z \neq x) \to A \subseteq H$
33		simplr	$⊢ (((((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land x \in C) \land y \in (B ∖ C)) \land y \neq x) \land z \in (A ∖ C)) \land z \neq x) \to z \in (A ∖ C)$
34	33	eldifad	$⊢ (((((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land x \in C) \land y \in (B ∖ C)) \land y \neq x) \land z \in (A ∖ C)) \land z \neq x) \to z \in A$
35	32 34	sseldd	$⊢ (((((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land x \in C) \land y \in (B ∖ C)) \land y \neq x) \land z \in (A ∖ C)) \land z \neq x) \to z \in H$
36	8	ad7antr	$⊢ (((((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land x \in C) \land y \in (B ∖ C)) \land y \neq x) \land z \in (A ∖ C)) \land z \neq x) \to B \subseteq H$
37		simp-4r	$⊢ (((((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land x \in C) \land y \in (B ∖ C)) \land y \neq x) \land z \in (A ∖ C)) \land z \neq x) \to y \in (B ∖ C)$
38	37	eldifad	$⊢ (((((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land x \in C) \land y \in (B ∖ C)) \land y \neq x) \land z \in (A ∖ C)) \land z \neq x) \to y \in B$
39	36 38	sseldd	$⊢ (((((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land x \in C) \land y \in (B ∖ C)) \land y \neq x) \land z \in (A ∖ C)) \land z \neq x) \to y \in H$
40		eqid	$⊢ Itv (G) = Itv (G)$
41	13	ad7antr	$⊢ (((((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land x \in C) \land y \in (B ∖ C)) \land y \neq x) \land z \in (A ∖ C)) \land z \neq x) \to A \in ran L$
42		simpr	$⊢ ((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \to x \in (A \cap B)$
43	42	ad5antr	$⊢ (((((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land x \in C) \land y \in (B ∖ C)) \land y \neq x) \land z \in (A ∖ C)) \land z \neq x) \to x \in (A \cap B)$
44	43	elin1d	$⊢ (((((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land x \in C) \land y \in (B ∖ C)) \land y \neq x) \land z \in (A ∖ C)) \land z \neq x) \to x \in A$
45	1 2 40 26 41 44	tglnpt	$⊢ (((((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land x \in C) \land y \in (B ∖ C)) \land y \neq x) \land z \in (A ∖ C)) \land z \neq x) \to x \in P$
46	1 2 40 26 41 34	tglnpt	$⊢ (((((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land x \in C) \land y \in (B ∖ C)) \land y \neq x) \land z \in (A ∖ C)) \land z \neq x) \to z \in P$
47		simpr	$⊢ (((((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land x \in C) \land y \in (B ∖ C)) \land y \neq x) \land z \in (A ∖ C)) \land z \neq x) \to z \neq x$
48	47	necomd	$⊢ (((((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land x \in C) \land y \in (B ∖ C)) \land y \neq x) \land z \in (A ∖ C)) \land z \neq x) \to x \neq z$
49	1 40 2 26 45 46 48 48 41 44 34	tglinethru	$⊢ (((((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land x \in C) \land y \in (B ∖ C)) \land y \neq x) \land z \in (A ∖ C)) \land z \neq x) \to A = x L z$
50	10	ad7antr	$⊢ (((((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land x \in C) \land y \in (B ∖ C)) \land y \neq x) \land z \in (A ∖ C)) \land z \neq x) \to A ⟂_{𝒢} (G) C$
51	49 50	eqbrtrrd	$⊢ (((((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land x \in C) \land y \in (B ∖ C)) \land y \neq x) \land z \in (A ∖ C)) \land z \neq x) \to (x L z) ⟂_{𝒢} (G) C$
52	22	adantr	$⊢ ((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \to G \in 𝒢_{Tarski}$
53	52	ad2antrr	$⊢ ((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land y \in (B ∖ C)) \land y \neq x) \to G \in 𝒢_{Tarski}$
54	15	ad2antrr	$⊢ ((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \to B \in ran L$
55	54	ad2antrr	$⊢ ((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land y \in (B ∖ C)) \land y \neq x) \to B \in ran L$
56	42	elin2d	$⊢ ((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \to x \in B$
57	56	ad2antrr	$⊢ ((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land y \in (B ∖ C)) \land y \neq x) \to x \in B$
58	1 2 40 53 55 57	tglnpt	$⊢ ((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land y \in (B ∖ C)) \land y \neq x) \to x \in P$
59		simplr	$⊢ ((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land y \in (B ∖ C)) \land y \neq x) \to y \in (B ∖ C)$
60	59	eldifad	$⊢ ((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land y \in (B ∖ C)) \land y \neq x) \to y \in B$
61	1 2 40 53 55 60	tglnpt	$⊢ ((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land y \in (B ∖ C)) \land y \neq x) \to y \in P$
62		simpr	$⊢ ((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land y \in (B ∖ C)) \land y \neq x) \to y \neq x$
63	62	necomd	$⊢ ((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land y \in (B ∖ C)) \land y \neq x) \to x \neq y$
64	1 40 2 53 58 61 63 63 55 57 60	tglinethru	$⊢ ((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land y \in (B ∖ C)) \land y \neq x) \to B = x L y$
65	64	adantllr	$⊢ (((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land x \in C) \land y \in (B ∖ C)) \land y \neq x) \to B = x L y$
66	65	ad2antrr	$⊢ (((((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land x \in C) \land y \in (B ∖ C)) \land y \neq x) \land z \in (A ∖ C)) \land z \neq x) \to B = x L y$
67	11	ad7antr	$⊢ (((((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land x \in C) \land y \in (B ∖ C)) \land y \neq x) \land z \in (A ∖ C)) \land z \neq x) \to B ⟂_{𝒢} (G) C$
68	66 67	eqbrtrrd	$⊢ (((((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land x \in C) \land y \in (B ∖ C)) \land y \neq x) \land z \in (A ∖ C)) \land z \neq x) \to (x L y) ⟂_{𝒢} (G) C$
69	1 2 3 26 28 29 30 31 35 39 51 68	perpeq	$⊢ (((((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land x \in C) \land y \in (B ∖ C)) \land y \neq x) \land z \in (A ∖ C)) \land z \neq x) \to x L z = x L y$
70	69 49 66	3eqtr4d	$⊢ (((((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land x \in C) \land y \in (B ∖ C)) \land y \neq x) \land z \in (A ∖ C)) \land z \neq x) \to A = B$
71	23	ad3antrrr	$⊢ ((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land y \in (B ∖ C)) \land y \neq x) \to A \in ran L$
72	27	ad2antrr	$⊢ ((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \to C \in ran L$
73	72	ad2antrr	$⊢ ((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land y \in (B ∖ C)) \land y \neq x) \to C \in ran L$
74		simpllr	$⊢ ((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land y \in (B ∖ C)) \land y \neq x) \to x \in (A \cap B)$
75	74	elin1d	$⊢ ((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land y \in (B ∖ C)) \land y \neq x) \to x \in A$
76		eqid	$⊢ dist (G) = dist (G)$
77	1 76 40 2 5 13 27 10	perpneq	$⊢ φ \to A \neq C$
78	77	ad4antr	$⊢ ((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land y \in (B ∖ C)) \land y \neq x) \to A \neq C$
79	1 40 2 53 71 73 75 78	tglnpt4	$⊢ ((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land y \in (B ∖ C)) \land y \neq x) \to \exists z \in (A ∖ C) z \neq x$
80	79	adantllr	$⊢ (((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land x \in C) \land y \in (B ∖ C)) \land y \neq x) \to \exists z \in (A ∖ C) z \neq x$
81	70 80	r19.29a	$⊢ (((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land x \in C) \land y \in (B ∖ C)) \land y \neq x) \to A = B$
82	1 76 40 2 5 15 27 11	perpneq	$⊢ φ \to B \neq C$
83	82	ad2antrr	$⊢ ((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \to B \neq C$
84	1 40 2 52 54 72 56 83	tglnpt4	$⊢ ((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \to \exists y \in (B ∖ C) y \neq x$
85	84	adantr	$⊢ (((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land x \in C) \to \exists y \in (B ∖ C) y \neq x$
86	81 85	r19.29a	$⊢ (((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land x \in C) \to A = B$
87	52	adantr	$⊢ (((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \to G \in 𝒢_{Tarski}$
88	10	ad3antrrr	$⊢ (((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \to A ⟂_{𝒢} (G) C$
89	87 88	perpin	$⊢ (((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \to A \cap C \neq \emptyset$
90	87	adantr	$⊢ ((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \to G \in 𝒢_{Tarski}$
91	11	ad2antrr	$⊢ ((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \to B ⟂_{𝒢} (G) C$
92	91	ad2antrr	$⊢ ((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \to B ⟂_{𝒢} (G) C$
93	90 92	perpin	$⊢ ((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \to B \cap C \neq \emptyset$
94	90	adantr	$⊢ (((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \land z \in (B \cap C)) \to G \in 𝒢_{Tarski}$
95	72	ad3antrrr	$⊢ (((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \land z \in (B \cap C)) \to C \in ran L$
96		simplr	$⊢ (((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \land z \in (B \cap C)) \to y \in (A \cap C)$
97	96	elin2d	$⊢ (((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \land z \in (B \cap C)) \to y \in C$
98		simpr	$⊢ (((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \land z \in (B \cap C)) \to z \in (B \cap C)$
99	98	elin2d	$⊢ (((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \land z \in (B \cap C)) \to z \in C$
100	23	ad4antr	$⊢ (((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \land z \in (B \cap C)) \to A \in ran L$
101		simp-4r	$⊢ (((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \land z \in (B \cap C)) \to x \in (A \cap B)$
102	101	elin1d	$⊢ (((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \land z \in (B \cap C)) \to x \in A$
103	1 2 40 94 100 102	tglnpt	$⊢ (((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \land z \in (B \cap C)) \to x \in P$
104	1 2 40 94 95 97	tglnpt	$⊢ (((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \land z \in (B \cap C)) \to y \in P$
105		simpllr	$⊢ (((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \land z \in (B \cap C)) \to \neg x \in C$
106		nelne2	$⊢ (y \in C \land \neg x \in C) \to y \neq x$
107	97 105 106	syl2anc	$⊢ (((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \land z \in (B \cap C)) \to y \neq x$
108	96	elin1d	$⊢ (((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \land z \in (B \cap C)) \to y \in A$
109	1 40 2 94 104 103 107 107 100 108 102	tglinethru	$⊢ (((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \land z \in (B \cap C)) \to A = y L x$
110	88	ad2antrr	$⊢ (((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \land z \in (B \cap C)) \to A ⟂_{𝒢} (G) C$
111	109 110	eqbrtrrd	$⊢ (((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \land z \in (B \cap C)) \to (y L x) ⟂_{𝒢} (G) C$
112	1 2 40 94 95 99	tglnpt	$⊢ (((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \land z \in (B \cap C)) \to z \in P$
113		nelne2	$⊢ (z \in C \land \neg x \in C) \to z \neq x$
114	99 105 113	syl2anc	$⊢ (((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \land z \in (B \cap C)) \to z \neq x$
115	54	ad3antrrr	$⊢ (((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \land z \in (B \cap C)) \to B \in ran L$
116	98	elin1d	$⊢ (((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \land z \in (B \cap C)) \to z \in B$
117	56	ad3antrrr	$⊢ (((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \land z \in (B \cap C)) \to x \in B$
118	1 40 2 94 112 103 114 114 115 116 117	tglinethru	$⊢ (((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \land z \in (B \cap C)) \to B = z L x$
119	92	adantr	$⊢ (((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \land z \in (B \cap C)) \to B ⟂_{𝒢} (G) C$
120	118 119	eqbrtrrd	$⊢ (((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \land z \in (B \cap C)) \to (z L x) ⟂_{𝒢} (G) C$
121	1 76 40 2 94 95 97 99 103 111 120	footeq	$⊢ (((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \land z \in (B \cap C)) \to y = z$
122	121	oveq2d	$⊢ (((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \land z \in (B \cap C)) \to x L y = x L z$
123	107	necomd	$⊢ (((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \land z \in (B \cap C)) \to x \neq y$
124	1 40 2 94 103 104 123 123 100 102 108	tglinethru	$⊢ (((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \land z \in (B \cap C)) \to A = x L y$
125	114	necomd	$⊢ (((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \land z \in (B \cap C)) \to x \neq z$
126	1 40 2 94 103 112 125 125 115 117 116	tglinethru	$⊢ (((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \land z \in (B \cap C)) \to B = x L z$
127	122 124 126	3eqtr4d	$⊢ (((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \land z \in (B \cap C)) \to A = B$
128	93 127	n0limd	$⊢ ((((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \land y \in (A \cap C)) \to A = B$
129	89 128	n0limd	$⊢ (((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \land \neg x \in C) \to A = B$
130	86 129	pm2.61dan	$⊢ ((φ \land A \cap B \neq \emptyset) \land x \in (A \cap B)) \to A = B$
131	25 130	n0limd	$⊢ (φ \land A \cap B \neq \emptyset) \to A = B$
132	24 131	breqtrd	$⊢ (φ \land A \cap B \neq \emptyset) \to A \underset{˙}{∥} B$
133	21 132	pm2.61dane	$⊢ φ \to A \underset{˙}{∥} B$

Metamath Proof Explorer

Theorem perpprlng

Proof