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 28461

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1541 ∈ wcel 2111 ≠ wne 2928 ‘cfv 6481 (class class class)co 7346 Basecbs 17120 distcds 17170 TarskiGcstrkg 28405 Itvcitv 28411

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 2113 ax-9 2121 ax-ext 2703 ax-nul 5242

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 2710 df-cleq 2723 df-clel 2806 df-ne 2929 df-ral 3048 df-rab 3396 df-v 3438 df-sbc 3737 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-nul 4281 df-if 4473 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4857 df-br 5090 df-iota 6437 df-fv 6489 df-ov 7349 df-trkgc 28426 df-trkg 28431

This theorem is referenced by: hlcgrex 28594 midexlem 28670 footexALT 28696 footexlem1 28697 footexlem2 28698 mideulem2 28712 opphllem3 28727 trgcopy 28782 iscgra1 28788 cgrane1 28790 cgrane2 28791 cgrcgra 28799 flatcgra 28802 cgrg3col4 28831 tgsas2 28834 tgsas3 28835 tgasa1 28836

W3C validator