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

Theorem tgcgrneq 28415
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
StepHypRef 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 (𝜑 → (𝐴 𝐵) = (𝐶 𝐷))
112, 3, 4, 5, 6, 7, 8, 9, 10tgcgreqb 28413 . . 3 (𝜑 → (𝐴 = 𝐵𝐶 = 𝐷))
1211necon3bid 2969 . 2 (𝜑 → (𝐴𝐵𝐶𝐷))
131, 12mpbid 232 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1540  wcel 2109  wne 2925  cfv 6476  (class class class)co 7340  Basecbs 17107  distcds 17157  TarskiGcstrkg 28359  Itvcitv 28365
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5241
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rab 3393  df-v 3435  df-sbc 3739  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5089  df-iota 6432  df-fv 6484  df-ov 7343  df-trkgc 28380  df-trkg 28385
This theorem is referenced by:  hlcgrex  28548  midexlem  28624  footexALT  28650  footexlem1  28651  footexlem2  28652  mideulem2  28666  opphllem3  28681  trgcopy  28736  iscgra1  28742  cgrane1  28744  cgrane2  28745  cgrcgra  28753  flatcgra  28756  cgrg3col4  28785  tgsas2  28788  tgsas3  28789  tgasa1  28790
  Copyright terms: Public domain W3C validator