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

Theorem tgcgrcomlr 25088
Description: Congruence commutes on both sides. (Contributed by Thierry Arnoux, 23-Mar-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 (𝜑 → (𝐴 𝐵) = (𝐶 𝐷))
Assertion
Ref Expression
tgcgrcomlr (𝜑 → (𝐵 𝐴) = (𝐷 𝐶))

Proof of Theorem tgcgrcomlr
StepHypRef Expression
1 tgcgrcomlr.6 . 2 (𝜑 → (𝐴 𝐵) = (𝐶 𝐷))
2 tkgeom.p . . 3 𝑃 = (Base‘𝐺)
3 tkgeom.d . . 3 = (dist‘𝐺)
4 tkgeom.i . . 3 𝐼 = (Itv‘𝐺)
5 tkgeom.g . . 3 (𝜑𝐺 ∈ TarskiG)
6 tgcgrcomlr.a . . 3 (𝜑𝐴𝑃)
7 tgcgrcomlr.b . . 3 (𝜑𝐵𝑃)
82, 3, 4, 5, 6, 7axtgcgrrflx 25074 . 2 (𝜑 → (𝐴 𝐵) = (𝐵 𝐴))
9 tgcgrcomlr.c . . 3 (𝜑𝐶𝑃)
10 tgcgrcomlr.d . . 3 (𝜑𝐷𝑃)
112, 3, 4, 5, 9, 10axtgcgrrflx 25074 . 2 (𝜑 → (𝐶 𝐷) = (𝐷 𝐶))
121, 8, 113eqtr3d 2647 1 (𝜑 → (𝐵 𝐴) = (𝐷 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wcel 1975  cfv 5786  (class class class)co 6523  Basecbs 15637  distcds 15719  TarskiGcstrkg 25042  Itvcitv 25048
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-nul 4708
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-ral 2896  df-rex 2897  df-rab 2900  df-v 3170  df-sbc 3398  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-sn 4121  df-pr 4123  df-op 4127  df-uni 4363  df-br 4574  df-iota 5750  df-fv 5794  df-ov 6526  df-trkgc 25060  df-trkg 25065
This theorem is referenced by:  tgcgrextend  25093  tgifscgr  25117  tgcgrsub  25118  iscgrglt  25123  trgcgrg  25124  tgcgrxfr  25127  cgr3swap12  25132  cgr3swap23  25133  tgbtwnxfr  25139  lnext  25176  tgbtwnconn1lem1  25181  tgbtwnconn1lem2  25182  tgbtwnconn1lem3  25183  tgbtwnconn1  25184  legov2  25195  legtri3  25199  legbtwn  25203  tgcgrsub2  25204  miriso  25279  mircgrextend  25291  mirtrcgr  25292  miduniq  25294  colmid  25297  symquadlem  25298  krippenlem  25299  midexlem  25301  ragcom  25307  ragflat  25313  ragcgr  25316  footex  25327  colperpexlem1  25336  mideulem2  25340  opphllem  25341  opphllem3  25355  lmiisolem  25402  hypcgrlem1  25405  trgcopy  25410  trgcopyeulem  25411  iscgra1  25416  cgracgr  25424  cgraswap  25426  cgrcgra  25427  cgracom  25428  cgratr  25429  dfcgra2  25435  sacgr  25436  acopy  25438  acopyeu  25439  cgrg3col4  25448  tgsas1  25449  tgsas3  25452  tgasa1  25453
  Copyright terms: Public domain W3C validator