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 28568

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 28566	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷))
12	11	necon3bid 2977	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷))
13	1, 12	mpbid 232	1 ⊢ (𝜑 → 𝐶 ≠ 𝐷)

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ‘cfv 6493 (class class class)co 7361 Basecbs 17173 distcds 17223 TarskiGcstrkg 28512 Itvcitv 28518

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-ext 2709 ax-nul 5242

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-sb 2069 df-clab 2716 df-cleq 2729 df-clel 2812 df-ne 2934 df-ral 3053 df-rab 3391 df-v 3432 df-sbc 3730 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4275 df-if 4468 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-br 5087 df-iota 6449 df-fv 6501 df-ov 7364 df-trkgc 28533 df-trkg 28538

This theorem is referenced by: hlcgrex 28701 midexlem 28777 footexALT 28803 footexlem1 28804 footexlem2 28805 mideulem2 28819 opphllem3 28834 trgcopy 28889 iscgra1 28895 cgrane1 28897 cgrane2 28898 cgrcgra 28906 flatcgra 28909 cgrg3col4 28938 tgsas2 28941 tgsas3 28942 tgasa1 28943

W3C validator