Theorem tgcgrcomlr 28822

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

Step	Hyp	Ref	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 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
8	2, 3, 4, 5, 6, 7	axtgcgrrflx 28804	. 2 ⊢ (𝜑 → (𝐴 − 𝐵) = (𝐵 − 𝐴))
9		tgcgrcomlr.c	. . 3 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
10		tgcgrcomlr.d	. . 3 ⊢ (𝜑 → 𝐷 ∈ 𝑃)
11	2, 3, 4, 5, 9, 10	axtgcgrrflx 28804	. 2 ⊢ (𝜑 → (𝐶 − 𝐷) = (𝐷 − 𝐶))
12	1, 8, 11	3eqtr3d 2805	1 ⊢ (𝜑 → (𝐵 − 𝐴) = (𝐷 − 𝐶))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ‘cfv 6537  (class class class)co 7416  Basecbs 17305  distcds 17355  TarskiGcstrkg 28769  Itvcitv 28775

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-nul 5267

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7419  df-trkgc 28790  df-trkg 28795

This theorem is used by:  tgcgrextend  28827  tgifscgr  28851  tgcgrsub  28852  iscgrglt  28857  trgcgrg  28858  tgcgrxfr  28861  cgr3swap12  28866  cgr3swap23  28867  tgbtwnxfr  28873  lnext  28910  tgbtwnconn1lem1  28915  tgbtwnconn1lem2  28916  tgbtwnconn1lem3  28917  tgbtwnconn1  28918  legov2  28929  legtri3  28933  legbtwn  28937  tgcgrsub2  28938  miriso  29022  mircgrextend  29034  mirtrcgr  29035  miduniq  29037  colmid  29040  symquadlem  29041  krippenlem  29042  midexlem  29044  ragcom  29053  ragflat  29059  ragcgr  29062  footexALT  29073  footexlem1  29074  footexlem2  29075  colperpexlem1  29086  mideulem2  29090  opphllem  29091  opphllem3  29105  lmiisolem  29181  symquadmid  29184  hypcgrlem1  29185  trgcopy  29191  trgcopyeulem  29192  iscgra1  29197  cgracgr  29205  cgraswap  29207  cgrcgra  29208  cgracom  29209  cgratr  29210  zerocgra  29211  flatcgra  29212  dfcgra2  29218  acopy  29221  acopyeu  29222  ragcgra  29223  ragsupplcgra  29225  tgaaddcpbllem1  29229  cgrg3col4  29252  angmgmaddeu1  29259  tgsas1  29279  tgsas3  29282  tgasa1  29283  symquadprlng  29320  tgaltai  29325