Theorem tgcgrcomlr 28725

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

Syntax hints:   → wi 4   = wceq 1568   ∈ wcel 2141  ‘cfv 6536  (class class class)co 7410  Basecbs 17268  distcds 17318  TarskiGcstrkg 28672  Itvcitv 28678

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733  ax-nul 5268

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rab 3415  df-v 3455  df-sbc 3744  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-iota 6492  df-fv 6544  df-ov 7413  df-trkgc 28693  df-trkg 28698

This theorem is referenced by:  tgcgrextend  28730  tgifscgr  28753  tgcgrsub  28754  iscgrglt  28759  trgcgrg  28760  tgcgrxfr  28763  cgr3swap12  28768  cgr3swap23  28769  tgbtwnxfr  28775  lnext  28812  tgbtwnconn1lem1  28817  tgbtwnconn1lem2  28818  tgbtwnconn1lem3  28819  tgbtwnconn1  28820  legov2  28831  legtri3  28835  legbtwn  28839  tgcgrsub2  28840  miriso  28923  mircgrextend  28935  mirtrcgr  28936  miduniq  28938  colmid  28941  symquadlem  28942  krippenlem  28943  midexlem  28945  ragcom  28953  ragflat  28959  ragcgr  28962  footexALT  28973  footexlem1  28974  footexlem2  28975  colperpexlem1  28986  mideulem2  28990  opphllem  28991  opphllem3  29005  lmiisolem  29079  hypcgrlem1  29082  trgcopy  29088  trgcopyeulem  29089  iscgra1  29094  cgracgr  29102  cgraswap  29104  cgrcgra  29105  cgracom  29106  cgratr  29107  flatcgra  29108  dfcgra2  29114  acopy  29117  acopyeu  29118  ragcgra  29119  ragsupplcgra  29121  cgrg3col4  29143  tgsas1  29144  tgsas3  29147  tgasa1  29148