tgcgrneq - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > tgcgrneq		Structured version Visualization version GIF version

Theorem tgcgrneq 28555

Description: Congruence and equality. (Contributed by Thierry Arnoux, 27-Aug-2019.)

**Hypotheses**
Ref	Expression
tkgeom.p	⊢ 𝑃 = (Base‘𝐺)
tkgeom.d	⊢ − = (dist‘𝐺)
tkgeom.i	⊢ 𝐼 = (Itv‘𝐺)
tkgeom.g	⊢ (𝜑 → 𝐺 ∈ TarskiG)
tgcgrcomlr.a	⊢ (𝜑 → 𝐴 ∈ 𝑃)
tgcgrcomlr.b	⊢ (𝜑 → 𝐵 ∈ 𝑃)
tgcgrcomlr.c	⊢ (𝜑 → 𝐶 ∈ 𝑃)
tgcgrcomlr.d	⊢ (𝜑 → 𝐷 ∈ 𝑃)
tgcgrcomlr.6	⊢ (𝜑 → (𝐴 − 𝐵) = (𝐶 − 𝐷))
tgcgrneq.1	⊢ (𝜑 → 𝐴 ≠ 𝐵)

**Assertion**
Ref	Expression
tgcgrneq	⊢ (𝜑 → 𝐶 ≠ 𝐷)

**Proof of Theorem tgcgrneq**
Step	Hyp	Ref	Expression
1		tgcgrneq.1	. 2 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
2		tkgeom.p	. . . 4 ⊢ 𝑃 = (Base‘𝐺)
3		tkgeom.d	. . . 4 ⊢ − = (dist‘𝐺)
4		tkgeom.i	. . . 4 ⊢ 𝐼 = (Itv‘𝐺)
5		tkgeom.g	. . . 4 ⊢ (𝜑 → 𝐺 ∈ TarskiG)
6		tgcgrcomlr.a	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
7		tgcgrcomlr.b	. . . 4 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
8		tgcgrcomlr.c	. . . 4 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
9		tgcgrcomlr.d	. . . 4 ⊢ (𝜑 → 𝐷 ∈ 𝑃)
10		tgcgrcomlr.6	. . . 4 ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐶 − 𝐷))
11	2, 3, 4, 5, 6, 7, 8, 9, 10	tgcgreqb 28553	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷))
12	11	necon3bid 2976	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷))
13	1, 12	mpbid 232	1 ⊢ (𝜑 → 𝐶 ≠ 𝐷)

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1541 ∈ wcel 2113 ≠ wne 2932 ‘cfv 6492 (class class class)co 7358 Basecbs 17136 distcds 17186 TarskiGcstrkg 28499 Itvcitv 28505

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-ext 2708 ax-nul 5251

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-sb 2068 df-clab 2715 df-cleq 2728 df-clel 2811 df-ne 2933 df-ral 3052 df-rab 3400 df-v 3442 df-sbc 3741 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-nul 4286 df-if 4480 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-br 5099 df-iota 6448 df-fv 6500 df-ov 7361 df-trkgc 28520 df-trkg 28525

This theorem is referenced by: hlcgrex 28688 midexlem 28764 footexALT 28790 footexlem1 28791 footexlem2 28792 mideulem2 28806 opphllem3 28821 trgcopy 28876 iscgra1 28882 cgrane1 28884 cgrane2 28885 cgrcgra 28893 flatcgra 28896 cgrg3col4 28925 tgsas2 28928 tgsas3 28929 tgasa1 28930

W3C validator