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

Theorem tgcgrneq 26281
 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 26279 . . 3 (𝜑 → (𝐴 = 𝐵𝐶 = 𝐷))
1211necon3bid 3034 . 2 (𝜑 → (𝐴𝐵𝐶𝐷))
131, 12mpbid 235 1 (𝜑𝐶𝐷)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2112   ≠ wne 2990  ‘cfv 6328  (class class class)co 7139  Basecbs 16479  distcds 16570  TarskiGcstrkg 26228  Itvcitv 26234 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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-nul 5177 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-ral 3114  df-rex 3115  df-v 3446  df-sbc 3724  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-iota 6287  df-fv 6336  df-ov 7142  df-trkgc 26246  df-trkg 26251 This theorem is referenced by:  hlcgrex  26414  midexlem  26490  footexALT  26516  footexlem1  26517  footexlem2  26518  mideulem2  26532  opphllem3  26547  trgcopy  26602  iscgra1  26608  cgrane1  26610  cgrane2  26611  cgrcgra  26619  flatcgra  26622  cgrg3col4  26651  tgsas2  26654  tgsas3  26655  tgasa1  26656
 Copyright terms: Public domain W3C validator