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

Theorem tgcgrcomlr 25596
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 25582 . 2 (𝜑 → (𝐴 𝐵) = (𝐵 𝐴))
9 tgcgrcomlr.c . . 3 (𝜑𝐶𝑃)
10 tgcgrcomlr.d . . 3 (𝜑𝐷𝑃)
112, 3, 4, 5, 9, 10axtgcgrrflx 25582 . 2 (𝜑 → (𝐶 𝐷) = (𝐷 𝐶))
121, 8, 113eqtr3d 2813 1 (𝜑 → (𝐵 𝐴) = (𝐷 𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1631  wcel 2145  cfv 6031  (class class class)co 6793  Basecbs 16064  distcds 16158  TarskiGcstrkg 25550  Itvcitv 25556
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-nul 4923
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-iota 5994  df-fv 6039  df-ov 6796  df-trkgc 25568  df-trkg 25573
This theorem is referenced by:  tgcgrextend  25601  tgifscgr  25624  tgcgrsub  25625  iscgrglt  25630  trgcgrg  25631  tgcgrxfr  25634  cgr3swap12  25639  cgr3swap23  25640  tgbtwnxfr  25646  lnext  25683  tgbtwnconn1lem1  25688  tgbtwnconn1lem2  25689  tgbtwnconn1lem3  25690  tgbtwnconn1  25691  legov2  25702  legtri3  25706  legbtwn  25710  tgcgrsub2  25711  miriso  25786  mircgrextend  25798  mirtrcgr  25799  miduniq  25801  colmid  25804  symquadlem  25805  krippenlem  25806  midexlem  25808  ragcom  25814  ragflat  25820  ragcgr  25823  footex  25834  colperpexlem1  25843  mideulem2  25847  opphllem  25848  opphllem3  25862  lmiisolem  25909  hypcgrlem1  25912  trgcopy  25917  trgcopyeulem  25918  iscgra1  25923  cgracgr  25931  cgraswap  25933  cgrcgra  25934  cgracom  25935  cgratr  25936  dfcgra2  25942  sacgr  25943  acopy  25945  acopyeu  25946  cgrg3col4  25955  tgsas1  25956  tgsas3  25959  tgasa1  25960
  Copyright terms: Public domain W3C validator