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

Theorem tgcgrcomlr 26265
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 26247 . 2 (𝜑 → (𝐴 𝐵) = (𝐵 𝐴))
9 tgcgrcomlr.c . . 3 (𝜑𝐶𝑃)
10 tgcgrcomlr.d . . 3 (𝜑𝐷𝑃)
112, 3, 4, 5, 9, 10axtgcgrrflx 26247 . 2 (𝜑 → (𝐶 𝐷) = (𝐷 𝐶))
121, 8, 113eqtr3d 2867 1 (𝜑 → (𝐵 𝐴) = (𝐷 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2115  cfv 6338  (class class class)co 7140  Basecbs 16474  distcds 16565  TarskiGcstrkg 26215  Itvcitv 26221
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-nul 5193
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 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ral 3137  df-rex 3138  df-rab 3141  df-v 3481  df-sbc 3758  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-nul 4275  df-if 4449  df-sn 4549  df-pr 4551  df-op 4555  df-uni 4822  df-br 5050  df-iota 6297  df-fv 6346  df-ov 7143  df-trkgc 26233  df-trkg 26238
This theorem is referenced by:  tgcgrextend  26270  tgifscgr  26293  tgcgrsub  26294  iscgrglt  26299  trgcgrg  26300  tgcgrxfr  26303  cgr3swap12  26308  cgr3swap23  26309  tgbtwnxfr  26315  lnext  26352  tgbtwnconn1lem1  26357  tgbtwnconn1lem2  26358  tgbtwnconn1lem3  26359  tgbtwnconn1  26360  legov2  26371  legtri3  26375  legbtwn  26379  tgcgrsub2  26380  miriso  26455  mircgrextend  26467  mirtrcgr  26468  miduniq  26470  colmid  26473  symquadlem  26474  krippenlem  26475  midexlem  26477  ragcom  26483  ragflat  26489  ragcgr  26492  footexALT  26503  footexlem1  26504  footexlem2  26505  colperpexlem1  26515  mideulem2  26519  opphllem  26520  opphllem3  26534  lmiisolem  26581  hypcgrlem1  26584  trgcopy  26589  trgcopyeulem  26590  iscgra1  26595  cgracgr  26603  cgraswap  26605  cgrcgra  26606  cgracom  26607  cgratr  26608  flatcgra  26609  dfcgra2  26615  acopy  26618  acopyeu  26619  cgrg3col4  26638  tgsas1  26639  tgsas3  26642  tgasa1  26643
  Copyright terms: Public domain W3C validator