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 26528

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1543 ∈ wcel 2112 ≠ wne 2932 ‘cfv 6358 (class class class)co 7191 Basecbs 16666 distcds 16758 TarskiGcstrkg 26475 Itvcitv 26481

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2708 ax-nul 5184

This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2073 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2728 df-clel 2809 df-ne 2933 df-ral 3056 df-rex 3057 df-rab 3060 df-v 3400 df-sbc 3684 df-dif 3856 df-un 3858 df-in 3860 df-ss 3870 df-nul 4224 df-if 4426 df-sn 4528 df-pr 4530 df-op 4534 df-uni 4806 df-br 5040 df-iota 6316 df-fv 6366 df-ov 7194 df-trkgc 26493 df-trkg 26498

This theorem is referenced by: hlcgrex 26661 midexlem 26737 footexALT 26763 footexlem1 26764 footexlem2 26765 mideulem2 26779 opphllem3 26794 trgcopy 26849 iscgra1 26855 cgrane1 26857 cgrane2 26858 cgrcgra 26866 flatcgra 26869 cgrg3col4 26898 tgsas2 26901 tgsas3 26902 tgasa1 26903

W3C validator