Theorem tgcgrneq 29002

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147   ≠ wne 2959  ‘cfv 6566  (class class class)co 7451  Basecbs 17431  distcds 17481  TarskiGcstrkg 28946  Itvcitv 28952

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5266

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574  df-ov 7454  df-trkgc 28967  df-trkg 28972

This theorem is used by:  hlcgrex  29139  midexlem  29221  footexALT  29250  footexlem1  29251  footexlem2  29252  mideulem2  29267  opphllem3  29282  trgcopy  29368  iscgra1  29374  cgrane1  29376  cgrane2  29377  cgrcgra  29385  flatcgra  29389  ragcgra  29400  tgaaddcpbllem1  29406  tgaaddcpbl  29409  cgrg3col4  29429  angmgmaddeu1  29436  angmgmaddeu2  29437  angmgmaddeu3  29438  angmgmaddeu5  29440  angmgmaddeu7  29442  angmgmaddov2lem  29444  angmgmaddov1  29445  angmgmaddov2  29446  angmgmaddcl  29448  angmgmaddlid  29449  angmgmaddrid  29450  tgsas2  29458  tgsas3  29459  tgasa1  29460  inagcgrasubbtwn  33107  inagcgratrgmain  33111  tgexta  33135